[SMT-LIB] [SMT-COMP] On QF_LIA benchmarks

[Clark Barrett]

Alberto,

Thanks--we are working on adding your benchmarks to SMT-LIB.  Regarding the
competition, generally all benchmarks (unless they are *very* easy) from
SMT-LIB are eligible for the competition, so yours will be no exception.
Benchmarks are selected according to the algorithm explained in the rules
document on the SMT-COMP web page.

It seems to me that these benchmarks should fall into the "crafted" category
(as opposed to "industrial" or "random").  Does that sound right to you?

-Clark 

> 
> 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
> 
> _______________________________________________
> SMT-COMP mailing list
> SMT-COMP at cs.nyu.edu
> http://cs.nyu.edu/mailman/listinfo/smt-comp
>