Dependency Learning for QBF (bibtex)

by Tomáš Peitl, Friedrich Slivovsky, Stefan Szeider

Abstract:

Quantified Boolean Formulas (QBFs) can be used to succinctly encode problems from domains such as formal verification, planning, and synthesis. One of the main approaches to QBF solving is Quantified Conflict Driven Clause Learning (QCDCL). By default, QCDCL assigns variables in the order of their appearance in the quantifier prefix so as to account for dependencies among variables. Dependency schemes can be used to relax this restriction and exploit independence among variables in certain cases, but only at the cost of nontrivial interferences with the proof system underlying QCDCL. We propose a new technique for exploiting variable independence within QCDCL that allows solvers to learn variable dependencies on the fly. The resulting version of QCDCL enjoys improved propagation and increased flexibility in choosing variables for branching while retaining ordinary (long-distance) Q-resolution as its underlying proof system. In experiments on standard benchmark sets, an implementation of this algorithm shows performance comparable to state-of-the-art QBF solvers.

Reference:

Dependency Learning for QBFTomáš Peitl, Friedrich Slivovsky, Stefan SzeiderTheory and Applications of Satisfiability Testing – SAT 2017 (Serge Gaspers, Toby Walsh, eds.), pages 298–313, 2017, Springer International Publishing.

Bibtex Entry:

@InProceedings{PeitlSlivovskySzeider17, author="Peitl, Tom{\'a}{\v{s}} and Slivovsky, Friedrich and Szeider, Stefan", editor="Gaspers, Serge and Walsh, Toby", title="Dependency Learning for QBF", booktitle="Theory and Applications of Satisfiability Testing -- SAT 2017", year="2017", publisher="Springer International Publishing", address="Cham", pages="298--313", abstract="Quantified Boolean Formulas (QBFs) can be used to succinctly encode problems from domains such as formal verification, planning, and synthesis. One of the main approaches to QBF solving is Quantified Conflict Driven Clause Learning (QCDCL). By default, QCDCL assigns variables in the order of their appearance in the quantifier prefix so as to account for dependencies among variables. Dependency schemes can be used to relax this restriction and exploit independence among variables in certain cases, but only at the cost of nontrivial interferences with the proof system underlying QCDCL. We propose a new technique for exploiting variable independence within QCDCL that allows solvers to learn variable dependencies on the fly. The resulting version of QCDCL enjoys improved propagation and increased flexibility in choosing variables for branching while retaining ordinary (long-distance) Q-resolution as its underlying proof system. In experiments on standard benchmark sets, an implementation of this algorithm shows performance comparable to state-of-the-art QBF solvers.", isbn="978-3-319-66263-3", doi="10.1007/978-3-319-66263-3_19", url="http://repositum.tuwien.ac.at/obvutwoa/download/pdf/2477616?originalFilename=true" }

Powered by bibtexbrowser