×

zbMATH — the first resource for mathematics

Applying logic synthesis for speeding up SAT. (English) Zbl 1214.68351
Marques-Silva, João (ed.) et al., Theory and applications of satisfiability testing – SAT 2007. 10th international conference, Lisbon, Portugal, May 28–31, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-72787-3/pbk). Lecture Notes in Computer Science 4501, 272-286 (2007).
Summary: SAT solvers are often challenged with very hard problems that remain unsolved after hours of CPU time. The research community meets the challenge in two ways: (1) by improving the SAT solver technology, for example, perfecting heuristics for variable ordering, and (2) by inventing new ways of constructing simpler SAT problems, either using domain specific information during the translation from the original problem to CNF, or by applying a more universal CNF simplification procedure after the translation. This paper explores preprocessing of circuit-based SAT problems using recent advances in logic synthesis. Two fast logic synthesis techniques are considered: DAG-aware logic minimization and a novel type of structural technology mapping, which reduces the size of the CNF derived from the circuit. These techniques are experimentally compared to CNF-based preprocessing. The conclusion is that the proposed techniques are complementary to CNF-based preprocessing and speedup SAT solving substantially on industrial examples.
For the entire collection see [Zbl 1120.68007].

MSC:
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
68Q25 Analysis of algorithms and problem complexity
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Software:
MiniSat
PDF BibTeX XML Cite
Full Text: DOI