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

[Hyondeuk.Kim@colorado.edu]

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