zbMATH — the first resource for mathematics

Improved local search for circuit satisfiability. (English) Zbl 1306.68151
Strichman, Ofer (ed.) et al., Theory and applications of satisfiability testing – SAT 2010. 13th international conference, SAT 2010, Edinburgh, UK, July 11–14, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-14185-0/pbk). Lecture Notes in Computer Science 6175, 293-299 (2010).
Summary: In this paper we describe a significant improvement to the justification-based local search algorithm for circuit satisfiability proposed by M. J√§rvisalo et al. [“Justification-based non-clausal local search for SAT”, in: M. Ghallab (ed.) et al., Proceedings of the 18th European conference on artificial intelligence, ECAI 2008. Amsterdam: IOS Press. 535–539 (2008)]. By carefully combining local search with Boolean Constraint Propagation we achieve multiple orders of magnitude reduction in run-time on industrial and structured benchmark circuits, and, in some cases, performance comparable with complete SAT solvers.
For the entire collection see [Zbl 1196.68013].
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
94C10 Switching theory, application of Boolean algebra; Boolean functions (MSC2010)
MiniSat; UnitWalk
Full Text: DOI