Sciweavers

FUIN
2010
112views more  FUIN 2010»
13 years 9 months ago
An Empirical Study of QBF Encodings: from Treewidth Estimation to Useful Preprocessing
From an empirical point of view, the hardness of quantified Boolean formulas (QBFs), can be characterized by the (in)ability of current state-of-the-art QBF solvers to decide abo...
Luca Pulina, Armando Tacchella
ENTCS
2007
141views more  ENTCS 2007»
13 years 10 months ago
Compressing BMC Encodings with QBF
Symbolic model checking is PSPACE complete. Since QBF is the standard PSPACE complete problem, it is most natural to encode symbolic model checking problems as QBF formulas and th...
Toni Jussila, Armin Biere
MSV
2004
14 years 5 days ago
An Effective QBF Solver for Planning Problems
A large number of applications can be represented by quantified Boolean formulas (QBF). Although evaluating QBF is NP-hard and thus very difficult, there has been significant progr...
Charles Otwell, Anja Remshagen, Klaus Truemper
DATE
2010
IEEE
126views Hardware» more  DATE 2010»
14 years 3 months ago
Leveraging dominators for preprocessing QBF
— Many CAD for VLSI problems can be naturally encoded as Quantified Boolean Formulas (QBFs) and solved with QBF solvers. Furthermore, such problems often contain circuitbased in...
Hratch Mangassarian, Bao Le, Alexandra Goultiaeva,...
SAT
2005
Springer
123views Hardware» more  SAT 2005»
14 years 4 months ago
Bounded Model Checking with QBF
Current algorithms for bounded model checking (BMC) use SAT methods for checking satisfiability of Boolean formulas. These BMC methods suffer from a potential memory explosion prob...
Nachum Dershowitz, Ziyad Hanna, Jacob Katz
VLSID
2005
IEEE
97views VLSI» more  VLSID 2005»
14 years 4 months ago
Q-PREZ: QBF Evaluation Using Partition, Resolution and Elimination with ZBDDs
In recent years, there has been an increasing interest in Quantified Boolean Formula (QBF) evaluation, since several VLSI CAD problems can be formulated efficiently as QBF insta...
Kameshwar Chandrasekar, Michael S. Hsiao
SAT
2009
Springer
158views Hardware» more  SAT 2009»
14 years 5 months ago
Beyond CNF: A Circuit-Based QBF Solver
State-of-the-art solvers for Quantified Boolean Formulas (QBF) have employed many techniques from the field of Boolean Satisfiability (SAT) including the use of Conjunctive Norm...
Alexandra Goultiaeva, Vicki Iverson, Fahiem Bacchu...
DATE
2009
IEEE
113views Hardware» more  DATE 2009»
14 years 5 months ago
Exploiting structure in an AIG based QBF solver
—In this paper we present a procedure for solving quantified boolean formulas (QBF), which uses And-Inverter Graphs (AIGs) as the core data-structure. We make extensive use of s...
Florian Pigorsch, Christoph Scholl