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.

    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.