[SMTCOMP] Sudoku based instances

[Bruno Dutertre]

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:
- they can be encoded as a big conjunction (no Boolean structure).
- they do not require combination of decision procedures
- 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.

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

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