[SMTCOMP] IMPORTANT: the infinite-precision issue

[Roberto Sebastiani]

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
------------------------------------------------------------------