MaxSAT Benchmarks
This webpage provides a growing collection of MaxSAT benchmarks arising from application studies
by the Constraint Reasoning and Optimization Group at the
Department of Computer Science, University of Helsinki.
Extension of the WCNF DIMACS format to support realvalued weights on soft clauses
Some of the MaxSAT benchmark sets provided here are based on problem domains in which
it is natural to have realvalued constants (weights on variables) in the objective function under optimization.
For these domains, we provide two variants of each instance:

One with integer weights, obtained by multiplying the original realvalued weights by 1) a large constant such
that the original decimal accuracy is preserved exactly, or 2) otherwise as large a constant
as possible within the [0,2^63] range supported by the standard WCNF DIMACS format, and
rounding to the nearest integer.
 One using the actual realvalued weights within the WCNF file.
While the use of realvalued weights would be a natural choice in many potential application domains of MaxSAT,
we note that the current standard WCNF DIMACS format does not support realvalued weight on soft clauses.
Hence currently some of the stateoftheart MaxSAT solvers do not support realvalued, either;
though there are exceptions, such as MaxHS.
Benchmarks
PROBLEM DOMAIN  BENCHMARK SET  MORE INFORMATION 
Correlation Clustering
The task of correlation clustering is to find a clustering that agrees (correlates) as well as possible with the pairwise similarity information of the dataset. 
realweighted
integerweighted

readme
paper: [1] [6]

Learning Optimal BoundedTreewidth Bayesian Network Structures
The Optimal BoundedTreewidth Bayesian Network structure learning task involves
learning a Bayesian Network (a directed acyclic graph) that optimizes
a given scoring function, expressed as local scores for each node and the
parents of that node.

realweighted
integerweighted

readme
paper: [2] [6]

Causal Structure Discovery (synthetic)
The task of (constraintbased) causal structure discovery involves finding a graph structure
whose reachability (and separability) properties agree as well as possible with the statistical (in)dependence relations in
passively observed data. 
realweighted
integerweighted

readme
papers: [6] [4] [3]

Exact Treewidth Computation
Given an undirected graph G the task of exactly computing the treewidth of G is a well known NPhard problem. This datasets contain MaxSAT instances created based on the linear ordering characterization of treewidth computation

integerweighted

readme
paper: [5]

Causal Structure Discovery (real)
The task of (constraintbased) causal structure discovery involves finding a graph structure
whose reachability (and separability) properties agree as well as possible with the statistical (in)dependence relations in
passively observed data. 
integerweighted

readme
papers: [7][3] [4] [6]

References

CostOptimal Constrained Correlation Clustering via Weighted Partial Maximum Satisfiability.
Jeremias Berg and Matti Järvisalo.
Artificial Intelligence,
to appear (2015).
[doi:10.1016/j.artint.2015.07.001]
Preliminary version: [pdf]
[abstract/bibtex]
 Learning Optimal Bounded Treewidth Bayesian Networks via Maximum Satisfiability.
Jeremias Berg, Matti Järvisalo, and Brandon Malone.
In Jukka Corander and Samuel Kaski, editors,
Proceedings of the 17th International Conference on
Artificial Intelligence and Statistics
(AISTATS 2014), volume 33 of
JMLR Workshop and Conference Proceedings,
pages 8695. JMLR, 2014.
[Publisher's version]
[pdf]
[abstract/bibtex]
 Discovering Cyclic Causal Models with Latent Variables: A General SATBased Procedure.
Antti Hyttinen, Patrik Hoyer,
Frederick Eberhardt, and Matti Järvisalo.
In Ann Nicholson and Padhraic Smyth, editors,
Proceedings of the 29th Conference on
Uncertainty in Artificial Intelligence
(UAI 2013),
pages 301310. AUAI Press, 2013.
[Publisher's version]
[pdf]
[abstract/bibtex]
 Constraintbased Causal Discovery: Conflict Resolution with Answer Set Programming.
Antti Hyttinen, Frederick Eberhardt, and Matti Järvisalo.
In Jin Tian and Nevin L. Zhang, editors,
Proceedings of the 30th Conference on
Uncertainty in Artificial Intelligence
(UAI 2014),
pages 340349. AUAI Press, 2014.
[pdf]
[abstract/bibtex]
 SATBased Approaches to Treewidth Computation: An Evaluation.
Jeremias Berg and Matti Järvisalo.
In Proceedings of the 2014
IEEE 26th International Conference
on Tools with Artificial Intelligence (ICTAI 2014),
pages 328335. IEEE Computer Society, 2014.
[doi:10.1109/ICTAI.2014.57]
[pdf]
[abstract/bibtex]
 Applications of MaxSAT in Data Analysis.
Jeremias Berg, Antti Hyttinen, and Matti Järvisalo.
In ???, editors, Proceedings of the
6th Pragmatics of
SAT Workshop (PoS 2015),
volume ?? of Easychair
Proceedings in Computing, pages ????. Easychair, 2015.
[pdf]
[abstract/bibtex]
 A CoreGuided Approach to Learning Optimal Causal Graphs.Antti Hyttinen, Paul Saikko, and Matti Järvisalo.
In Proceedings of the
26th International Joint Conference on Artificial Intelligence
(IJCAI 2017), pages 645651. AAAI Press, 2017.
[Publisher's version]
[pdf]
[abstract/bibtex]
