[SMTCOMP] IMPORTANT: the infinite-precision issue

[Leonardo de Moura]

Aaron, Clark and I have the following position on the subject:

1) The theories are exactly as stated. This means solvers should
support multi-precision arithmetic or they risk being incomplete,
or even unsound if they do not detect under and overflows.
If someone wants to propose a new theory or logic that limits
  the size of integers, they are free to do so.

2) We collect the best benchmarks we can based on real problems.
We don't think we should fill our benchmark pool with artificial  
problems
in order to bias the results towards certain kinds of solvers.
Moreover, we already have several benchmarks in QF_LIA (CIRC)
and QF_LRA (clock_synchro) that require multi-precision arithmetic.
At least in the algorithm I use, one cannot express intermediate results
using an integer or a pair of integers for rationals.

3) We publish the benchmarks and the criteria for choosing the  
competition
benchmarks.  Everyone has the same information. And, everybody
was welcome to submit benchmarks to the competition.

That said, we will enforce that (where applicable) each division  
contains
at least one benchmark that requires bignums, kind of like we did with
integers last year.  That way, people have some incentive to move to
multi-precision arithmetic.

So, in the next revision of the benchmark library, we will include  
one benchmark
that requires bignums to the following divisions: QF_IDL, QF_RDL,  
QF_UFIDL,
QF_UFLIA, and QF_AUFLIA.

Best wishes,
Leonardo
for Aaron and Clark, too.

On Jun 8, 2006, at 1:17 AM, Roberto Sebastiani wrote:

> Hi all.
> I think the discussion has gone a little far from the original  
> issue I raised.
> Thus, let me do one step back.
>
> (First, Leonardo, notice that we're perfectly at ease with the idea  
> of incomplete solvers, but this was not intended to be the issue of  
> my email.)
>
> My issue was: we WANT CLEAR RULES ABOUT INFINITE PRECISION.
>
> That is, for each category, either:
> 1) we state that infinite precision is required, and we add a  
> significant
> amount of "critical" problems (which may cause wrong solution if  
> plain finite
>  precision is used), or
> 2) we state that infinite precision is *not* required, and we include
> no such critical problem.
>
> In the first case, each tool is guaranteed againts unfair  
> comparisions with
> non-infinite-precision tools. In the second case, one can safely  
> release infinite precision to that to have a fair competition with  
> non-infinite-precision tools.
>
> Notice that we're not pushing for either direction: we're simply  
> pushing for clear rules.
>
> Roberto
>
> PS: as far as Cesare's proposal is concerned, I agree with the  
> arguments of Paulo Matos. Moreover, from a practical perspective, I  
> think this would add a lot of extra workload in estabilishing the  
> ranges and/or ask the authors.
> (BTW: who guarantees that the authors of the problems are right?).
>> From a more principled perspective, I don't like the idea of  
>> customizing tools for
> single instances, or of adopting tricks like
> "if infty run mathsat_infty else if 32 run mathsat_32 else run  
> mathsat_64".
>
>
>
>
>
>
>
>
> On Tue, 6 Jun 2006, Leonardo de Moura wrote:
>
>> Hi Roberto,
>>
>> This is a good point.
>>
>>> there is an important question about SMT-COMP which apparently  
>>> nobody asked so far: do we explicitly require infinite precision  
>>> from SMT solvers on arithmetic-related theories? (I.e., RDL/IDL/ 
>>> LAR/LAI and combinations.)
>>
>> I believe one needs to use multi precision arithmetic for solving  
>> some problems in
>> LRA and LIA, but I agree with you that the benchmarks in RDL and  
>> IDL do not
>> require infinite precision.
>>
>> I'm not sure if we should force/require people to use multi  
>> precision arithmetic.
>> I think it is perfectly ok to use fixed precision, and return  
>> "unknown"
>> when an overflow/underflow is detected.
>>
>> I also believe it is perfectly ok to enter an incomplete solver,  
>> and return
>> "unknown" for formulas you know your solver is incomplete.
>> For example, Aaron Stump did that last year. CVC is not complete
>> for integers, and he returned "unknown" for potential "sat"  
>> instances.
>>
>> Anyway, I really interested in knowing what the rest of the SMT  
>> community
>> thinks about this issue.
>>
>>> On the one hand, infinite precision prevents an SMT tool from
>>> giving wrong answers on some problems. On the other hand, using  
>>> infinite precision significantly slows down the performances  
>>> (around a 3 factor in our experience).
>>
>> In my experiments, I noticed a 1.4 factor. I'm using GMP  
>> (www.swox.com/gmp/)
>> for infinite precision. I guess you are using it too. :-)
>> We found that memory management can be expensive with GMP, and a  
>> good trick
>> is to create a pool of GMP numbers and reuse them for intermediate  
>> computations.
>>
>> Cheers,
>> Leonardo.
>>
>>
>
> -- 
> ------------------------------------------------------------------
> Prof. ROBERTO SEBASTIANI
> Dip. Informatica e Telecomunicazioni
> Fac. Scienze M.F.N., Universita` di Trento    Tel: +39 0461 881514
> Via Sommarive 14, I-38050, Trento, Italy      Fax: +39 0461 882093
> roberto.sebastiani at dit.unitn.it     http://www.dit.unitn.it/~rseba
> ------------------------------------------------------------------