Next Year’s change to the Input format.
Input Format: Next year we will be changing the input format of the maxsat instances. This will require some change to your solver’s parser, but will make it easier to construct and submit new benchmark instances.The changes will be as follows:
- No more p-line! The p-line is a source of many problems when constructing benchmark files. There is some value for knowing how many variables and clauses there are in the formula before reading the clauses (e.g., for allocating fixed sized arrays). But even in this case the space required for storing the clauses would have to be dynamically reallocated as the clauses are read from the file.
- No more top. As a consequence of removing the p-line there will no longer be a specification of a top value. Computing the correct value of top has proved to be error prone, and the standard value of top (the sum of the soft clause weights + 1) has issues with overflow.
- h lines. In the new format hard clauses will be indicated with an in initial ‘h’ comming before the list of literals in the clause.
- Weights. We preserve the change made in 2017 where all soft clauses must have a weight. So the first number in every soft clause will continue to denote its weight.
Instance in the current format:
c This is a comment
c Example 1...another comment
p wcnf 7 4 12
12 1 2 3 4 0
1 -3 -5 6 7 0
6 -1 -2 0
4 1 6 -7 0
In new format
c This is a comment
c Example 1...another comment
h 1 2 3 4 0
1 -3 -5 6 7 0
6 -1 -2 0
4 1 6 -7 0