Satisfiability advancements enabled by state machines

This dissertation focuses on research for state-based Satisfiability (SAT), 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 user-domain 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, 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.