Sat Solvers.

Fahiem Bacchus, University of Toronto

The following software is available:

  1. 2clseq-A DPLL Solver Using Extensive Binary Clause Reasoning

  2. HypBinRes Preprocessor

  3. NoClause DPLL solver that solves non-clausal theories.

Before you download please be aware of the following legal restriction on the use of the software.

Legal Matters

The software available at this site is copyright (c) 1994-2002 Fahiem Bacchus. All rights are reserved. Use of this software is permitted for non-commercial research purposes, and it may be copied only for that use. All copies must include this copyright message. This software and any documentation and/or information supplied with it is distributed on an as is basis. Fahiem Bacchus and the University of Toronto make no warranties, express or implied, including but not limited to implied warranties of merchantability and fitness for a particular purpose, regarding the documentation, functions or performance of such software, documentation and/or information.

If you would like to use any of this software for commercial purposes, please contact the author.

1. 2clseq-A DPLL Solver Using Extensive Binary Clause Reasoning

2clseq is a DPLL SAT solver that utilizes extensive reasoning with the binary clause subtheory at every node of the search tree. Since this reasoning is performed dynamically many more opportunities arise as we descend the search tree. In particular, as literals are valued and clauses reduced many new binary clauses are produced.

2clseq displays very impressive performance. It is competitive with the state of the art SAT solvers (state of the art in 2002). Interesting, with very few exceptions these other solvers utilize only unit propagation at each node of the search tree, avoiding any more complex forms of reasoning. In fact, prior to 2clseq there has never been any convincing evidence that more reasoning at each node could payoff in terms of improved performance.

The following two papers describe the approach.

  1. Enhancing Davis Putnam with Extended Binary Clause Reasoning, F. Bacchus, National Conference on Artificial Intelligence (AAAI-2002) to appear, 2002.
    This paper presents the basic ideas that are the foundation of the 2clseq system.
  2. Exploring the Computational Tradeoff of more Reasoning and Less Searching, F. Bacchus, Fifth International Symposium on Theory and Applications of Satisfiability Testing, pages 7-16, 2002.
    This paper presents some additional empirical data, and discusses the issue of how much search can be saved by doing more reasoning.

Download the 2clseq Software here (tar file with sources as well as prebuilt Linux executable).

Some more information about the software:

2clseq is written in C++ (using C++ as an improved version of C rather than the object oriented nightmare that it can easily mutate to). It should compile on almost any machine (including under Windows using Visual C++). This is version 2.0, it is the version that was entered in the SAT2002 SAT solvers competition. Check the competition web site for information about how well 2clseq performed. Version 2.0 features

  1. Binary Clause resolution, detection of hyper-resolvants, and equality reduction (as described in my AAAI2002 paper linked above).
  2. Intelligent backtracking via detection of conflicts.
  3. 2nd order relevance bounded clause learning which facilitates a low overhead implementation.
  4. Five Heuristics:
    1. "-h 0" Lexographic variable ordering.
    2. "-h 1" MOMs, variable with largest number of active 2 clauses break ties by number of active 3-clauses.
    3. "-h 2" Like 1, but chooses among tied variables randomly (random tie breaking works well).
    4. "-h 3" Estimates the number of new 2-clauses that would be produced, and picks variable that would generate the largest number of new 2-clauses. (Best for random problems.)
    5. "-h 4" The heursitic used in the competition. Like 2 but does small amount of lookahead to see if it can detect a few more new binary clauses.
    6. "-h 5" Like 3 except uses a TABU list to ensure that the same variable is not always instantiated at the same level.

    As far as I can tell from my experiments, use "-h 4" for non-random problems and "-h 3" for random problems.

  5. A pacifier. As a rough estimate of how much progress the search is making, the pacifier rate can be set with "-pcr K". Then every K nodes of the search tree the highest level it backtracked to and the deepest level the search reached during last K nodes is printed. (If the search is spending most of its time at a very deep level of the search tree odds are it won't finish anytime soon.)
  6. Statistics Log file. The file "timetable.dat" contains one line for every problem run. The line is a comma separated list of the following numbers:
    1. input file name
    2. [0,1,-1]: 0=UNSAT, 1=SAT -1=UNKNOWN
    3. total CPU seconds used
    4. CPU seconds used to do initial processing
    5. number of nodes searched (calls to DPLL)
    6. number of terminal nodes visited (leaves)
    7. fraction of times a hyper-resolvant was found amoung the times one was searched for.
    8. number of hyper-resolvants found
    9. number of times a hyper-resovant was searched for
    10. number of pure literals reduced
    11. number of literal equalities found
    12. number of clause subsumptions found (in initial processing).

2. Hypre Preprocessor Software

The Hyper binary resolution + equality reduction inference used inside of 2clseq has been implemented in a preprocessor. The preprocessor often does a rather remarkable job of simplifying formulas, working best on structured formulas. The following paper describes the approach (which is quite different from the approach used in 2clseq)

 

Download the hypre software here (tar file with C++ sources).
Executables here (tar file with prebuilt Linux executables).

Some more information about the software.

  1. hypre the preprocessor itself. By default when run with an input file "foo.cnf" produces the output file "foo_out.cnf". Each run adds a data line to "preprocessor.dat". The fields of this file are: input file name, solution status (with 0 = UNSAT, 1 = SAT, -1 = UNRESOLVED by the preprocessor), original number of variables. The output file "foo_out.cnf" contains a mapping of the original variables. The mapping specifies what happened to each of the original variables (whether or not they became true or false, disappeared from the theory, or were made equal to some other variable). The mapping is specified as a set of comment lines at the top of the DIMACS formatted "foo_out.cnf". With the mapping one can map solutions of the perprocessed formula  to solutions of the original formula. Some software along these lines is provided as the next two items.
  2. modelcheck takes a file containing a v-line (a solution in the format used by the SAT competition: a line starting with a 'v' followed by a list of the true literals terminated by 0) and a .cnf file and determines whether or not the solution specified by the v-line satisfies the .cnf theory.
  3. vline takes as input a file containing a v-line, and a file output by the preprocessor (a *_out.cnf file) and generates a file containing a new v-line. The new v-line should be a solution to the original *.cnf file. This is accomplished by using the map placed in the *_out.cnf file by the preprocessor. By
    1. running the preprocessor on an original cnf file foo.cnf one obtains foo_out.cnf, a simplified cnf file.
    2. solving foo_out.cnf and placing the v-line solution (dependent on the solver one might need to edit its output) in an output file foo.vline
    3. running v-line on foo.vline to get vline.out
    4. running modelcheck on vline.out and foo.cnf

    one can check that the solution to the preprocessed file correctly maps to a solution to the original cnf theory.

3. NoClause DPLL solver that solves non-clausal theories.

The following paper describes the approach:

Download the NoClause software here (gzipped tar file with C++ sources). This is a slighly modified version that fixes some bugs. The modifications were made by Paul Tyler of NICTA.

Download the fvp-unsat.2.0-iscas problem suite.

This suite is due to M. Velev. It demonstrates the ISCAS format NoClause can take as input. NoClause can also solve any of the other ISCAS format suites from Velev's benchmark site.
To my home page.