On 21.03.2013 at 12:20 in S6, there is the following noon lecture:
Unified Approach for SAT Solvers to Achieve Efficient Diversification
University of Tokyo
(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.
Webmaster: kamweb.mff.cuni.cz Modified: 19. 10. 2010