The tool Yices

The tool Yices is a program for satisfiability modulo theories (smt). It accepts smt format, but can also be used as a boolean SAT solver accepting dimacs format.

On the homepage of Yices you find documentation and download instructions.

The examples and flags indicated below apply for Yices, not for Yices 2

Some important flags for Yices:

• -smt means that the standard smt format is used, as described in SMT-LIB Standard
• -d means that dimacs format is used, as in the dimacs format for the SAT Competition
• -e means that in case of satisfiability the satisfying assignment is given

Example 1:
Calling
yices -e -smt test.smt
where the file "test.smt" consists of

(benchmark test.smt
:extrafuns ((A Int) (B Int) (C Int))
:formula
(and
(= A 987654323456789)
(= B (* 99 987654323456789))
(= C (+ A B))
))

yields as result:

sat
(= A 987654323456789)
(= B 97777778022222111)
(= C 98765432345678900)


Example 2:
Calling
yices -e -smt test.smt
where the file "test.smt" consists of

(benchmark test.smt
:extrafuns ((A Int Int))
:formula
(and
(= (A 1) 1)
(= (A 100) 2)
(forall (?i Int) (= (A ?i) (A (+ ?i 1))))
))

yields as result: "unsat"

Example 3:
Calling
yices -e -d test.d
where the file "test.d" consists of

p cnf 4 15
1 2 3 0
1 -3 4 0
1 -2 3 4 0
1 -2 -3 -4 0
-1 2 3 4 0
-1 2 -4 0
-1 2 -3 4 0
-1 -2 3 4 0
-2 3 -4 0
-1 -2 -3 4 0
-1 -2 -3 -4 0

yields as result:

sat
-1 -2 3 4



Last change: September 5, 2011