Go to page
 

Bibliographic Metadata

Title
Dependency Learning for QBF
AuthorPeitl, Tomáš ; Slivovsky, Friedrich ; Szeider, Stefan
Published in
Theory and Applications of Satisfiability Testing SAT 2017 : Gaspers, Serge; Walsh, Toby, Cham, 2017, page 298-313
Published2017
LanguageEnglish
SeriesLecture Notes in Computer Science ; 10491
Document typeArticle in a collected edition
Keywords (EN)Quantified Boolean Formulas / Quantified Conflict Driven Clause Learning / Variable Dependencies
Project-/ReportnumberAustrian Science Fund (FWF): P27721
Project-/ReportnumberAustrian Science Fund (FWF): W1255-N23
ISBN9783319662633
URNurn:nbn:at:at-ubtuw:3-3440 Persistent Identifier (URN)
DOI10.1007/978-3-319-66263-3_19 
Restriction-Information
 The work is publicly available
Files
Dependency Learning for QBF [0.35 mb]
Links
Reference
Classification
Abstract (English)

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.

Note
Note
Stats
The PDF-Document has been downloaded 33 times.