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:

- the version yices-smt is an SMT solver accepting the standard smt format (SMT-LIB version 1.2), as described in SMT-LIB Standard,
- the version yices-sat is a pure SAT solver accepting dimacs format, as in the dimacs format for the SAT Competition,
- the flag -m means that in case of satisfiability the satisfying assignment is given.

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)

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)

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