Satisfiability Advancements Enabled by State Machines
Sean Weaver · OhioLink ETD Center (Ohio Library and Information Network) · 2012
This dissertation focuses on research for state-based Satisfiability (SAT) [64-66], a variant of SAT that uses state machines (Smurfs) to represent constraints.Using this constraint representation allows for compact representations of SAT problem instances that retain more ungarbled userdomain information than other more common representations such as Conjunctive Normal Form (CNF).State-base SAT also supports earlier inference deduction during search, the use of powerful search heuristics, and the integration of special purpose constraints and solvers.SBSAT, a state-based SAT research platform [144], was used and enhanced for both researching the new techniques presented here and gathering experimental data.Since the power of state-based SAT is diminished on problems naturally represented in CNF, the benchmarks used to collect results focus on domains with rich constraints such as verification and model checking.2.5.Supporting Tools 2.5.Supporting Tools Chapter 6.Conclusion 96 6.2.Future Work