|M.Sc Student||Gershman Roman|
|Subject||Improvements of SAT Solving Techniques|
|Department||Department of Computer Science||Supervisor||Professor Ofer Strichman|
|Full Thesis text|
We present two
algorithms that improve current state-of-art SAT solving techniques. The first
algorithm is an improvement of Bacchus and Winter's Binary
Hyper-Resolution preprocessing algorithm for simplifying CNF formulas.
Unlike the original algorithm, we restrict the application of Unit-Propagation to
the roots of the Binary Implications Graph, and learn stronger implications by finding dominators that are responsible for the implications. Our algorithm HyperBinFast is typically faster and more cost-effective when run on industrial problems.
The second algorithm is a new decision heuristic in the DPLL framework. We present a theoretical model, based on abstraction-refinement, which is helpful in explaining clause-based decision heuristics such as Berkmin. Based on this model, we suggest a different heuristic, called Clause-Move-To-Front (CMTF), which attempts to keep the refinement focused on one path, in contrast to Berkmin. We also suggest a new algorithm for scoring variables, based on their activity in the internal resolution process that the SAT solver performs. Together these heuristics perform better
on average than the well-known VSIDS and Berkmin heuristics, based on a large set of industrial problems.
The algorithms described in the thesis are implemented in our SAT solver HaifaSat. HaifaSat won the third place in the 2005 SAT competition in the industrial-benchmarks category.