Benchmarks


Discrete-Event System (DES) Diagnosis


These partial MaxSAT benchmarks were provided by Alban Grastien.
More information regarding these benchmarks can be found at the author's webpage.


Download

Set of 600 instances provided by the author: des (680 MB)
Subset of 100 instances submitted to the MaxSAT evaluation 2013: des_maxsat13 (204 MB)


References

Importance de la sémantique dans le codage CNF de contraintes de cardinalité : application au diagnostic de SED
Anbulagan, Alban Grastien
In Journées Francophones de Programmation par Contraintes 2008.

Importance of variables semantic in CNF encoding of cardinality constraints
Anbulagan, Alban Grastien
In Symposium on Abstraction, Reformulation and Approximation 2009.

Close Solutions


These partial MaxSAT benchmarks were provided by Ignasi Abío.


Download

Set of 486 instances provided by the author: close_solutions (4.5 GB)
Subset of 100 instances submitted to the MaxSAT evaluation 2013: close_solutions_maxsat13 (1017 MB)


References

Reducing Chaos in SAT-Like Search: Finding Solutions Close to a Given One
Ignasi Abío, Morgan Deters, Robert Nieuwenhuis, Peter J. Stuckey
In International Conference on Theory and Applications of Satisfiability Testing 2011.

Conflict Directed Lazy Decomposition
Ignasi Abío, Peter J. Stuckey
In International Conference on Principles and Practice of Constraint Programming 2012.


Preference-Based Planning


These weighted partial MaxSAT benchmarks were provided by Farah Juma.


Download

Set of 29 instances provided by the author and submitted to the MaxSAT evaluation 2013: preference_planning (12 MB)


References

Exploiting MaxSAT for Preference-Based Planning
Farah Juma, Eric I. Hsu, Sheila A. McIlraith
In Workshop on Constraint Satisfaction Techniques for Planning and Scheduling Problems 2011.

Preference-Based Planning via MaxSAT.
Farah Juma, Eric I. Hsu, and Sheila A. McIlraith
In Canadian Conference on AI 2012.