[SMTCOMP] IMPORTANT: the infinite-precision issue

[Cesare Tinelli]

Hi Roberto,

I second your request for clear rules. And I leave it to the SMT-COMP 
organizers to establish what those should be.
Here, I just have a couple of comments about your email.

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.
 >
I do agree with that of course, but I'm not sure how much less work 
there is in your proposal 1) above.
Adding a significant number of critical problems to a division would 
require the ability to choose them from an even greater pool. Wouldn't 
identifying or generating problems for this pool require a similar 
amount of work as well?


> (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".
> 
Fair enough. But I find it puzzling to hear this from a main MathSAT 
developer. Isn't MathSAT's layered approach based exactly on the 
principle of using the right (sub)solver for each specific input 
(sub)problem? How would this be different?

Cheers,


Cesare



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