MaxSATOutput

cpbenchy run instances/ -s ortools -t 60 -p cpbenchy.observers:MaxSATOutput

What it does

Writes what a solver in the MaxSAT Evaluation prints, for each run on a WCNF instance. The cost is the objective, and the solution is a string of 0s and 1s, one per variable:

o 5
o 2
s OPTIMUM FOUND
v 010

Each competition specifies what a solver prints:

• o lines with each better objective value, while it solves
• an s line with its answer: OPTIMUM FOUND, SATISFIABLE, UNSATISFIABLE or UNKNOWN
• v lines with the solution

The output goes to each run’s logs/<run_id>.maxsat.out, written inside the measured run, as a competition solver would print it, so it costs the run the time it would cost in the competition. A run that is killed keeps its o lines. Under cpbenchy solve, the output goes to stdout, where competitions read it.

Variables that occur in no clause get 0. Instances in the format before 2022 declare their number of variables in the p wcnf header; for newer ones, it is the highest variable in a clause.

Use it

import cpbenchy
from cpbenchy import observers

cpbenchy.run("mse/*.wcnf.xz", solvers=["ortools", "exact"], time_limit=60, plugins=[observers.MaxSATOutput()])

cpbenchy run mse/*.wcnf.xz -s ortools -s exact -t 60 -p cpbenchy.observers:MaxSATOutput

There are no built-in MaxSAT rules yet; Rules shows how to write them.

What it records

Implementation

The MaxSATOutput in src/cpbenchy/observers.py, lines 105–122 of 222, as of this version of the docs.

class MaxSATOutput(CompetitionOutput):
    """MaxSAT Evaluation output: the cost as `o`, the assignment as a string of 0s and 1s."""

    name = "maxsat"
    formats = ("wcnf",)

    def on_finish(self, ctx):
        if ctx.status in ("optimal", "feasible"):
            cost = fmt.number(ctx.objective) if ctx.objective is not None else "0"
            # without soft clauses, any solution is optimal
            optimal = ctx.status == "optimal" or not ctx.model.has_objective()
            self.write(ctx, f"o {cost}", "s OPTIMUM FOUND" if optimal else "s SATISFIABLE")
            self.write(ctx, *(f"v {line}" for line in self.solution(ctx)))
        else:
            super().on_finish(ctx)

    def solution(self, ctx):
        return [fmt.bits(*numbered(ctx))]