|Ph.D Student||Ryvchin Vadim|
|Subject||Core Algorithms for SAT and SAT Related Problems|
|Department||Department of Industrial Engineering and Management||Supervisor||Professor Ofer Strichman|
|Full Thesis text|
Boolean Satisﬁability (SAT) is the canonical NP-complete problem, and has numerous practical applications. This thesis focuses on three main topics related to Conﬂict-Driven Clause Learning (CDCL) SAT technology: core heuristics of SAT solving, Incremental SAT Solving, and Minimal Unsatisﬁable Core extraction. All the suggested algorithms were implemented and tested with hundreds of public benchmarks, which proved their eﬀectiveness. As an example of the techniques developed as part of the thesis, consider the problem of minimal unsatisﬁable core extraction. A variety of tasks in formal veriﬁcation require ﬁnding small or minimal unsatisﬁable cores (unsatisﬁable 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 modiﬁcations. Several application (perhaps even most) require to minimize the High-Level Unsatisﬁable 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-deﬁned 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.