Guiding CNF-SAT Search by Analyzing Constraint-Variable Dependencies and Clause Lengths

The type of decision strategies employed for CNF-SAT have a profound effect on the efficiency and performance of SAT engines. Over the years, a variety of decision heuristics have been proposed; each has its own achievements and limitations. This paper re-visits the issue of decision heuristics and engineers a new approach that takes an integrated view of the overall problem structure. Our approach qualitatively analyzes clause-variable dependencies by accounting for variable/literal activity, clause connectivity, distribution of variables among clauses of different lengths, and correlation among variables, to derive an initial static ordering for SAT search. To account for conflict clauses and their resolution, a corresponding dynamic variable order update strategy is also presented. Quantitative metrics are proposed that are used to devise an algorithmic approach to guide overall SAT search. Experimental results demonstrate that our strategy significantly outperforms conventional approaches