You are viewing a javascript disabled version of the site. Please enable Javascript for this site to function properly.
Go to headerGo to navigationGo to searchGo to contentsGo to footer
In content section. Select this link to jump to navigation

DepQBF: A Dependency-Aware QBF Solver

Subtitle: System description

Article type: Research Article

Authors: Lonsing, Florian | Biere, Armin

Affiliations: Institute for Formal Models and Verification, Johannes Kepler University, Linz, Austria. E-mails: florian.lonsing@jku.at, biere@jku.at

Keywords: QBF solving, DPLL, dependency schemes, restarts

DOI: 10.3233/SAT190077

Journal: Journal on Satisfiability, Boolean Modeling and Computation, vol. 7, no. 2-3, pp. 71-76, 2010

Received 1 March 2010
|
Revision received 1 May 2010
|
Published: 1 August 2010
Get PDF open access

Abstract

We present DepQBF 0.1, a new search-based solver for quantified boolean formulae (QBF). It integrates compact dependency graphs to overcome the restrictions imposed by linear quantifier prefixes of QBFs in prenex conjunctive normal form (PCNF). DepQBF 0.1 was placed first in the main track of QBFEVAL’10 in a score-based ranking. We provide a general system overview and describe selected orthogonal features such as restarts and removal of learnt constraints.

Show more