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

[Roberto Sebastiani]

Hi Hyondeuk

I'm at ease with SMT(QF_IDL) problems with many disequalities.
The problem is that n-queens are *CSP* problems with many disequalities!

As I said below, the risk with this kind of problems is that,
(unlike diamonds & mathsat/fischer suites) 
these problems have a recognizable structure, so that 
ad hoc solutions can be adopted for the competition.

Roberto

PS: As far as the diamonds & mathsat/fischer suites are concerned,
  I'm open to discuss the opportunity of dropping them as well 
if anybody proposes it.



On Fri, 7 Jul 2006, Hyondeuk.Kim at colorado.edu wrote:

> Hello Roberto,
>
> I submitted this benchmark since it is interesting to know how difference logic
> solver handles the problem with many disequalities.
>  I think each set of SMT
> benchmarks in QF_IDL has a different feature. For example, diamond suite makes
> the solver to check every diamond for feasibility, mathsat suite hardly makes
> the solver to call theory solver. As I mentioned, the purpose of the queens
> benchmark is to check how the solver handles the disequality constraints.
> Therefore, I think it is still interesting to leave some queens benchmarks in
> the SMT competition.
>
> Thank you.
>
> Hyondeuk
>
> Quoting Roberto Sebastiani <rseba at dit.unitn.it>:
>
>> 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
------------------------------------------------------------------