טכניון מכון טכנולוגי לישראל
הטכניון מכון טכנולוגי לישראל - בית הספר ללימודי מוסמכים  
Ph.D Thesis
Ph.D StudentRyvchin Vadim
SubjectCore Algorithms for SAT and SAT Related Problems
DepartmentDepartment of Industrial Engineering and Management
Supervisor Professor Ofer Strichman
Full Thesis textFull thesis text - English Version


Abstract

Boolean Satisfiability (SAT) is the canonical NP-complete problem, and has numerous practical applications. This thesis focuses on three main topics related to Conflict-Driven Clause Learning (CDCL) SAT technology: core heuristics of SAT solving, Incremental SAT Solving, and Minimal Unsatisfiable Core extraction. All the suggested algorithms were implemented and tested with hundreds of public benchmarks, which proved their eectiveness. As an example of the techniques developed as part of the thesis, consider the problem of minimal unsatisfiable core extraction. A variety of tasks in formal verification require finding small or minimal unsatisfiable cores (unsatisfiable subsets of the original set of clauses). As a result, MUS extraction algorithms are currently a very active area of research. We provide several optimizations to well- known algorithms and new ideas for modifications. Several application (perhaps even most) require to minimize the High-Level Unsatisfiable Core (HLMUC), which means that what needs to be minimized is not the number of values that participate in the proof, rather the number of pre-defined sets of constraints that participate in the proof. In the thesis we propose seven heuristic improvements to the state-of-the-art which together result in an overall reduction of 55% in run time and 73% in the size of the resulting core, based on our experiments with hundreds of industrial test cases. Our work on optimizations for MUC and HLMUC culminated in the best known MUS and HLMUC solvers today: the solvers Haifa-MUC and Haifa-HLMUC, which were developed as part of this thesis, won the gold medals in the last annual competition for the fastest core- and high-level core extraction engine. The thesis is a collection of six published articles, with a joint introduction and summary.