[SMTCOMP] Sudoku based instances

[Hyondeuk.Kim@colorado.edu]

I believe there are a lot of disequality constraints in Sudoku problem. It is
interesting to check how SMT solver deals with instances that are rich in
disequalities. It is true that Sudoku problem can be encoded as a big
conjunction. In fact, all difference logic problem can be encoded as a Boolean
formula using finite instantiation. I think Sudoku problem is a good starting
example to check how the solver deals with a lot of disequalities. There can be
more interesting benchmark with more complex boolean structure rich in
disequalities, for example, scheduling problem.

Thanks,

Hyondeuk


Quoting "Paulo J. Matos" <pocmatos at gmail.com>:

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