[SMTCOMP] About the QF_IDL "n-queens" problms

[Roberto Sebastiani]

Hi Leonardo,
see my answer to Hyondeuk. MOreover:

On Fri, 7 Jul 2006, Leonardo de Moura wrote:

> Dear Roberto,
>
> We are aware of the problem. The n-queens benchmarks were marked
> as crafted. The benchmark selection algorithm uses the following
> distribution: 85% industrial, 10% crafted, 5% random.
> In our simulations, only 4 queens problems were selected.

Well, 4 problems are well enough to reshape the whole result,
in particular on QF_IDL. E.g., last year:

TOOL                 #SOLVED
BarcelogicTools 	47 
Yices 			47 
MathSat 		46 
Ario 			43

Roberto

> You can find more information about the benchmark selection
> algorithm at:
> http://www.csl.sri.com/users/demoura/smt-comp/bench_selection.shtml
>
> Cheers,
> Leonardo
>
>
> On Jul 7, 2006, at 10:00 AM, Roberto Sebastiani wrote:
>
>> Dear colleagues,
>> 
>> Let me raise one more point, about "n-queens" problems in the QF_IDL 
>> benchmark suite. (I apologize for doing it only now, but we noticed this 
>> fact
>> only recently.)
>> 
>> 297 out of 893 total benchmarks in QF_IDL  are "n-queens".
>> It seems to us they are all "pigeonhole-style" problems:
>> 
>> 1. { x_i != x_j }_{ij}
>> 2. { x_i=value_{i_1} | x_i=value_{i_2} | ... | x_i=value_{i_K} }_i
>> 
>> which are encoded into QF_IDL as
>> 
>> 1.1. { x_i != x_j }_{ij}
>> 2.1. { {i_1}  <= x_i-zero <= i_K }_i
>> 
>> ("zero" being one variable representing zero).
>> 
>> Thus, they are FULLY-COMBINATORIAL CSP PROBLEMS disguised as SMT(QF_IDL) 
>> problems, and have hardly anything to do with QF_IDL.
>> In fact, no  arithmetical property should be exploited to solve these 
>> problems.
>> (Notice, e.g., that the actual values of the constants value_{i_j}'s are 
>> irrelevant: the only relevant fact is weather they are pairwise equal or 
>> different. Thus. "-" and ">=" have no effective mathematical meaning here.)
>> 
>> We believe this is against the spirit of SMT-COMP.
>> Moreover, these are the kind of problems which may push people to customize 
>> "ad hoc" solutions for the competition.
>> 
>> Thus, we believe these problems should be dropped from the list.
>> 
>> Roberto
>> 
>> 
>> -- 
>> ------------------------------------------------------------------
>> 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
>> ------------------------------------------------------------------

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