MaxSAT Evaluation 2021
Affiliated with SAT 2021   ·   July 5-9   ·   Barcelona, Spain

Change to the v-line

For instances with millions of variables, the v-line occupies 10’s of millions of characters. In particular, each literal printed can require almost 10 characters. This poses a problem especially in the incomplete track where the solvers can return many v-lines (one for every solution found).

We propose to reduce that by a factor of 10 by having the v-line be a sequence of '0'/'1' characters one for each variable of the problem in order. For example

v-line in the current format: v -1 2 3 -4 5 6 -7 -8 -9 10 11 -12 -13 -14 15 16 17 18 v-line in new format: v 011011000110001111 Note that the new format is positional---unlike the old format the variable values must be output in order.

This year solvers can use either the new or the previous format for their outputted v-lines. We encourage solvers, particularly in the Top-K and incomplete tracks to use the new format. Next year, we will require the new format.