forked from lonsing/depqbf
-
Notifications
You must be signed in to change notification settings - Fork 0
DepQBF, a solver for quantified boolean formulae (QBF).
License
hmarkus/depqbf
Folders and files
| Name | Name | Last commit message | Last commit date | |
|---|---|---|---|---|
Repository files navigation
July 2012
-------------------
GENERAL INFORMATION
-------------------
This is version 1.0 of the search-based QBF solver DepQBF. Compared to the
previously released version 0.1, it includes the following major changes:
- Some code maintenance and bug fixes
- Blocking literals to improve cache performance
- Trace generation (contributed by Aina Niemetz): DepQBF 1.0 can produce
traces in QRP format (ASCII and binary version of the QRP format are
supported; see also usage information). If called with the '--trace' option,
the solver prints *every* resolution step during clause and cube learning to
<stdout>. The output format is QRP ("Q-Resolution Proof"). For example, the
call './depqbf --trace input-formula.qdimacs > trace.qrp' dumps the trace
for the QBF 'input-formula.qdimacs' to the file 'trace.qrp'. The generated
trace file can be used to extract a certificate of (un)satisfiability of the
given formula using additional tools. See also the website
'http://fmv.jku.at/cdepqbf/' and our tool paper at SAT'12:
@inproceedings{DBLP:conf/sat/NiemetzPLSB12,
author = {Aina Niemetz and
Mathias Preiner and
Florian Lonsing and
Martina Seidl and
Armin Biere},
title = {Resolution-Based Certificate Extraction for QBF - (Tool
Presentation)},
booktitle = {SAT},
year = {2012},
pages = {430-435},
ee = {http://dx.doi.org/10.1007/978-3-642-31612-8_33},
crossref = {DBLP:conf/sat/2012},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
- The solver can be used as a library. The API is declared in file 'qdpll.h'
and file 'qdpll_app.c' demonstrates how it can be used. Note that the API,
apart from basic use, has not yet been thoroughly tested.
DepQBF is free software released under GPLv3. See also file
COPYING. Unfortunately, documentation is scarce and the code structure is not
as readable as it should be to allow for easy modifications. Please do not
hesitate to contact Florian Lonsing (see below) for any questions related to
DepQBF.
DepQBF consists of a dependency manager (file 'qdpll_dep_man_qdag.c') and a
core QDPLL solver (file 'qdpll.c'). During a run the solver queries the
dependency manager to find out if there is a dependency between two variables,
say 'x' and 'y'. Given the original quantifier prefix of a QBF, there is such
dependency if 'x' is quantified to the left of 'y' and 'x' and 'y' are
quantified differently. In contrast to that simple approach, DepQBF (in
general) is able to extract more sophisticated dependency information from the
given QBF. It computes the so-called 'standard dependency scheme' which is
represented as a compact graph by the dependency manager.
If you are interested only in the core solver based on QDPLL then it is
probably best not to look at the code of the dependency manager in file
'qdpll_dep_man_qdag.c' at all but only consider file 'qdpll.c'.
------------
INSTALLATION
------------
Unpack the sources into a directory and call 'make'. This produces optimized
code without assertions (default).
Note: set the flag 'FULL_ASSERT' in file 'qdpll_config.h' from 0 to 1 to
switch on *expensive* assertions. The solver will run *substantially* slower
in this case. As usual, the compiler flag 'DNDEBUG' removes all assertions
from the code, regardless from the value of 'FULL_ASSERT'.
-----------------------
CONFIGURATION AND USAGE
-----------------------
Call './depqbf -h' to display usage information. Further, undocumented command
line parameters can be found in function 'qdpll_configure(...)' in file
'qdpll.c'.
The solver returns exit code 10 if the given instance was found satisfiable and exit
code 20 if the instance was found unsatisfiable. Any other exit code indicates
that the instance was not solved.
Parameter '-v' enables basic verbose mode where the solver prints information
on restarts and backtracks to <stderr>. More occurrences of '-v' result in
heavy verbose mode where information on individual assignments is
printed. This can slow down the solver considerably and should be used for
debugging only.
Trace generation can be enabled by parameter '--trace'. Note that printing the
tracing information causes I/O overhead and might slow down the
solver. Writing traces in binary QRP format (enabled by parameter
'--trace=bqrp') usually produces smaller traces, as far as byte size is
concerned.
Calling DepQBF without command line parameters results in default behaviour
which was tuned on instances from QBFLIB. For performance comparisons with
other solvers it is recommended not to pass any command line parameters to
DepQBF.
By default, statistical output is disabled. To enable statistics, set the flag
'COMPUTE_STATS' in file 'qdpll_config.h' from 0 to 1. Similarly, time
statistics can be enabled by setting flag 'COMPUTE_STATS'.
----------
REFERENCES
----------
A system description appeared in JSAT:
@article{DBLP:journals/jsat/LonsingB10,
author = {Florian Lonsing and
Armin Biere},
title = {DepQBF: A Dependency-Aware QBF Solver},
journal = {JSAT},
volume = {7},
number = {2-3},
year = {2010},
pages = {71-76},
ee = {http://jsat.ewi.tudelft.nl/content/volume7/JSAT7_6_Lonsing.pdf},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
-------
CONTACT
-------
For comments, questions, bug reports etc. related to DepQBF please contact Florian Lonsing.
See also http://www.kr.tuwien.ac.at/staff/lonsing/ and http://fmv.jku.at/depqbf/.
About
DepQBF, a solver for quantified boolean formulae (QBF).
Resources
License
Stars
Watchers
Forks
Packages 0
No packages published
Languages
- C 97.8%
- Java 1.6%
- Other 0.6%