Tracks

Solvers can be submitted for evaluation in the following tracks, characterized by the types of benchmarks instances used within each track to evaluate the solvers. Please note that MSE 2020 does not include a track for randomly generated MaxSAT instances.

Main Tracks

• Unweighted: Combines the industrial and crafted unweighted and unweighted partial MaxSAT categories from previous MaxSAT evaluations. Purely randomly generated instances are not included.
• Weighted: Combines the industrial and crafted weighted and weighted partial MaxSAT categories from previous MaxSAT evaluations. All benchmarks will be truly weighted, i.e., contain soft clauses with different weights. Purely randomly generated instances are not included.

Special Tracks

• Incomplete Special Tracks: Two special tracks, unweighted and weighted (following the categorization of the main tracks), for incomplete solvers are organized. Every incomplete solver participating in one or both of the tracks will be evaluated using two distinct per-instance time limits: 60 seconds and 300 seconds. The ranking criterion for these tracks is described under rules.
• [New] Top-k track: This year we introduce a new experimental track. In some applications there is a need for diverse high-quality solutions. This often arises when some solution quality criteria which cannot be easily expressed in the objective function. In these cases it is useful for the solver to be able to generate multiple solutions from which one can be selected. The details for this track are described here.