Variable and clause ordering in an FSA approach to propositional satisfiability

We use a finite state (FSA) construction approach to address the problem of propositional satisfiability (SAT). We use a very simple translation from formulas in conjunctive normal form (CNF) to regular expressions and use regular expressions to construct an FSA. As a consequence of the FSA construc...

Descripción completa

Detalles Bibliográficos
Publicado: 2011
Materias:
ALL-SAT
FSA intersection
model counting
regular expression compilation
Automata composition
Conjunctive normal forms
Finite state
Propositional satisfiability
Regular expressions
Running time
SAT solvers
Several variables
State-of-the-art performance
Boolean functions
Decision theory
Acceso en línea:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v6807LNCS_n_p76_Castano
http://hdl.handle.net/20.500.12110/paper_03029743_v6807LNCS_n_p76_Castano
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id paper:paper_03029743_v6807LNCS_n_p76_Castano
record_format dspace
spelling paper:paper_03029743_v6807LNCS_n_p76_Castano2023-06-08T15:28:40Z Variable and clause ordering in an FSA approach to propositional satisfiability ALL-SAT FSA intersection model counting regular expression compilation ALL-SAT Automata composition Conjunctive normal forms Finite state FSA intersection Propositional satisfiability Regular expressions Running time SAT solvers Several variables State-of-the-art performance Boolean functions Decision theory We use a finite state (FSA) construction approach to address the problem of propositional satisfiability (SAT). We use a very simple translation from formulas in conjunctive normal form (CNF) to regular expressions and use regular expressions to construct an FSA. As a consequence of the FSA construction, we obtain an ALL-SAT solver and model counter. We compare how several variable ordering (state ordering) heuristics affect the running time of the FSA construction. We also present a strategy for clause ordering (automata composition). We compare the running time of state-of-the-art model counters, BDD based sat solvers and we show that this FSA approach obtains state-of-the-art performance on some hard unsatisfiable benchmarks. This work brings up many questions on the possible use of automata to address SAT. © 2011 Springer-Verlag. 2011 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v6807LNCS_n_p76_Castano http://hdl.handle.net/20.500.12110/paper_03029743_v6807LNCS_n_p76_Castano
institution Universidad de Buenos Aires
institution_str I-28
repository_str R-134
collection Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
topic ALL-SAT
FSA intersection
model counting
regular expression compilation
ALL-SAT
Automata composition
Conjunctive normal forms
Finite state
FSA intersection
Propositional satisfiability
Regular expressions
Running time
SAT solvers
Several variables
State-of-the-art performance
Boolean functions
Decision theory
spellingShingle ALL-SAT
FSA intersection
model counting
regular expression compilation
ALL-SAT
Automata composition
Conjunctive normal forms
Finite state
FSA intersection
Propositional satisfiability
Regular expressions
Running time
SAT solvers
Several variables
State-of-the-art performance
Boolean functions
Decision theory
Variable and clause ordering in an FSA approach to propositional satisfiability
topic_facet ALL-SAT
FSA intersection
model counting
regular expression compilation
ALL-SAT
Automata composition
Conjunctive normal forms
Finite state
FSA intersection
Propositional satisfiability
Regular expressions
Running time
SAT solvers
Several variables
State-of-the-art performance
Boolean functions
Decision theory
description We use a finite state (FSA) construction approach to address the problem of propositional satisfiability (SAT). We use a very simple translation from formulas in conjunctive normal form (CNF) to regular expressions and use regular expressions to construct an FSA. As a consequence of the FSA construction, we obtain an ALL-SAT solver and model counter. We compare how several variable ordering (state ordering) heuristics affect the running time of the FSA construction. We also present a strategy for clause ordering (automata composition). We compare the running time of state-of-the-art model counters, BDD based sat solvers and we show that this FSA approach obtains state-of-the-art performance on some hard unsatisfiable benchmarks. This work brings up many questions on the possible use of automata to address SAT. © 2011 Springer-Verlag.
title Variable and clause ordering in an FSA approach to propositional satisfiability
title_short Variable and clause ordering in an FSA approach to propositional satisfiability
title_full Variable and clause ordering in an FSA approach to propositional satisfiability
title_fullStr Variable and clause ordering in an FSA approach to propositional satisfiability
title_full_unstemmed Variable and clause ordering in an FSA approach to propositional satisfiability
title_sort variable and clause ordering in an fsa approach to propositional satisfiability
publishDate 2011
url https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v6807LNCS_n_p76_Castano
http://hdl.handle.net/20.500.12110/paper_03029743_v6807LNCS_n_p76_Castano
_version_ 1768542738268028928

Ejemplares similares