Extracting Hardware Circuits from CNF Formulas

SAT solvers can solve the Boolean satisfiability problem efficiently. For example, they are used for formal verification and other tasks in the field of Electronic Design Automation. Most solvers require input to be in conjunctive normal form (CNF). Logic circuits can be encoded in CNF efficiently using Tseitin transformation. Such a conversion usually causes information loss. The logic paths and gates are lost. Therefore, algorithms have been proposed that aim at reconstructing circuit structures from CNF. Using these techniques might allow to apply circuit-SAT techniques to arbitrary CNFs. In this work we present the tool cnf2aig that can reconstruct circuits from CNFs and outputs them as and-inverter graphs.We give efficient algorithms for detecting the most common hardware gates in CNF. Further we have implemented a solution for the partial MAX-SAT problem that guarantees that the reconstructed circuit is maximal with respect to the gates our algorithms can detect. We show how we use a circuit fuzzer to test our tool. Concluding we give detailed benchmark results using the SAT competition 2013 application benchmarks.