2012 | OriginalPaper | Buchkapitel
Counter Implication Restart for Parallel SAT Solvers
verfasst von : Tomohiro Sonobe, Mary Inaba
Erschienen in: Learning and Intelligent Optimization
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
A portfolio approach has become the mainstream for parallel SAT solvers, making diversification of the search for each process more important. In the SAT Competition 2011, we proposed a novel restart method called counter implication restart (CIR), for sequential solvers and won gold and silver medals with CIR. CIR enables SAT solvers to change the search spaces drastically after a restart. In this paper, we propose an adaptation of CIR to parallel SAT solvers to provide better diversification. Experimental results indicate that CIR provides good diversification and its overall performance is very competitive with state-of-the-art parallel solvers.