利用可滿足性問題證明核心生成的合格校正點進行工程改變命令補丁優化

Abstract

這份研究提出了一種新的方法，以解決先前工程改變命令方法中觀察到的限制。 在給定一組候選校正點的情況下，先前的方法使用量化布林公式求解器來檢驗候選的校正點集合是否足以修復錯誤，但有兩個缺點：首先，往往候選校正點不足，從而導致在重試中的運行時間過長。 其次，候選集合中可能有些多餘的校正點，導致產生的補丁將遠離最佳解。 為此，我們提出了一種高效的全稱量詞消除的方法，從而可以將校正點識別問題轉為合取範式，並透過SAT求解器解決。 我們進一步利用產生的SAT證明來提取一組最小的校正點集合，以修正工程改變命令的錯誤。 透過將證明核心作為阻斷子句加入SAT求解器中，我們能夠列舉候選集合的所有可能解。 實驗結果表明，在效率和性能方面，與傳統策略和商業工具相比，本方法取得了改進。

This work introduces a novel method to address limitations observed in previous Engineering Change Order (ECO) approaches. Given a set of rectification candidates, previous methods use Quantified Boolean Formula (QBF) solver to verify whether the candidates are adequate to fix the bug. The deficiencies of the previous approaches are twofold: First, it is often that the sets of candidates are inadequate, thus leading to excessive runtime in retrying. Second. the identified rectification points may contain redundancies and therefore the resultant patch will be far from optimality. In response, the proposed method introduces an efficient elimination of universal quantifiers, and thus the rectification point identification problem can be modelled as Conjunctive Normal Form (CNF) and solved by an SAT solver. We further utilize the resulting SAT proof to extract a minimal set of rectification points to fix the ECO bug. By adding proof cores as blocking clauses to the SAT solver, we are able to enumerate all the possible solutions of the candidate set. Experimental results demonstrate an improvement over conventional strategies and a commercial tool in terms of efficiency and performance.