Top-k 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. In this track the input is a standardly encoded maxsat instances (*.wcnf file) along with an integer k. So you solver will be invoked with the command line like the following: your_solver input_instance.wcnf 10 where in this example k = 10.

Your solver is expected to output k solutions (as v-lines where the true literal of every variable is listed) satisfying the following properties:

• Each solution is a feasible solution of input_instance.wcnf, i.e., it must satisfy all hard clauses of input_instance.wcnf.
• Each solution must falsify a different set of soft clauses.
• Each solution must be an optimal solution among the set of solutions falsifying different soft clauses that remain.

  More precisely, let S = {s | s is a feasible solution of input_instance.wcnf}; let s1, s2, …, si, be the sequence of first i solutions returned by your solver; and for any feasible solution s let sameSofts(s) be the subset of S consisting of all solutions that falsify the same set of solutions as s.

  Then it must be the case that the i+1’th solution returned, si+1, must have the lowest cost among the set of solutions S - (sameSofts(s1) U … U sameSofts(si) .

• Your solver should return an empty v-line (i.e., a line starting and ending with the character v) and exit if after returning i solutions there are no more feasible solutions. That is, when S - (sameSofts(s1) U … U sameSofts(si) is empty.

Note. As a consequence of these properties every solver should produce an identical sequence of solution costs (even though the individual solutions can vary),

Example 1. Consider the maxsat instance p wcnf 3 4 7 1 -1 0 2 -2 0 3 -3 0 7 1 2 3 0 Which corresponds to the soft clauses {(-1, wt=1), (-2, wt=2), (-3, wt=3)} and the single hard clause (1 2 3). With k = 5 your solver should return the following sequence of v-lines v 1 -2 -3 v -1 2 -3 v 1 2 -3 v -1 -2 3 V 1 -2 3 Note that solutions 3 and 4 both have cost 3 and so could be returned in either order. Note also that there are only 7 solutions satisfying different sets of soft clauses so if k > 7 your solver would return an empty v-line and terminate.

Example 2. With the maxsat instance p wcnf 6 7 4 1 -1 -2 0 2 -3 -4 0 4 -5 1 0 4 -5 2 0 4 -6 3 0 4 -6 4 0 4 5 6 0 With k = 4 the first v-line returned by your solver should be one of the following: v 1 2 -3 -4 5 -6 v 1 2 -3 4 5 -6 or v 1 2 3 -4 5 -6 All of these solutions falsify the first soft clause and have cost 1, The second v-line returned by your solver should be one of the following v -1 -2 3 4 -5 6 v -1 2 3 4 -5 6 or v 1 -2 3 4 -5 6 All of these solutions falsify the second soft clause and have cost 2, The third solution returned by your solver should be: v 1 2 3 4 5 6 This solution falsifies both soft clauses and has cost 3 Finally, your solver should return the empty v-line v indicating that no more different solutions can be found.

Scoring:

Since the Top-K track is experimental this year, we will use a simple scoring scheme to obtain an indication of solver performance on this task. The scoring scheme will be refined in future evaluations after consultation with the participants. In particular, this year the emphasis will be on the number of correct solutions returned rather than on the time required to find those solutions. (Solver efficiency will still play a role on instances where it is hard to find all k solutions).

For each instance a solver will receive a score of a/k where a is the number of correct solutions returned by the solver within the time bound, and k is the minimum of the number of solutions requested on the command line and the number of solutions actually available plus one. That is, in cases where the specified k is larger than the number of distinct solutions, we will count the final empty v-line as one of the valid solutions.

If the solver returns an erroneous solution (e.g., a solution that is not the next optimal solution amongst the remaining distinct solutions as described above), that erroneous solution and all subsequent solutions will be discarded and not be counted in the sum of correct solutions a.

Example 3. Consider the input instance specified in example 2, but with k = 10. This instance has only 3 distinct top-K solutions and one more for the final v-line, so the maximum number of correct v-lines that could be returned is 4. Suppose that solver s returns the following sequence of v-lines

• v 1 2 3 -4 5 -6 v 1 2 3 4 5 6 Then s would get a score of ¼ on this instance: the first v-line is correct it has cost 1. The second v-line is incorrect as it has cost 3 and there are solutions of cost 2.
• v 1 2 -3 -4 5 -6 v -1 2 3 4 -5 6 Then s would get a score of 2/4. As both v-lines are correct.
• v 1 2 -3 -4 5 -6 v -1 2 3 4 -5 6 v 1 2 3 4 5 6 v Then s would get a score of 4/4 if it was the only solver returning all 4 correct v-lines