Module satcli 

The SAT command-line driver shared by logos-sat and largo sat.

One implementation of the SAT Competition main-track interface — read a DIMACS CNF, run the certified solve, print s SATISFIABLE/s UNSATISFIABLE (+ a v model for SAT), optionally export an UNSAT certificate — with the output streams injected so both binaries stay in lockstep and the driver is directly testable.

Exit codes follow the competition convention: 10 = SAT, 20 = UNSAT, 1 = usage/parse/IO error.

Functions

run

Run the solver on input, writing the solution to out and comments / diagnostics to err. When proof_path is given and the verdict is UNSAT, an exportable certificate is written there. stats prints a c stats … line to err.