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

Guardado en:
Detalles Bibliográficos
Autores principales: Castaño, J.M., Castaño, R.
Formato: SER
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: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 todo:paper_03029743_v6807LNCS_n_p76_Castano
record_format dspace
spelling todo:paper_03029743_v6807LNCS_n_p76_Castano2023-10-03T15:19:19Z Variable and clause ordering in an FSA approach to propositional satisfiability Castaño, J.M. Castaño, R. 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. SER info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar 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
Castaño, J.M.
Castaño, R.
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.
format SER
author Castaño, J.M.
Castaño, R.
author_facet Castaño, J.M.
Castaño, R.
author_sort Castaño, J.M.
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
url http://hdl.handle.net/20.500.12110/paper_03029743_v6807LNCS_n_p76_Castano
work_keys_str_mv AT castanojm variableandclauseorderinginanfsaapproachtopropositionalsatisfiability
AT castanor variableandclauseorderinginanfsaapproachtopropositionalsatisfiability
_version_ 1807317496174215168

Ejemplares similares