source: COSEAL Portfolio Benchmark authors: Carlos Ansotegui, Yuri Malitsky, Meinolf Sellmann translator into coseal format: Yuri Malitsky The data does not distinguish between timeout, memout or crashes! The status file will only have ok, timeout, or out of memory! This data is a collection of random, crafted and industrial Unweighted MaxSAT instances from the 2012 Evaluation (http://maxsat.ia.udl.cat:81/12/benchmarks/index.html) There are a total of 876 instances each of which is defined by 37 features and solved with 6 state-of-the-art solvers from 2012 (akmaxsat_ls, akmaxsat, DSWPM1_924, pwbo2.1, qmaxsat0.21comp, qmaxsat0.21g2comp). The best single solver, qmaxsat0.21g2comp, solves 674 instances with a PAR10 score of 4,893 while the virtual best of all 6 solvers finishes 747 instances with a PAR10 score of 3,128. The features computed using an in house developed tool and are based on a version of UBC SAT features and provide the following: Problem Size Features: [1-2] Number of variables and clauses in original formula: denoted v and c, respectively [3] Percentage of Soft Clauses [4-7] Soft Clause Weights: mean, stdev, min and max [8] Ratio of variables to clauses Variable-Clause Graph Features: [9-13] Variable node degree statistics: mean, stdev, min, max, spread [14-18] Clause node degree statistics: mean, stdev, min, max, spread Balance Features: [19-23] Positive to negative occurrences of each variable: mean, stdev, min, max, spread [24-28] Positive to negative literals in each clause: mean, stdev, min, max, spread [29-31] Fraction of unary, binary and ternary clauses Proximity to Horn Formula: [32-36] Occurrences of a variable in a Horn clause: mean, stdev, min, max, spread [37] Fraction of Horn clauses