[SMT-LIB] On QF_LIA benchmarks

[Cesare Tinelli]

Dear Alberto and all,

thanks a lot for your contribution to SMT-LIB. The benchmarks will be  
added to the library soon, after we run our validation checks on  
them. Clark will contact you directly for more benchmarks, as needed.

Best,


Cesare


PS: The decision of including any SMT-LIB benchmark into SMT-COMP is  
governed by the competition's rules and policy, and is up to its  
organizers. So I will let them respond about that.



On Apr 19, 2008, at 11:46 AM, Alberto Griggio wrote:

>  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.<rings.tar.gz>_______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib