Abstract
Monotone literal fixing (MLF) and learning are well-known lookahead and lookback mechanisms in propositional satisfiability (SAT). When considering Quantified Boolean Formulas (QBFs), their separate implementation leads to significant speed-ups in state-of-the-art DPLL-based solvers.
This paper is dedicated to the efficient implementation of MLF in a QBF solver with learning. The interaction between MLF and learning is far from being obvious, and it poses some nontrivial questions about both the detection and the propagation of monotone literals. Complications arise from the presence of learned constraints, and are related to the question about whether learned constraints have to be considered or not during the detection and/or propagation of monotone literals. In the paper we answer to this question both from a theoretical and from a practical point of view. We discuss the advantages and the disadvantages of various solutions, and show that our solution of choice, implemented in our solver QuBE, produces significant speed-ups in most cases. Finally, we show that MLF can be fundamental also for solving some SAT instances, taken from the 2002 SAT solvers competition.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Cadoli, M., Schaerf, M., Giovanardi, A., Giovanardi, M.: An algorithm to evaluate quantified boolean formulae and its experimental evaluation. Journal of Automated Reasoning 28(2), 101–142 (2002)
Giunchiglia, E., Narizzano, M., Tacchella, A.: Learning for Quantified Boolean Logic Satisfiability. In: 18th National Conference on Artificial Intelligence (AAAI 2002), AAAI Press/MIT Press (2002)
Le Berre, D., Simon, L., Tacchella, A.: Challenges in the QBF arena: the SAT’03 evaluation of QBF solvers. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 468–485. Springer, Heidelberg (2004)
Giunchiglia, E., Narizzano, M., Tacchella, A.: QuBE: A system for deciding Quantified Boolean Formulas satisfiability. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, p. 364. Springer, Heidelberg (2001)
Giunchiglia, E., Narizzano, M., Tacchella, A.: Backjumping for Quantified Boolean Logic Satisfiability. In: Seventeenth International Joint Conference on Artificial Intelligence (IJCAI 2001), Morgan Kaufmann, San Francisco (2001)
Giunchiglia, E., Narizzano, M., Tacchella, A.: Backjumping for Quantified Boolean Logic satisfiability. Artificial Intelligence 145, 99–120 (2003)
Giunchiglia, E., Narizzano, M., Tacchella, A.: QBF reasoning on real-world instances. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 105–121. Springer, Heidelberg (2005)
Gent, I.P., Giunchiglia, E., Narizzano, M., Rowley, A., Tacchella, A.: Watched Data Structures for QBF Solvers. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 25–36. Springer, Heidelberg (2004)
Scholl, C., Becker, B.: Checking equivalence for partial implementations. In: 38th Design Automation Conference, DAC 2001 (2001)
Ayari, A., Basin, D.: Bounded model construction for monadic second-order logics. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 99–113. Springer, Heidelberg (2000)
Rintanen, J.: Constructing conditional plans by a theorem prover. Journal of Artificial Intelligence Research 10, 323–352 (1999)
Castellini, C., Giunchiglia, E., Tacchella, A.: Sat-based planning in complex domains: Concurrency, constraints and nondeterminism. Artificial Intelligence 147(1), 85–117 (2003)
Giunchiglia, E., Maratea, M., Tacchella, A. (In)Effectiveness of Look-Ahead Techniques in a Modern SAT Solver. In: Rossi, F. (ed.) CP 2003. LNCS, vol. 2833, pp. 842–846. Springer, Heidelberg (2003)
Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proceedings of the 38th Design Automation Conference (DAC 2001), pp. 530–535 (2001)
Goldberg, E., Novikov, Y.: BerkMin: A fast and robust SAT-solver. In: Design, Automation, and Test in Europe (DATE 2002), March 2002, pp. 142–149 (2002)
Freeman, J.W.: Improvements to propositional satisfiability search algorithms. PhD thesis, University of Pennsylvania (1995)
Kuehlmann, M.K., Ganai, V.: Paruthi. Circuit-based Boolean Reasoning. In: 38th Design Automation Conference (2001)
Cadoli, M., Schaerf, M., Giovanardi, A., Giovanardi, M.: An Algorithm to Evaluate Quantified Boolean Formulae and its Experimental Evaluation. In: Highlights of Satisfiability Research in the Year 2000, IOS Press, Amsterdam (2000)
Letz, R.: Lemma and model caching in decision procedures for quantified boolean formulas. In: Egly, U., Fermüller, C. (eds.) TABLEAUX 2002. LNCS (LNAI), vol. 2381, pp. 160–175. Springer, Heidelberg (2002)
Zhang, L., Malik, S.: Conflict driven learning in a quantified boolean satisfiability solver. In: Proceedings of International Conference on Computer Aided Design, ICCAD 2002 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Giunchiglia, E., Narizzano, M., Tacchella, A. (2004). Monotone Literals and Learning in QBF Reasoning. In: Wallace, M. (eds) Principles and Practice of Constraint Programming – CP 2004. CP 2004. Lecture Notes in Computer Science, vol 3258. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30201-8_21
Download citation
DOI: https://doi.org/10.1007/978-3-540-30201-8_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23241-4
Online ISBN: 978-3-540-30201-8
eBook Packages: Springer Book Archive