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
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 https://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=artiaex&d=paper_03043975_v450_n_p92_Castano_oai
Aporte de:	Repositorio Digital de la Universidad de Buenos Aires (UBA) de Universidad de Buenos Aires

id	I28-R145-paper_03043975_v450_n_p92_Castano_oai
record_format	dspace
spelling	I28-R145-paper_03043975_v450_n_p92_Castano_oai2024-08-16 Castaño, J.M. Castaño, R. 2012 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. application/pdf http://hdl.handle.net/20.500.12110/paper_03043975_v450_n_p92_Castano info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar Theor Comput Sci 2012;450:92-108 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 A finite state intersection approach to propositional satisfiability info:eu-repo/semantics/article info:ar-repo/semantics/artículo info:eu-repo/semantics/publishedVersion https://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=artiaex&d=paper_03043975_v450_n_p92_Castano_oai
institution	Universidad de Buenos Aires
institution_str	I-28
repository_str	R-145
collection	Repositorio Digital de la Universidad de Buenos Aires (UBA)
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 https://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=artiaex&d=paper_03043975_v450_n_p92_Castano_oai
work_keys_str_mv	AT castanojm afinitestateintersectionapproachtopropositionalsatisfiability AT castanor afinitestateintersectionapproachtopropositionalsatisfiability AT castanojm finitestateintersectionapproachtopropositionalsatisfiability AT castanor finitestateintersectionapproachtopropositionalsatisfiability
_version_	1809357220703371264

A finite state intersection approach to propositional satisfiability

Ejemplares similares