Boolean satisfiability (SAT) was the first problem to be proven to be NP-Complete.
The proof, provided by Stephen Cook in 1971, demonstrated that inputs accepted by
a non-deterministic Turing machine can be described by satisfying assignments of a
Boolean formula. The reduction to SAT feels natural for a wealth of decision problems;
this has motivated an immense amount of research into heuristics for solving SAT instances
quickly. Over the past decade the performance of SAT solvers has improved
tremendously, and as a consequence, real-world problems that were once thought to be
intractable are now feasible in many cases.
In this thesis we discuss how some problems in logic synthesis and verification can be
solved with Boolean satisfiability. The dissertation begins by discussing Cyclic Combinational
Circuits. Cyclic Combinational Circuits are logic circuits that contain feedback,
but exhibit no state behavior. Many functions can be implemented with fewer gates
using a cyclic topology rather than an acyclic topology. A pivotal step in synthesizing
these circuits is proving whether or not the resulting structure is actually combinational,
and if not, how to modify the circuit to behave properly. This analysis can be elegantly
cast as an instance of SAT. Furthermore, this thesis demonstrates how modern SATBased
synthesis techniques can be used to generate cyclic structures, rather than just
These SAT-Based synthesis techniques rely on augmenting proofs of unsatisfiability
to generate circuit structures. These structures, called Craig Interpolants, and the
proofs they are generated from are the focus of the second portion of this dissertation.
Techniques are proposed for reducing the size of these interpolants,and then the use of
proofs of unsatisfiability as an underlying data structure for synthesis is advocated.
Finally, the last portion of this thesis discusses some improvements to a new model
checking algorithm known as Property Directed Reachability (PDR). This algorithm iteratively solves SAT instances representing discrete time frames of a sequential circuit in order to demonstrate that a state invariant exists.
University of Minnesota Ph.D. dissertation. March 2013. Major:Electrical Engineering. Advisor: Marc D. Riedel. 1 computer file (PDF); xi, 145 pages.
Backes, John D..
Algorithms and data structures for logic synthesis and verification using Boolean satisfiability.
Retrieved from the University of Minnesota Digital Conservancy,
Content distributed via the University of Minnesota's Digital Conservancy may be subject to additional license and use restrictions applied by the depositor.