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 real-valued weights on soft clauses

Some of the MaxSAT benchmark sets provided here are based on problem domains in which it is natural to have real-valued 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 real-valued 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 real-valued weights within the WCNF file.

While the use of real-valued 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 real-valued weight on soft clauses. Hence currently some of the state-of-the-art MaxSAT solvers do not support real-valued, either; though there are exceptions, such as MaxHS.

Benchmarks

PROBLEM DOMAIN BENCHMARK SETMORE 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.		 real-weighted
integer-weighted
 readme
paper: [1] [6]
Learning Optimal Bounded-Treewidth Bayesian Network Structures
The Optimal Bounded-Treewidth 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. 		real-weighted
integer-weighted
 readme
paper: [2] [6]
Causal Structure Discovery (synthetic)
The task of (constraint-based) 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.		 real-weighted
integer-weighted
 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 NP-hard problem. This datasets contain MaxSAT instances created based on the linear ordering characterization of treewidth computation 		integer-weighted
 readme
paper: [5]
Causal Structure Discovery (real)
The task of (constraint-based) 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.		 integer-weighted
 readme
papers: [7][3] [4] [6]

References

  1. Cost-Optimal 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]
  2. 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 86-95. JMLR, 2014.
    [Publisher's version] [pdf] [abstract/bibtex]
  3. Discovering Cyclic Causal Models with Latent Variables: A General SAT-Based 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 301-310. AUAI Press, 2013.
    [Publisher's version] [pdf] [abstract/bibtex]
  4. Constraint-based 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 340-349. AUAI Press, 2014.
    [pdf] [abstract/bibtex]
  5. SAT-Based 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 328-335. IEEE Computer Society, 2014.
    [doi:10.1109/ICTAI.2014.57] [pdf] [abstract/bibtex]
  6. 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]
  7. A Core-Guided 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 645-651. AAAI Press, 2017.
    [Publisher's version] [pdf] [abstract/bibtex]