A finite state intersection approach to propositional satisfiability

Mostrar todas las versiones(3)

We use a finite state (FSA) construction approach to address the problem of propositional satisfiability (SAT). We present 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 cons...

Descripción completa

Guardado en:

Detalles Bibliográficos
Autores principales:	Castaño, J.M., Castaño, R.
Formato:	Artículo publishedVersion
Lenguaje:	Inglés
Publicado:	2012
Materias:	ALL-SAT FSA intersection Intersection grammars (FSIG) Model counting Regular expression compilation Automata composition Clause learning Conjunctive normal forms Construction approaches Finite state Propositional satisfiability Regular expressions Running time SAT solvers Several variables State-of-the-art performance Benchmarking Boolean functions Decision theory Pattern matching Finite automata
Acceso en línea:	http://hdl.handle.net/20.500.12110/paper_03043975_v450_n_p92_Castano
Aporte de:	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires

id	paperaa:paper_03043975_v450_n_p92_Castano
record_format	dspace
spelling	paperaa:paper_03043975_v450_n_p92_Castano2023-06-12T16:47:30Z A finite state intersection approach to propositional satisfiability Theor Comput Sci 2012;450:92-108 Castaño, J.M. Castaño, R. ALL-SAT FSA intersection Intersection grammars (FSIG) Model counting Regular expression compilation ALL-SAT Automata composition Clause learning Conjunctive normal forms Construction approaches Finite state Propositional satisfiability Regular expressions Running time SAT solvers Several variables State-of-the-art performance Benchmarking Boolean functions Decision theory Pattern matching Finite automata We use a finite state (FSA) construction approach to address the problem of propositional satisfiability (SAT). We present 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. This automata construction can be considered essentially a finite state intersection grammar (FSIG). We also show how an FSIG approach can be encoded. Several variable ordering (state ordering) heuristics are compared in terms of the running time of the FSA and FSIG construction. We also present a strategy for clause ordering (automata composition). Running times of state-of-the-art model counters and BDD based SAT solvers are compared and we show that both the FSA and FSIG approaches obtain an state-of-the-art performance on some hard unsatisfiable benchmarks. It is also shown that clause learning techniques can help improve performance. This work brings up many questions on the possible use of automata and grammar models to address SAT. © 2012 Elsevier B.V. All rights reserved. 2012 info:eu-repo/semantics/article info:ar-repo/semantics/artículo info:eu-repo/semantics/publishedVersion application/pdf eng info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar http://hdl.handle.net/20.500.12110/paper_03043975_v450_n_p92_Castano
institution	Universidad de Buenos Aires
institution_str	I-28
repository_str	R-134
collection	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
language	Inglés
orig_language_str_mv	eng
topic	ALL-SAT FSA intersection Intersection grammars (FSIG) Model counting Regular expression compilation ALL-SAT Automata composition Clause learning Conjunctive normal forms Construction approaches Finite state Propositional satisfiability Regular expressions Running time SAT solvers Several variables State-of-the-art performance Benchmarking Boolean functions Decision theory Pattern matching Finite automata
spellingShingle	ALL-SAT FSA intersection Intersection grammars (FSIG) Model counting Regular expression compilation ALL-SAT Automata composition Clause learning Conjunctive normal forms Construction approaches Finite state Propositional satisfiability Regular expressions Running time SAT solvers Several variables State-of-the-art performance Benchmarking Boolean functions Decision theory Pattern matching Finite automata Castaño, J.M. Castaño, R. A finite state intersection approach to propositional satisfiability
topic_facet	ALL-SAT FSA intersection Intersection grammars (FSIG) Model counting Regular expression compilation ALL-SAT Automata composition Clause learning Conjunctive normal forms Construction approaches Finite state Propositional satisfiability Regular expressions Running time SAT solvers Several variables State-of-the-art performance Benchmarking Boolean functions Decision theory Pattern matching Finite automata
description	We use a finite state (FSA) construction approach to address the problem of propositional satisfiability (SAT). We present 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. This automata construction can be considered essentially a finite state intersection grammar (FSIG). We also show how an FSIG approach can be encoded. Several variable ordering (state ordering) heuristics are compared in terms of the running time of the FSA and FSIG construction. We also present a strategy for clause ordering (automata composition). Running times of state-of-the-art model counters and BDD based SAT solvers are compared and we show that both the FSA and FSIG approaches obtain an state-of-the-art performance on some hard unsatisfiable benchmarks. It is also shown that clause learning techniques can help improve performance. This work brings up many questions on the possible use of automata and grammar models to address SAT. © 2012 Elsevier B.V. All rights reserved.
format	Artículo Artículo publishedVersion
author	Castaño, J.M. Castaño, R.
author_facet	Castaño, J.M. Castaño, R.
author_sort	Castaño, J.M.
title	A finite state intersection approach to propositional satisfiability
title_short	A finite state intersection approach to propositional satisfiability
title_full	A finite state intersection approach to propositional satisfiability
title_fullStr	A finite state intersection approach to propositional satisfiability
title_full_unstemmed	A finite state intersection approach to propositional satisfiability
title_sort	finite state intersection approach to propositional satisfiability
publishDate	2012
url	http://hdl.handle.net/20.500.12110/paper_03043975_v450_n_p92_Castano
work_keys_str_mv	AT castanojm afinitestateintersectionapproachtopropositionalsatisfiability AT castanor afinitestateintersectionapproachtopropositionalsatisfiability AT castanojm finitestateintersectionapproachtopropositionalsatisfiability AT castanor finitestateintersectionapproachtopropositionalsatisfiability
_version_	1769810031647129600

A finite state intersection approach to propositional satisfiability

Ejemplares similares