Research Abstracts - 2006

Boolean Constraint Propagation in SAT Solvers

Shen Qu & Brian C. Williams

Boolean Satisfiability is one of the most studied combinatorial search problems. These studies resulted in an array of SAT solvers based on various algorithms. SAT algorithms can generally be broken down to 5 major parts: 1) initial preprocessing, which may include addition and deletion of clauses, initializing data structures, and initial Boolean constraint propagation (BCP), unit propagation in most cases; 2) DPLL search branching decision, which may involve any number of heuristics from random selection to conflict analysis of previous results to look ahead algorithms for current states; 3) Boolean constraint propagation resulting from the latest search decision; 4) DPLL search backtracking to decide which point in the search tree to backtrack to; and 5) Boolean constraint propagation backtracking (or unpropagation), which removes the implications made from the DPLL search decisions. Research have shown that SAT solvers spent about 90% their time on BCP and unpropagation. Therefore efficient BCP algorithms are key to the performance of SAT solvers. .

Previous Work

The 2-literal watching scheme [1, 2] and ITMS [3] are 2 algorithms that dramatically improves BCP and un-propagation performance. The former uses a clever data structure to reduce the number of clauses visited for each variable (proposition) assignment or un-assignment; and the latter uses an aggressive propositional assignment resupport algorithm to reduce the number of unnecessary propositional unassignments during BCP backtracking.

2-literal watching has two special literals for each clause called watched literals. Each proposition has two lists containing pointers to all the watched literals corresponding to it in either phase (positive or negative). Initially all propositions are not assigned. When a proposition is assigned, instead of visiting all clauses that contains a literal corresponding to that proposition, the 2-literal watching scheme allows the solver to only check clauses containing watched literals corresponding to the proposition (see Figure 1). Furthermore, proposition un-assignment during backtrack in the 2-literal watching scheme takes constant time. This is because the two watched literals are the last to be assigned to 0 in a clause, so as a result, any backtracking will make sure that the literals being watched are either unassigned, or assigned to one. Thus, no action is required to update the pointers for the literals being watched [2].

The ITMS algorithm focuses on improving BCP backtracking time. Conflict repair is a element of ITMS that allows the solver to propagate through conflicts in newly added clauses or proposition assignments before deleting clauses and unassigning propositions. This increases the chance of aggressive resupport where when a proposition loses its supporting clause, the algorithm looks for another possible support for that proposition and only unassigns the proposition if a resupport cannot be found.

Approach

In order to further improve the performance of BCP and unpropagation, we are currently working on an algorithm which combines the 2-literal watching scheme with the ITMS algorithm. There are no major issues with merging watched literals with ITMS BCP forward propagation. However, during BCP backtracking, ITMS’s idea of add-before-delete through conflict repair negates the 2-literal watching assumption that the last assigned literals (the watched literals) are the first unassigned. At the moment the merged algorithm sacrifices the constant time backtracking property of 2-literal watching in order to implement ITMS algorithm. However, we are still looking at ways to keep the full benefit of both algorithms in order to receive maximum performance gain possible.

References:

[1] Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an Efficient SAT Solver. In The Proceedings of the 39th Design Automation Conference, 2001.

[2] L. Zhang and S. Malik. The Quest for Efficient Boolean Satisfiability Solvers. In The Proceedings of the 8th International conference on computer Aided Deduction, July 2002.

[3] P. Nayak and B. Williams. Fast Context Switching in Real-time Propositional Reasoning. In The Proceedings of the AAAI Conference, 1997.