Department of
Applied
Mathematics

Unified Approach for SAT Solvers to Achieve Efficient Diversification

Mary Inaba

University of Tokyo

Abstract

(joint work with Tomohiro Sonobe)

SAT(SATisfiability) problem is well known as NP-complete problem in theory, and has various applications such as circuit design and automatic theorem proving in the real world. Recent progress of SAT solvers is remarkable, and sometimes it can solve problems with more than 1 million variables. And now, parallelization is eagerly studied for its usefullness. In this talk, first, basic elements for recent SAT solver progresses are briefly introduced. Then, our proposed framework for keeping diversity of the search is shown with its two applications; Counter Implication Restart (CIR) which was awarded in SAT competition 2011, (2nd place for UNSATapplication category, and 1st place for miniSAT-hack) and Block Branching for parallel portfolio solver.