Search

Abstract: Boolean Satisfiability (SAT) is a well-known NP-complete problem. Despite the theoretical hardness of SAT, backtracking search based Conflict Directed ClauseLearning (CDCL) SAT solvers can solve very large real-world SAT instances with surprising efficiency. The high efficiency of CDCL SAT solving is due to the careful integration of its key ingredients: preprocessing, inprocessing, decision heuristics,learning of clauses from conflicts, intelligent backtracking, and restarts.Clause learning from conflicts helps a CDCL solver to prune its search space and achieve solving efficiency. Since finding conflicts is the only way to learn clauses, generating conflicts at a high rate is crucial for CDCL SAT solving. A key component of CDCL SAT is the decision step, which heuristically selects an unassgined variable to make a boolean assignment during the search. Standard CDCL heuristics for branching are designed based on a look-back principle that uses information of past search states. Examples are Variable State Independent Decaying Sum (VSIDS) and Learning Rate Based (LRB). Both of these heuristics are conflict guided and prioritize selection of variables that are likely to lead to the discovery of conflicts.These decision heuristics play a crucial role for CDCL. However, there is a lack of empirical understanding of how these branching heuristics work. This has been regarded as an important open problem in SAT research. In this thesis, we study state-of-the-art CDCL decision heuristics empirically and design extensions of these heuristics based on the insights obtained from our empirical studies. First, we present a study on two types of decision variables: glue and no-glue variables. These are named depending on their appearance in a special type of learned clause calledglue-clause. We demonstrate that decisions with glue variables are more conflict efficient than decisions with non-glue variables. Based on this insight, we develop a decision strategy named glue bump, which prioritizes selection of glue-variables. We show that the glue bumping strategy implemented on top of state-of-the-art CDCL SAT solvers improves the performance of these solvers. Secondly, we present a study of the conflict generation patterns in CDCL with two leading CDCL branching heuristics. We discovered that con-flicts in CDCL are generated in phases of short bursts, often followed by longer conflict depression phases, where the search does not find any conflicts for a number of consecutive decisions. We developed a CDCL algorithmic extension named expAT that performs random exploration during substantial conflict depression phases. We demonstrated that expSAT improves the performance of state-of-the-art CDCL SAT solvers on two years of SAT competition benchmarks and on a set of hard cryptographic instances from Bitcoin mining benchmarks. Thirdly, we study conflict producing decisions in CDCL, where we distinguish two types of decisions: single conflict (sc) and multi-conflict (mc) decisions. We present a characterization of sc and mc decisions, based on the quality of learned clauses that each produces. With this characterization, we propose a decision strategy named Common ReasonVariable score Reduction (CRVR). CRVR de-prioritizes selection of those variables,which contribute to the generation of lower quality learned clauses in poor decisions. Our empirical evaluation of CRVR demonstrates performance improvement of state-of-the-art CDCL SAT solvers on Satisfiable instances.