Author
|
Conference
|
Journal
|
Organization
|
Year
|
DOI
Look for results that meet for the following criteria:
since
equal to
before
between
and
Search in all domains
Limit my searches in the following domains
Agriculture Science
Arts & Humanities
Biology
Chemistry
Computer Science
Economics & Business
Engineering
Environmental Sciences
Geosciences
Material Science
Mathematics
Medicine
Physics
Social Science
Multidisciplinary
Keywords
(7)
Benchmark Problem
Binary Decision Diagram
Knowledge Representation and Reasoning
Propositional Logic
Satisfiability
Search Algorithm
Quantified Boolean Formula
Related Publications
(2)
Quantifier structure in search based procedures for QBFs
QUBOS: Deciding Quantified Boolean Logic Using Propositional Satisfiability Solvers
Subscribe
Academic
Publications
Embedding Memoization to the Semantic Tree Search for Deciding QBFs
Edit
Embedding Memoization to the Semantic Tree Search for Deciding QBFs
(
Citations: 4
)
BibTex
|
RIS
|
RefWorks
Download
Mohammad Ghasemzadeh
,
Volker Klotz
,
Christoph Meinel
Quantified Boolean formulas (QBFs) play an important role in arti- ficial intelligence subjects, specially in planning,
knowledge representation and reasoning
(20). In this paper we present ZQSAT (sibling of our FZQSAT (15)), which is an algorithm for evaluating quantified Boolean formulas. QBF is a lan- guage that extends
propositional logic
in such a way that many advanced forms of reasoning can be easily formulated and evaluated. ZQSAT is based on ZDD, which is a variant of BDD, and an adopted version of the DPLL algorithm. The program has been implemented in C using the CUDD package. The capability of ZDDs in storing sets of subsets efficiently enabled us to store the clauses of a QBF very compactly and led us to implement the
search algorithm
in such a way that we could store and reuse the results of all previously solved subformulas with few overheads. This idea along some other techniques, enabled ZQSAT to solve some standard QBF benchmark problems faster than the best existing QSAT solvers.
Conference:
Australian Joint Conference on Artificial Intelligence - AUS-AI
, pp. 681-693, 2004
DOI:
10.1007/978-3-540-30549-1_59
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
)
(
www.hpi.uni-potsdam.de
)
(
springerlink.metapress.com
)
(
www.informatik.uni-trier.de
)
More »
Citation Context
(4)
...To abstain from the CNF structure has also been proposed in BDD-based approaches (see, e.g., [
20
]), and for the solver QuBos [3] which eliminates one type of variables by expansion and numerous optimizations (including miniscoping), and then passes the resulting formula to a SAT solver...
...There are a few further solvers, namely QuBoS [3], boole6, and zqsat [
20
] in the literature, which...
Uwe Egly
,
et al.
A solver for QBFs in negation normal form
...Although we are in the first stages of our investigation, but learning from our previous experience [
7
], [8] we think employing a variant of BDD called ZDD can lead to more advantages...
Mohammad Ghasemzadeh
,
et al.
K-terminal Network Reliability Evaluation Using Binary Decision Diagra...
...zqsat [
16
], which also allow arbitrary QBFs as input, but rely on different techniques...
Uwe Egly
,
et al.
A Solver for QBFs in Nonprenex Form
...However, there are a few solver s which are able to handle arbitrary QBFs (e.g., [11,
14
]) and recent results [15,11] s how that non-normal form approaches are highly beneficial on certain instances...
Uwe Egly
,
et al.
Reasoning in Argumentation Frameworks Using Quantified Boolean Formula...
References
(14)
ZBDD-Based Backtrack Search SAT Solver
(
Citations: 16
)
Fadi A. Aloul
,
Maher N. Mneimneh
,
Karem A. Sakallah
Conference:
International Workshop on Logic & Synthesis - IWLS
, pp. 131-136, 2002
Graph-Based Algorithms for Boolean Function Manipulation
(
Citations: 5294
)
Randal E. Bryant
Journal:
IEEE Transactions on Computers - TC
, vol. C-35, no. 8, pp. 677-691, 1986
An Algorithm to Evaluate Quantified Boolean Formulae and Its Experimental Evaluation
(
Citations: 94
)
Marco Cadoli
,
Marco Schaerf
,
Andrea Giovanardi
,
Massimo Giovanardi
Journal:
Journal of Automated Reasoning - JAR
, vol. 28, no. 2, pp. 101-142, 2002
Multi-resolution on compressed sets of clauses
(
Citations: 47
)
Philippe Chatalic
,
Laurent Simon
Journal:
IEEE Transactions on Applications and Industry
, pp. 2-10, 2000
A Machine Program for Theorem Proving
(
Citations: 1542
)
Martin Davis
,
George W. Logemann
,
Donald W. Loveland
Journal:
Communications of The ACM - CACM
, vol. 5, no. 7, pp. 394-397, 1962
Order by:
Citations
(4)
A solver for QBFs in negation normal form
(
Citations: 6
)
Uwe Egly
,
Martina Seidl
,
Stefan Woltran
Journal:
Constraints - An International Journal - CONSTRAINTS
, vol. 14, no. 1, pp. 38-79, 2009
K-terminal Network Reliability Evaluation Using Binary Decision Diagram
Mohammad Ghasemzadeh
,
Christoph Meinel
,
Sara Khanji
Conference:
International Conference on Information and Communication Technologies: From Theory to Applications - ICTTA
, 2008
A Solver for QBFs in Nonprenex Form
(
Citations: 14
)
Uwe Egly
,
Martina Seidl
,
Stefan Woltran
Conference:
European Conference on Artificial Intelligence - ECAI
, pp. 477-481, 2006
Reasoning in Argumentation Frameworks Using Quantified Boolean Formulas
(
Citations: 6
)
Uwe Egly
,
Stefan Woltran
Conference:
Computational Models of Argument - COMMA
, pp. 133-144, 2006