The Decision Procedure Toolkit (DPT) includes a propositional
satisfiability solver and a satisfiability solver for the theory of
uninterpreted functions. The build system can produce native-code and
Objective Caml byte-code executable files for these solvers. In
addition, it can build a custom top-level with the DPT
libraries. The installation instructions
describe how to produce these. Instructions on how to use these
programs follow. (For byte-code versions of the solvers, substitute
Note that the solver executables are memory intensive on larger
benchmarks. We are yet to investigate this in detail, but it seems
that changing the OCaml garbage collection settings can have a
significant benefit. For example, increasing the size of the minor
heap appears to help. You can do that by adding the string
OCAMLRUNPARAM environment variable as follows before
running a solver.
OCAMLRUNPARAM="s=51200000"; export OCAMLRUNPARAM
setenv OCAMLRUNPARAM "s=51200000"
cnf_sat.opt [OPTION]... FILE
This solver accepts problem files in the DIMACS Challenge Satisfiability Suggested Format.
smtlib_solver.opt [OPTION]... FILE
This solver accepts problem files in the format described in The SMT-LIB Standard Version 1.2 (30 August 2006). The solver expects to find the logic and theory files for SMT-lib in:
These files can be downloaded via the logics and theories links from the SMT-LIB web site.
dpt_toplevel -I <path-to-dpt>/include
Starts an Objective Caml interpreter, with the DPT libraries loaded.Copyright © 2007 Intel Corporation