# [SMT-LIB] On QF_LIA benchmarks

Alberto Griggio alberto.griggio at disi.unitn.it
Sat Apr 19 12:46:32 EDT 2008

``` Hello list,

We're writing this email to raise an issue about the current benchmarks
in the QF_LIA logic. In essence, most of the unsatisfiable ones are
still unsatisfiable even when interpreted over the reals. With the new
SMT-COMP approaching, we think this is very undesirable: with very few
benchmarks that really require reasoning on the integers, it's very
difficult to assess the strenghts and weaknesses of current SMT solvers
on integer arithmetic.

As a first contribution in the direction of addressing this issue,
we're proposing a new set of benchmarks which are not affected by this
problem. Essentially, they encode associativity properties like:

a + 2*b + 4*c + 8*d = a + 2(b + 2(c + 2d))

on arithmetic modulo 2^n, for different values of n and different
numbers of variables. Addition and Multiplication modulo 2^n were
encoded with two different techniques:

1. Using "sigmas" as in [1]. For example, 4*b in arithmetic modulo
16 is encoded as (4*b - 16*sigma) with constraints (0 <= sigma < 4),
where sigma is a fresh integer variable

2. Using nested ITEs. For example, 4*b in arithmetic modulo 16 would be
ITE(4 * v2 < 16,
4 * v2 ,
ITE(4 * v2 < 32,
4 * v2 - 16,
ITE(4 * v2 < 48,
4 * v2 - 32,
ITE(4 * v2 < 64,
4 * v2 - 48,
4 * v2 - 64 ))))

We're attaching a tarball with some instances (we can generate more if
needed), hoping that they will be added to the library and to the pool
for the competition.

Each benchmark "ring_2expN_Mvars_Kite_unsat.smt" has been generated
according to the following parameters:
- N is the number of bits of the modulo (2^N)
- M is the number of variables in the expression
- K is the number of multiplications that were encoded with nested ITEs
(instead of sigmas). Notice that this parameter controls the trade-off
between "integer search" and "boolean search": if all multiplications
were encoded as ITEs, the problem would be unsatisfiable also on the
reals.

Alberto, Alessandro, Anders and Roberto

[1] Raik Brinkmann and Rolf Drechsler, RTL-Datapath Verification using
Integer Linear Programming, 2002.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: rings.tar.gz
Type: application/x-gzip
Size: 365772 bytes
Desc: not available
Url : /pipermail/smt-lib/attachments/20080419/3244d7f5/rings.tar-0001.bin
```