Solving Quantified Boolean Formulas with circuit observability don't cares

Daijue Tang, Sharad Malik

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

2 Scopus citations

Abstract

Traditionally the propositional part of a Quantified Boolean Formula (QBF) instance has been represented using a conjunctive normal form (CNF). As with propositional satisfiability (SAT), this is motivated by the efficiency of this data structure. However, in many cases, part of or the entire propositional part of a QBF instance can often be represented as a combinational logic circuit. In a logic circuit, the limited observability of the internal signals at the circuit outputs may make their assignments irrelevant for specific assignments of values to other signals in the circuit. This circuit observability don't care (ODC) information has been used to advantage in circuit based SAT solvers. A CNF encoding of the circuit, however, does not capture the signal direction and this limited observability, and thus cannot directly take advantage of this. However, recently it has been shown that this don't care information can be encoded in the CNF description and taken advantage of in a DPLL based SAT solver by modifying the decision heuristics/Boolean constraint propagation/conflict- driven-learning to account for these don't cares. Thus far, however, the use of these don't cares in the CNF encoding has not been explored for QBF solvers. In this paper, we examine how this can be done for QBF solvers as well as evaluate its practical benefits through experimentation. We have developed and implemented the usage of circuit ODCs in various parts of the DPLL-based procedure of the Quaffle QBF solver. We show that DPLL search based QBF solvers can use circuit ODC information to detect satisfying branches earlier during search and make satisfiability directed learning more effective. Our experiments demonstrate that significant performance gain can be obtained by considering circuit ODCs in checking the satisfiability of QBFs.

Original languageEnglish (US)
Title of host publicationTheory and Applications of Satisfiability Testing, SAT 2006 - 9th International Conference, Proceedings
PublisherSpringer Verlag
Pages368-381
Number of pages14
ISBN (Print)3540372067, 9783540372066
DOIs
StatePublished - 2006
Event9th International Conference on Theory and Applications of Satisfiability Testing, SAT 2006 - Seattle, WA, United States
Duration: Aug 12 2006Aug 15 2006

Publication series

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

Other

Other9th International Conference on Theory and Applications of Satisfiability Testing, SAT 2006
CountryUnited States
CitySeattle, WA
Period8/12/068/15/06

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Solving Quantified Boolean Formulas with circuit observability don't cares'. Together they form a unique fingerprint.

  • Cite this

    Tang, D., & Malik, S. (2006). Solving Quantified Boolean Formulas with circuit observability don't cares. In Theory and Applications of Satisfiability Testing, SAT 2006 - 9th International Conference, Proceedings (pp. 368-381). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4121 LNCS). Springer Verlag. https://doi.org/10.1007/11814948_34