[SMT-LIB] On QF_LIA benchmarks
Cesare Tinelli
tinelli at cs.uiowa.edu
Mon Apr 21 13:50:15 EDT 2008
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
More information about the SMT-LIB
mailing list