Usage

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 “.byte” for “.opt”.)

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 “s=<minor-heap-size>” to the OCAMLRUNPARAM environment variable as follows before running a solver.

Bourne Shell

OCAMLRUNPARAM="s=51200000"; export OCAMLRUNPARAM

C Shell

setenv OCAMLRUNPARAM "s=51200000"

DPLL-based SAT solver for DIMACS CNF files

Usage

cnf_sat.opt [OPTION]... FILE

Exit status

0

if satisfiable

1

if unsatisfiable

Options

-v n

Verbosity, default is 1

This solver accepts problem files in the DIMACS Challenge Satisfiability Suggested Format.

Solver for SMT-LIB files

Usage

smtlib_solver.opt [OPTION]... FILE

Exit status

0

if unsatisfiable

1

if satisfiable

100

if unexpected status

101

if unsupported logic

Options

-v n

Verbosity, default is 1

-l path-to-smt-lib

Path to SMT-LIB libraries, default is “.”

-q

Top level equality propagation, default is false

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:

• <path-to-smt-lib>/theories/
• <path-to-smt-lib>/logics/

These files can be downloaded via the logics and theories links from the SMT-LIB web site.

DPT custom top-level

Usage

dpt_toplevel -I <path-to-dpt>/include

Starts an Objective Caml interpreter, with the DPT libraries loaded.

Hosted by the ^* web site.
^*Other names and brands may be claimed as the property of others.