טכניון מכון טכנולוגי לישראל
הטכניון מכון טכנולוגי לישראל - בית הספר ללימודי מוסמכים  
M.Sc Thesis
M.Sc StudentGershman Roman
SubjectImprovements of SAT Solving Techniques
DepartmentDepartment of Computer Science
Supervisor Professor Ofer Strichman
Full Thesis textFull thesis text - English Version


Abstract

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.