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 the current version Yices 2

Some important versions and a flag for Yices:



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

(benchmark test.smt
:logic QF_UFLIA
:extrafuns ((A Int) (B Int) (C Int) (D Int))
:formula (and
(> (* 2 A) (+ B C))
(> (* 2 B) (+ C D))
(> (* 2 C) (* 3 D))
(> (* 3 D) (+ A C))
))

yields as result:

sat
(= A 30)
(= B 27)
(= C 32)
(= D 21)



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

(benchmark test.smt
:logic QF_UFLIA
: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 3:
Calling
yices-sat -m test.d
where the file "test.d" consists of

p cnf 4 11
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

A few more examples are given in the slides.



Last change: November 16, 2015