[SMTCOMP] About the QF_IDL "n-queens" problms
Roberto Sebastiani
rseba at dit.unitn.it
Fri Jul 7 13:00:03 EDT 2006
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
------------------------------------------------------------------
More information about the SMT-COMP
mailing list