Harald Seltner,
"Extracting Hardware Circuits from CNF Formulas"
, Johannes Kepler Universität, Linz, 7-2014
Original Titel:
Extracting Hardware Circuits from CNF Formulas
Sprache des Titels:
Englisch
Original Kurzfassung:
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.
Forschungs-