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].

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) |