Lehrstuhl Informatik IV

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.

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:

Some examples of input files:

For other examples and other QBF procedures, see QuBE, QSOLVE , or Rintanen's page . Finally, there is a web page QBFLIB at the University of Genova devoted to numerous aspects of QBF solving.