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

[Hyondeuk.Kim@colorado.edu]

Hello,

I think I did not reply to all. This is what I replied to Roberto.
I submitted Queens benchmark since it is interesting to know how difference
logic solver handles the problem with many disequality constraints. As you
know,  in QF_IDL, each benchmark set has its own feature. For example, the
diamond benchmark makes the solver to check every diamonds for feasibility, and
the mathsat benchmark makes the solver hardly call the theory solver. As I said,
the purpose of the queens benchmark is to check how the solver handles the
diseqaulity constraints. Therefore, I think it is still interesting to leave
Queens benchmarks in SMT COMP.

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