[SMTCOMP] Sudoku based instances

[Paulo J. Matos]

On 27/04/06, Bruno Dutertre <bruno at csl.sri.com> wrote:
> Hyondeuk.Kim at colorado.edu wrote:
> > Yeah, I think they are interesting.
> >
> > Hyondeuk
> >
>
> Well, I'm not so sure these kinds of puzzles are particularly
> relevant to SMT:

In fact I don't think they are relevant for the SMT Competition...
I've sent the email initially to know if would be interesting for
anyone in this mailing list.

> - they can be encoded as a big conjunction (no Boolean structure).

Indeed, I agree with you although we can also make the encoding as
complex as we wish adding additional redundant information. Still, the
benchmarks were generated to test my solver and not to make
interesting benchmarks.

> - they do not require combination of decision procedures

That's not really a problem, right? IDL doesn't require a combination
of decision procedures. Only a Boolean enumerator and a decision
procedure for difference constraints are needed.

> - they are probably easy to solve using CSP or pure Boolean
>    SAT techniques and encoding them in arithmetic is likely
>    to be much less efficient. I doubt anybody who really cares
>    about solving Soduku (if such a person exists) would think
>    of using SMT solvers for it.

I don't think people use solvers, be it CSPs or SAT solvers, in the
daily life to solve sudoku anyways. As I said they were interesting at
least for me because I can make them as hard as I want and test not
only the performance of the solver but also its memory usage and its
data structures.

>
> Because of this, I don't think performance of an SMT solver
> on Sudoku is likely to tell us a lot about performance of the
> same solver on more realistic applications (e.g., verification
> problems).

Agree, but not all examples in SMTCOMP are 'realistic' anyways.

> We should try to evaluate SMT solvers on problems that
> require decision procedures, not on problems that can be solved
> faster/better using other methods.
>

Indeed! Probably I was misunderstood, I don't think they should be
used for SMT Solver comparison or evaluation or even to be used for
sudoku solving. Just though someone might be interested in them just
for hobby, testing or any other non-pratical motif.

Anyway, I agree with you when you say that they are not useful for the
competition. :)

Cheers,

Paulo Matos

> Bruno
>
>
> > Quoting "Paulo J. Matos" <pocmatos at gmail.com>:
> >
> >
> >>Hi all,
> >>
> >>I have generated some sudoku based instances. Would those be
> >>interesting for SMTCOMP?
> >>Want me to send them in?
> >>
> >>Cheers,
> >>--
> >>Paulo Jorge Matos - pocm at sat inesc-id pt
> >>Web: http://sat.inesc-id.pt/~pocm
> >>Computer and Software Engineering
> >>INESC-ID - SAT Group
> >>
> >
> >
> >
> --
> Bruno Dutertre                             | bruno at csl.sri.com
> CSL, SRI International                     | fax: 650 859-2844
> 333 Ravenswood Avenue, Menlo Park CA 94025 | tel: 650 859-2717
>
>


--
Paulo Jorge Matos - pocm at sat inesc-id pt
Web: http://sat.inesc-id.pt/~pocm
Computer and Software Engineering
INESC-ID - SAT Group