{"id":{"repo_id":"ohiolink","oai_identifier":"oai:etd.ohiolink.edu:ucin1353343116"},"canonical_url":"https://search.dev.ndltd.org/etd/ohiolink/oai:etd.ohiolink.edu:ucin1353343116","repository":{"repo_id":"ohiolink","name":"OhioLINK","base_url":"https://etd.ohiolink.edu/acprod/odb_etd/ws/oai/oai"},"display":{"title":"Satisfiability Advancements Enabled by State Machines","abstract":"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.","abstract_html":"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.","abstract_has_math":false,"creators":["Weaver, Sean A."],"institution":"University of Cincinnati","degree_name":"PhD","degree_level":"doctoral","degree_discipline":"Engineering and Applied Science: Computer Science and Engineering","degree_department":null,"school":null,"contributors":["Franco, John"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2012,"date_issued":"2012","date_published":"2012","updated_at":"2026-07-24T03:36:23Z","subjects":["Computer Science","Satisfiability","BDD","SBSAT","nonclausal"],"languages":["English"],"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."],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://rave.ohiolink.edu/etdc/view?acc_num=ucin1353343116","outbound_label":"Repository record","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Franco, John"]},{"key":"dc:creator","label":"Author","values":["Weaver, Sean A."]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2012"]},{"key":"dc:publisher","label":"Institution","values":["University of Cincinnati / OhioLINK"]},{"key":"dc:type","label":"Dc Type","values":["Electronic Thesis or Dissertation"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Engineering and Applied Science: Computer Science and Engineering"]},{"key":"thesis:degree_level","label":"Degree Level","values":["doctoral"]},{"key":"thesis:degree_name","label":"Degree Name","values":["PhD"]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Cincinnati"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Computer Science","Satisfiability","BDD","SBSAT","nonclausal"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["English"]},{"key":"dc:rights","label":"Dc Rights","values":["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."]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://rave.ohiolink.edu/etdc/view?acc_num=ucin1353343116"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["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."]},{"key":"dc:format","label":"Dc Format","values":["application/pdf","p.115","1.66 MB"]},{"key":"dc:title","label":"Title","values":["Satisfiability Advancements Enabled by State Machines"]}]}],"canonical_facts":{"dc:contributor":["Franco, John"],"dc:creator":["Weaver, Sean A."],"dc:date":["2012"],"dc:description":["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."],"dc:format":["application/pdf","p.115","1.66 MB"],"dc:identifier":["http://rave.ohiolink.edu/etdc/view?acc_num=ucin1353343116"],"dc:language":["English"],"dc:publisher":["University of Cincinnati / OhioLINK"],"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."],"dc:subject":["Computer Science","Satisfiability","BDD","SBSAT","nonclausal"],"dc:title":["Satisfiability Advancements Enabled by State Machines"],"dc:type":["Electronic Thesis or Dissertation"],"thesis:degree_discipline":["Engineering and Applied Science: Computer Science and Engineering"],"thesis:degree_level":["doctoral"],"thesis:degree_name":["PhD"],"thesis:institution_name":["University of Cincinnati"]},"updated_at":"2026-07-24T03:36:23Z"}