Sign in
Author

Conference

Journal

Organization

Year

DOI
Look for results that meet for the following criteria:
since
equal to
before
between
and
Search in all fields of study
Limit my searches in the following fields of study
Agriculture Science
Arts & Humanities
Biology
Chemistry
Computer Science
Economics & Business
Engineering
Environmental Sciences
Geosciences
Material Science
Mathematics
Medicine
Physics
Social Science
Multidisciplinary
Keywords
(4)
Boolean Satisfiability
Sat Solver
Conjunctive Normal Form
Quantified Boolean Formula
Related Publications
(1)
Exploiting QBF Duality on a Circuit Representation
Subscribe
Academic
Publications
Beyond CNF: A CircuitBased QBF Solver
Beyond CNF: A CircuitBased QBF Solver,10.1007/9783642027772_38,Alexandra Goultiaeva,Vicki Iverson,Fahiem Bacchus
Edit
Beyond CNF: A CircuitBased QBF Solver
(
Citations: 7
)
BibTex

RIS

RefWorks
Download
Alexandra Goultiaeva
,
Vicki Iverson
,
Fahiem Bacchus
Stateoftheart solvers for Quantified Boolean Formulas (QBF) have employed many techniques from the field of
Boolean Satisfiability
(SAT) including the use of
Conjunctive Normal Form
(CNF) in representing the QBF formula. Although CNF has worked well for SAT solvers, recent work has pointed out some inherent problems with using CNF in QBF solvers. In this paper, we describe a QBF solver, called CirQit (CirQit) that utilizes a circuit representation rather than CNF. The solver can exploit its circuit representation to avoid many of the problems of CNF. For example, we show how this approach generalizes some previously proposed techniques for overcoming the disadvantages of CNF for QBF solvers. We also show how important techniques like clause and cube learning can be made to work with a circuit representation. Finally, we empirically compare the resulting solver against other stateoftheart QBF solvers, demonstrating that our approach can often outperform these solvers.
Conference:
Theory and Applications of Satisfiability Testing
, pp. 412426, 2009
DOI:
10.1007/9783642027772_38
Cumulative
Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
(
www.springerlink.com
)
(
www.springerlink.com
)
(
dx.doi.org
)
(
www.informatik.unitrier.de
)
More »
Citation Context
(7)
...It has thus been proposed to use nonprenex nonclausal form [11], [
15
]...
Christoph M. Wintersteiger
,
et al.
Efficiently solving quantified bitvector formulas
...in [8,16]. The latter corresponds to directly considering the parse tree of a formula and can be integrated in nonPCNF solvers such as [9,
18
,28]...
Florian Lonsing
,
et al.
Integrating Dependency Schemes in SearchBased QBF Solvers
...For example, in [
2
] a QBF solver utilizing a circuit representation was presented and shown to have some advantages over CNF based solvers...
...We have implemented all of these techniques as an extension of the CirQit solver [
2
], and we present empirical evidence supporting their usefulness...
...In circuitbased solvers, e.g., the CirQit solver of [
2
], φ is represented as a logical circuit consisting of AND, OR and NOT gates along with lines running from gate outputs to the inputs of other gates...
...As shown in [
2
] clausal reasons for each forced line can be extracted from the circuit, and clause learning can be performed when conflicts are detected...
...Table 1 shows the comparison between CirQit2.1, CirQit2 [3], CirQit [
2
] and some stateoftheart CNFbased QBF solvers: quantor (version 3.0, with the recommended picosat back end) [6], Qube (version 6.5) [7], nenofex [8] and depqbf [9]—the latter two are the versions submitted to the main track of QBFEVAL’10...
Alexandra Goultiaeva
,
et al.
Exploiting Circuit Representations in QBF Solving
...In particular, circuit observability don’tcares can be used to improve the performance of QBF solvers [11], [
12
] just as they did for SAT [13], [14]...
...More recently, QBF solvers that handle problems directly in a circuitbased format have shown promising results using various solving methods [
12
], [17], [18]...
...They are originally given in the QBF1.0 format, and are converted in negligible time into our specified format using the converter of [
12
]...
...Since none of the +sim runs terminate, our results were validated using the circuitbased QBF solver CirQit [
12
]...
Hratch Mangassarian
,
et al.
Leveraging dominators for preprocessing QBF
...Efficient QBF solvers would be of great benefit in applications such as model checking and verification, and multiagent planning [
GIB09
], however the effectiveness of QBF solvers lags far behind that of SAT solvers...
...In this context even more so than for SAT, techniques for solving the problem directly on formulae would be useful [
GIB09
], [Zha06]...
Rahul Santhanam
.
Fighting Perebor: New and Improved Algorithms for Formula and QBF Sati...
References
(19)
Asymptotically Optimal Encodings of Conformant Planning in QBF
(
Citations: 4
)
Jussi Rintanen
Conference:
National Conference on Artificial Intelligence  AAAI
, pp. 10451050, 2007
Solving Advanced Reasoning Tasks Using Quantified Boolean Formulas
(
Citations: 84
)
Uwe Egly
,
Thomas Eiter
,
Hans Tompits
,
Stefan Woltran
Conference:
National Conference on Artificial Intelligence  AAAI
, pp. 417422, 2000
A performancedriven QBFbased iterative logic array representation with applications to verification, debug and test
(
Citations: 18
)
Hratch Mangassarian
,
Andreas G. Veneris
,
Sean Safarpour
,
Marco Benedetti
,
Duncan Smith
Conference:
International Conference on Computer Aided Design  ICCAD
, pp. 240245, 2007
A Computing Procedure for Quantification Theory
(
Citations: 1436
)
Martin Davis
,
Hilary Putnam
Journal:
Journal of The ACM  JACM
, vol. 7, no. 3, pp. 201215, 1960
Resolve and Expand
(
Citations: 122
)
Armin Biere
Conference:
Theory and Applications of Satisfiability Testing
, pp. 5970, 2004
Sort by:
Citations
(7)
Efficiently solving quantified bitvector formulas
(
Citations: 4
)
Christoph M. Wintersteiger
,
Youssef Hamadi
,
Leonardo Mendonça de Moura
Conference:
Formal Methods in ComputerAided Design  FMCAD
, pp. 239246, 2010
Integrating Dependency Schemes in SearchBased QBF Solvers
(
Citations: 2
)
Florian Lonsing
,
Armin Biere
Conference:
Theory and Applications of Satisfiability Testing
, pp. 158171, 2010
Exploiting Circuit Representations in QBF Solving
(
Citations: 1
)
Alexandra Goultiaeva
,
Fahiem Bacchus
Conference:
Theory and Applications of Satisfiability Testing
, pp. 333339, 2010
Leveraging dominators for preprocessing QBF
(
Citations: 1
)
Hratch Mangassarian
,
Bao Le
,
Alexandra Goultiaeva
,
Andreas G. Veneris
,
Fahiem Bacchus
Conference:
Design, Automation, and Test in Europe  DATE
, pp. 16951700, 2010
Fighting Perebor: New and Improved Algorithms for Formula and QBF Satisfiability
(
Citations: 1
)
Rahul Santhanam
Conference:
IEEE Symposium on Foundations of Computer Science  FOCS
, pp. 183192, 2010