SATOutput

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

What it does

Writes what a solver in the SAT competition prints, for each run on a DIMACS CNF instance. The solution is DIMACS literals, 20 per line, ending in 0:

s SATISFIABLE
v -1 2 3 -4 0

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>.sat.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.

Use it

import cpbenchy
from cpbenchy import observers

cpbenchy.run("sat/*.cnf.xz", solvers=["ortools", "exact"], time_limit=60, plugins=[observers.SATOutput()])

cpbenchy run sat/*.cnf.xz -s ortools -s exact -t 60 -p cpbenchy.observers:SATOutput

What it records

Notes

CPMpy’s CNF loader gives variables generated names, which lose their DIMACS numbers. So, unless the run has its own loader, SATOutput loads CNF instances itself, with formats.load_cnf, which names them x1, x2, … Loading is still measured as parse_s.

Implementation

The SATOutput in src/cpbenchy/observers.py, lines 125–142 of 222, as of this version of the docs.

class SATOutput(CompetitionOutput):
    """SAT competition output: `v` lines of DIMACS literals, ending in 0.

    CPMpy's CNF loader names variables in a way that loses their numbers, so unless the run has its own
    loader, this loads `.cnf` files with `cpbenchy.formats.load_cnf` instead (timed as `parse_s`, as usual).
    """

    name = "sat"
    formats = ("cnf",)

    def on_load(self, ctx):
        if ctx.spec.loader is None:
            path = ctx.spec.instance.path
            return fmt.load_cnf(path, Loader().opener(path))
        return None

    def solution(self, ctx):
        return fmt.dimacs_values(*numbered(ctx))