×

Monotone literals and learning in QBF reasoning. (English) Zbl 1152.68554

Wallace, Mark (ed.), Principles and practice of constraint programming – CP 2004. 10th international conference, CP 2004, Toronto, Canada, September 27–October 1, 2004. Proceedings. Berlin: Springer (ISBN 978-3-540-23241-4/pbk). Lecture Notes in Computer Science 3258, 260-273 (2004).
Summary: 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.
For the entire collection see [Zbl 1139.68008].

MSC:

68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
68T05 Learning and adaptive systems in artificial intelligence

Software:

Quaffle; Chaff; BerkMin
PDFBibTeX XMLCite
Full Text: DOI