Variable and clause ordering in an FSA approach to propositional satisfiability

Mostrar otras versiones (1)

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
Autor principal: Castaño, J.M
Otros Autores: Castaño, R.
Formato: Acta de conferencia Capítulo de libro
Lenguaje:Inglés
Publicado: 2011
Acceso en línea:Registro en Scopus
DOI
Handle
Registro en la Biblioteca Digital
Aporte de:Registro referencial: Solicitar el recurso aquí
Biblioteca Central Dr. Luis F. Leloir (FCEN) de Universidad de Buenos Aires
LEADER 07311caa a22008177a 4500
001 PAPER-10372
003 AR-BaUEN
005 20230518204024.0
008 190411s2011 xx ||||fo|||| 00| 0 eng|d
024 7 |2 scopus  |a 2-s2.0-79961184618 
040 |a Scopus  |b spa  |c AR-BaUEN  |d AR-BaUEN 
100 1 |a Castaño, J.M. 
245 1 0 |a Variable and clause ordering in an FSA approach to propositional satisfiability 
260 |c 2011 
270 1 0 |m Castaño, J.M.; Depto. de Computación, FCEyN, UBAArgentina; email: jcastano@dc.uba.ar 
506 |2 openaire  |e Política editorial 
504 |a Aloul, F., Lynce, I., Prestwich, S., Symmetry Breaking in Local Search for Unsatisfiability 7th International Workshop on Symmetry and Constraint Satisfaction Problems, Providence, RI (2007) 
504 |a Aloul, F.A., Markov, I.L., Sakallah, K.A., FORCE: A fast and easy-to-implement variable-ordering heuristic (2003) ACM Great Lakes Symposium on VLSI, pp. 116-119. , ACM Press, New York 
504 |a Aloul, F.A., Ramani, A., Markov, I.L., Sakallah, K.A., Solving difficult SAT instances in the presence of symmetry (2002) DAC, pp. 731-736. , ACM Press, New York 
504 |a Barton, G.E., Computational complexity in two-level morphology (1986) Proc. of the 24th ACL, New York, pp. 53-59 
504 |a Beesley, K., Karttunen, L., (2003) Finite State Morphology, , CSLI Publications 
504 |a Biere, A., Heule, M., Van Maaren, H., Walsh, T., (2009) Handbook of Satisfiability, , IOS Press, Amsterdam 
504 |a Büchi, J.R., Weak second-order arithmetic and finite automata (1960) Zeit. Math. Logik. Grund. Math., pp. 66-92 
504 |a Castaño, J., Two views on crossing dependencies, language, biology and satisfiability (2011) 1st International Work-Conference on Linguistics, Biology and Computer Science: Interplays, , IOS Press, Amsterdam 
504 |a Darwiche, A., New Advances in Compiling CNF into Decomposable Negation Normal Form (2004) ECAI, pp. 328-332 
504 |a Elgot, C.C., Decision problems of automata design and related arithmetics (1961) Transactions of the American Mathematical Society 
504 |a Franco, J., Kouril, M., Schlipf, J., Ward, J., Weaver, S., Dransfield, M.R., Vanfleet, W.M., SBSAT: A state-based, BDD-based satisfiability solver (2004) LNCS, 2919, pp. 398-410. , Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. Springer, Heidelberg 
504 |a Gomes, C.P., Sabharwal, A., Selman, B., Model Counting (2009) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, 185, pp. 633-654. , IOS Press, Amsterdam 
504 |a Hadzic, T., Hansen, E.R., O'Sullivan, B., On Automata (2008) MDDs and BDDs in Constraint Satisfaction 
504 |a Hansen, P., Jaumard, B., Algorithms for the maximum satisfiability problem (1990) Computing, 44, pp. 279-303 
504 |a Lange, K., Rossmanith, P., The emptiness problem for intersections of regular languages (1992) LNCS, 629, pp. 346-354. , Havel, I.M., Koubek, V. (eds.) MFCS 1992. Springer, Heidelberg 
504 |a Lewis, H.R., Papadimitriou, C.H., (1997) Elements of the Theory of Computation, , 2nd edn. Prentice-Hall, Upper Saddle River 
504 |a Marek, V.W., (2010) Introduction to Mathematics of Satisfiability, , Chapman and Hall/CRC 
504 |a Muise, C., Beck, J.C., McIlraith, S., (2010) Fast D-DNNF Compilation with SharpSAT 
504 |a Sinz, C., Biere, A., Extended resolution proofs for conjoining BDDs (2006) LNCS, 3967, pp. 600-611. , Grigoriev, D., Harrison, J., Hirsch, E.A. (eds.) CSR 2006. Springer, Heidelberg 
504 |a Tapanainen, P., Applying a Finite-State Intersection Grammar (1997) Finite-State Language Processing, pp. 311-327. , Roche, E., Schabes, Y. (eds.) MIT Press, Cambridge 
504 |a Thurley, M., SharpSAT - Counting models with advanced component caching and implicit BCP (2006) LNCS, 4121, pp. 424-429. , Biere, A., Gomes, C.P. (eds.) SAT 2006. Springer, Heidelberg 
504 |a Urquhart, A., Hard examples for resolution (1987) J. ACM, 34 (1), pp. 209-219 
504 |a Vardi, M., Logic and Automata: A Match Made in Heaven (2003) LNCS, 2719, pp. 193-193. , Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. Springer, Heidelberg 
504 |a Vardi, M.Y., Wolper, P., Automata-Theoretic techniques for modal logics of programs (1986) J. Comput. Syst. Sci., 32, pp. 183-221 
504 |a Vempaty, N.R., Solving Constraint Satisfaction Problems Using Finite State Automata (1992) AAAI, pp. 453-458A4 - Universite Francois Rabelais Tours; CNRS; Region Centre; Ville de Blois; Universite de Rouen 
520 3 |a 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.  |l eng 
593 |a Depto. de Computación, FCEyN, UBA, Argentina 
690 1 0 |a ALL-SAT 
690 1 0 |a FSA INTERSECTION 
690 1 0 |a MODEL COUNTING 
690 1 0 |a REGULAR EXPRESSION COMPILATION 
690 1 0 |a ALL-SAT 
690 1 0 |a AUTOMATA COMPOSITION 
690 1 0 |a CONJUNCTIVE NORMAL FORMS 
690 1 0 |a FINITE STATE 
690 1 0 |a FSA INTERSECTION 
690 1 0 |a PROPOSITIONAL SATISFIABILITY 
690 1 0 |a REGULAR EXPRESSIONS 
690 1 0 |a RUNNING TIME 
690 1 0 |a SAT SOLVERS 
690 1 0 |a SEVERAL VARIABLES 
690 1 0 |a STATE-OF-THE-ART PERFORMANCE 
690 1 0 |a BOOLEAN FUNCTIONS 
690 1 0 |a DECISION THEORY 
700 1 |a Castaño, R. 
711 2 |c Blois  |d 13 July 2011 through 16 July 2011  |g Código de la conferencia: 85887 
773 0 |d 2011  |g v. 6807 LNCS  |h pp. 76-87  |p Lect. Notes Comput. Sci.  |n Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)  |x 03029743  |w (AR-BaUEN)CENRE-983  |z 9783642222559  |t 16th International Conference on Implementation and Application of Automata, CIAA 2011 
856 4 1 |u https://www.scopus.com/inward/record.uri?eid=2-s2.0-79961184618&doi=10.1007%2f978-3-642-22256-6_8&partnerID=40&md5=ae54abb943bc3516c70baedb508c2459  |y Registro en Scopus 
856 4 0 |u https://doi.org/10.1007/978-3-642-22256-6_8  |y DOI 
856 4 0 |u https://hdl.handle.net/20.500.12110/paper_03029743_v6807LNCS_n_p76_Castano  |y Handle 
856 4 0 |u https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v6807LNCS_n_p76_Castano  |y Registro en la Biblioteca Digital 
961 |a paper_03029743_v6807LNCS_n_p76_Castano  |b paper  |c PE 
962 |a info:eu-repo/semantics/article  |a info:ar-repo/semantics/artículo  |b info:eu-repo/semantics/publishedVersion 
963 |a VARI 
999 |c 71325 

Ejemplares similares