Towards a symmetric treatment of satisfaction and conflicts in quantified Boolean formula evaluation

Lintao Zhang, Sharad Malik

Research output: Chapter in Book/Report/Conference proceedingConference contribution

74 Scopus citations

Abstract

In this paper, we describe a new framework for evaluating Quantified Boolean Formulas (QBF). The new framework is based on the Davis-Putnam (DPLL) search algorithm. In existing DPLL based QBF algorithms, the problem database is represented in Conjunctive Normal Form (CNF) as a set of clauses, implications are generated from these clauses, and backtracking in the search tree is chronological.In this work, we augment the basic DPLL algorithm with conflict driven learning as well as satisfiability directed implication and learning. In addition to the traditional clause database, we add a cube database to the data structure. We show that cubes can be used to generate satisfiability directed implications similar to conflict directed implications generated by the clauses. We show that in a QBF setting,conflicting leaves and satisfying leaves of the search tree both provide valuable information to the solver in a symmetric way. We have implemented our algorithm in the new QBF solver Quaffle.Experimental results show that for some test cases, satisfiability directed implication and learning significantly prunes the search.

Original languageEnglish (US)
Title of host publicationPrinciples and Practice of Constraint Programming- CP 2002 - 8th International Conference, CP 2002, Proceedings
EditorsPascal Van Hentenryck
PublisherSpringer Verlag
Pages200-215
Number of pages16
ISBN (Print)3540441204, 9783540441205
DOIs
StatePublished - 2002
Event8th International Conference on Principles and Practice of Constraint Programming, CP 2002 - Ithaca, United States
Duration: Sep 9 2002Sep 13 2002

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2470
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other8th International Conference on Principles and Practice of Constraint Programming, CP 2002
CountryUnited States
CityIthaca
Period9/9/029/13/02

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Towards a symmetric treatment of satisfaction and conflicts in quantified Boolean formula evaluation'. Together they form a unique fingerprint.

  • Cite this

    Zhang, L., & Malik, S. (2002). Towards a symmetric treatment of satisfaction and conflicts in quantified Boolean formula evaluation. In P. Van Hentenryck (Ed.), Principles and Practice of Constraint Programming- CP 2002 - 8th International Conference, CP 2002, Proceedings (pp. 200-215). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2470). Springer Verlag. https://doi.org/10.1007/3-540-46135-3_14