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.

Name thesis:degree_name

PhD

Level thesis:degree_level

doctoral

Discipline thesis:degree_discipline

Engineering and Applied Science: Computer Science and Engineering

Grantor dc:publisher

University of Cincinnati

Year dc:date

2012

Author dc:creator

• Weaver, Sean A.

Contributors dc:contributor

• Franco, John

• Computer Science
• Satisfiability
• BDD
• SBSAT
• nonclausal

Statement dc:rights

• unrestricted
• This thesis or dissertation is protected by copyright: all rights reserved. It may not be copied or redistributed beyond the terms of applicable copyright laws.

Language dc:language

English

Repository record dc:identifier

http://rave.ohiolink.edu/etdc/view?acc_num=ucin1353343116

OAI identifier oai:identifier

oai:etd.ohiolink.edu:ucin1353343116