[SMT-LIB] On QF_LIA benchmarks

[Alberto Griggio]

 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