equiv_receipt.solver

Run an external SAT solver in proof-emitting mode and keep the proof.

The bundled minisolve is a demonstration. It cannot reach the instances a real equivalence check produces, and it says so. This module lets you point the package at a solver that can — CaDiCaL, Kissat, or anything else that speaks DIMACS and writes a DRAT proof.

The trust story does not change, which is the entire point. The external solver is not trusted. It is asked for a proof, the proof goes into the receipt, and the proof is re-checked by equiv_receipt.forward_rup_check() — code you can read — before any verdict is asserted. Swapping in a faster solver buys reach, not credibility. A solver that lies produces a proof that fails to check.

Two consequences worth stating plainly:

  • If the solver reports UNSAT but emits no usable proof, this raises rather than returning a receipt. An unproven UNSAT is a claim, and this package does not package claims.
  • If the solver is not on PATH or exits in a way that is not "SAT" or "UNSAT", that is an error, not a verdict. Silence is never read as agreement.
Clause = typing.List[int]
class SolverError(builtins.RuntimeError):

The external solver could not be used, or did not answer usefully.

class Solver:

An external SAT solver, described by how to invoke it.

argv is a template list. {cnf} is replaced by the input path and {drat} by the path the solver should write its proof to. For example::

Solver("cadical", ["cadical", "-q", "--no-binary", "{cnf}", "{drat}"])
Solver("kissat",  ["kissat", "-q", "--relaxed", "{cnf}", "{drat}"])

Nothing here is specific to those two; any solver with a DIMACS-in, DRAT-out interface works, and the template is the whole configuration.

Solver(name: str, argv: Sequence[str], *, timeout: float = 300.0)
name
argv
timeout
executable: str
def available(self) -> bool:
def version(self) -> str:

Best-effort version string, recorded in the receipt for provenance.

Provenance only — nothing is trusted on the strength of it. If the solver will not report a version, that is not an error.

def run(self, cnf_text: str, workdir: Optional[str] = None) -> Dict:

Solve cnf_text. Returns {"unsat", "drat", "model", "raw_exit"}.

Raises SolverError if the solver is missing, times out, or gives an answer that cannot be read. None of those are verdicts.

KNOWN: Dict[str, List[str]] = {'cadical': ['cadical', '-q', '--no-binary', '{cnf}', '{drat}'], 'kissat': ['kissat', '-q', '--no-binary', '{cnf}', '{drat}'], 'minisat': ['minisat', '-verb=0', '{cnf}', '{drat}']}
def known_solver(name: str, **kw) -> Solver:
def detect(**kw) -> Optional[Solver]:

The first known solver present on PATH, or None. Never guesses further.

def refute( clauses: Sequence[List[int]], solver: Optional[Solver] = None, **kw) -> Dict:

Refute clauses with an external solver. Same result shape as minisolve.refute.

The returned proof has already been re-checked here, so a solver that emits a proof this package cannot verify is reported as such rather than passed on to become someone else's problem later.