Technische Universität München,
Fakultät für Informatik
Lehrstuhl Informatik IV
SEMPROP - A Decision Procedure for Quantified Boolean Formulas
Semprop is a decision procedure for Quantified Boolean Formulas (QBFs).
Semprop is based on the method of semantic trees, which is implemented a la
Davis, (Putnam), Logemann, and Loveland.
The system incorporates the standard techniques like unit propagation and
the purity rule, which are more powerful in the quantified Boolean case.
Furthermore, a dependency-directed backtracking mechanism and learning
features are integrated in the actual release.
There is a paper
R. Letz. Lemma and Model Caching in Decision Procedures for
Quantified Boolean Formulas
presented at TABLEAUX2002 describing the recent developments.
To run semprop in default mode, just type: semprop <problem_file>,
where <problem_file> is in
Rintanen's
format or in (slightly restricted)
qdimacs
format. Both formats are extensions of the dimacs format for
propositional formulae to QBFs. Semprop also accepts standard dimacs format
and may be used as a (non-optimized) SAT solver.
Executables (save and chmod +x):
semprop010604 (actual release):
Linux.
This release is almost as semprop240202 (see below),
but the -lemma option
is the default, in order to switch it off type -nolemmas.
Note: for very large inputs, before calling semprop say: limit stacksize
unlimited (this may be necessary, because the main semprop loop is recursive).
This version of semprop is the first which also accepts (slightly restricted)
qdimacs
format (the restriction is that all variables in the clauses must occur
in the prefix and only the quantifiers 'e and 'a must occur).
Example (in Rintanens format):
The QBF: Ax Ey Ez Eu ( (x or y) and (-x or -z) and (-u or z) ) is written as:
p cnf 4 3 # header: 4 variables, 3 clauses
q 0 # alternating quantifier prefix: must always
q 1 0 # start with a (possibly empty) sequence of
q 2 3 4 0 # existential variables; 0 is separator
1 2 0 # clauses; 0 is separator
-1 -3 0 #
-4 3 0 #
In order to get some information about the parameters of the system,
just type: semprop without any arguments.
Remark: for problems with more than 2^16 variables it might be necessary to increase the
stacksize (e.g. limit stacksize 16384 or 32768) before running semprop, since
the system uses recursion for building the semantic tree.
Older releases:
semprop190301 (first release):
Sun Solaris,
Linux.
Limitations and bugs: variable number limited to 65536, clauses in the input without
existential variables lead to error, clause length is limited to 1000 literals.
semprop260601:
Sun Solaris ,
Linux.
This release has the mentioned limitations and bugs of the previous release
removed;
furthermore, a new pruning technique called sign abstraction
is incorporated which is used by default,
to switch it off (for compatibility with semprop190301)
type: semprop -true-clauses 0 <problem_file>;
finally, the output format is changed from
satisfiable/unsatisfiable to true/false.
semprop240202:
Sun Solaris ,
Linux.
This release is as semprop260601, but has learning for false subgoals
integrated, ie, the feature called lemmas in the paper above;
furthermore, the atom selection function was slightly changed).
In order to use the lemma feature, type: semprop -lemmas
<problem_file>
Some examples of input files:
A test example (should be satisfiable (true))
CHAIN12v.13 ,
CHAIN13v.14 ,
BLOCKS3iii.5
(from Rintanen's collection)
A class of very small false formulae, which are hard for tree-based (but not for
resolution-based) QBF procedures:
tree-exa2-10,
tree-exa2-15,
tree-exa2-20,
tree-exa2-25,
tree-exa2-30,
tree-exa2-35,
tree-exa2-40,
tree-exa2-45,
tree-exa2-50.
A class of very small true formulae, which are hard for QBF procedures:
tree-exa10-10,
tree-exa10-15,
tree-exa10-20,
tree-exa10-25,
tree-exa10-30.