[SMT-LIB] job-shop satisfiable instances

[Roberto Bruttomesso]

Dear SMT-COMP Organizers,

during the tuning of the latest version of MathSAT we realized
that we are able to solve 6 job-shop (satisfiable) instances whose
status is currently set as "unknown"

QF_IDL/job_shop/jobshop18-2-9-9-2-4-9.smt
QF_IDL/job_shop/jobshop26-2-13-13-2-4-9.smt
QF_IDL/job_shop/jobshop30-2-15-15-2-4-9.smt
QF_IDL/job_shop/jobshop38-2-19-19-4-4-12.smt
QF_IDL/job_shop/jobshop52-2-26-26-4-4-12.smt
QF_IDL/job_shop/jobshop60-2-30-30-2-4-12.smt

We are able to produce a model for each instance,
and we have verified their consistency by putting the
model in conjunction with the original formula and
running other SMT solvers on them (yices 1.0,
bclt 1.1, ario 1.2 and mathsat 3.4).

I attach a tarball containing:

- the original smt files
- the model for each instance (filename.model), in the form
 ( a ~ b ) = X, where a,b are variables ~ is a predicate and X
 is either T (true) or F (false)
- the corresponding benchmarks in smt format obtained by including
 the model in the original benchmarks (filename.msat.smt)

I hope this is a sufficient proof for changing the status
of these benchmarks.

Sicerely,
Roberto

-- 
____________________________________
| Roberto Bruttomesso -- PhD Student
| University of Trento - ITC/IRST
| http://sra.itc.it/people/bruttomesso/
| Loc. Pante', Povo, 38050, Trento, Italy
| Tel. 0461 314146
-------------- next part --------------
A non-text attachment was scrubbed...
Name: jobshoptest.tgz
Type: application/x-gzip
Size: 481874 bytes
Desc: not available
Url : /pipermail/smt-lib/attachments/20070621/b0a38297/jobshoptest-0001.bin