XCSP 2.1 Benchmarks

---

fischerExtConvert

Lecoutre's category
PATT (Patterned instances) - Fischer
Lecoutre's tooltips
This series correspond to Fischer SMT Instances from MathSat converted to CSP by Lucas Bordeaux. The translation is a straightforward encoding of the SMT syntax in which Boolean combinations of arithmetic constraints are decomposed into primitive constraints, using reification where appropriate. Note that the domains have been artificially bounded, whereas in SMT theorem proving should be done over the unbounded integers.
Source
http://www.cril.univ-artois.fr/~lecoutre/research/benchmarks/fischer.tgz
Comments
None

Number of instances: 2 (0 processed, 0 partially processed, 2 failed)

Processing completed

Partially processed

Processing failed
fischer-10-10-fair
fischer-10-10-fair_ext