logicaffeine_proof/
satcli.rs

1//! The SAT command-line driver shared by `logos-sat` and `largo sat`.
2//!
3//! One implementation of the SAT Competition main-track interface — read a
4//! DIMACS CNF, run the certified solve, print `s SATISFIABLE`/`s
5//! UNSATISFIABLE` (+ a `v` model for SAT), optionally export an UNSAT
6//! certificate — with the output streams injected so both binaries stay in
7//! lockstep and the driver is directly testable.
8//!
9//! Exit codes follow the competition convention: `10` = SAT, `20` = UNSAT,
10//! `1` = usage/parse/IO error.
11
12use std::io::Write;
13use std::path::Path;
14
15use crate::cdcl::Lit;
16use crate::dimacs;
17use crate::proof::ProofStep;
18use crate::proof_emit;
19use crate::solve::{solve_structured, Answer, Route};
20
21/// Run the solver on `input`, writing the solution to `out` and comments /
22/// diagnostics to `err`. When `proof_path` is given and the verdict is
23/// UNSAT, an exportable certificate is written there. `stats` prints a
24/// `c stats …` line to `err`.
25pub fn run(
26    input: &Path,
27    proof_path: Option<&Path>,
28    stats: bool,
29    out: &mut dyn Write,
30    err: &mut dyn Write,
31) -> u8 {
32    let text = match std::fs::read_to_string(input) {
33        Ok(t) => t,
34        Err(e) => {
35            let _ = writeln!(err, "c error: cannot read {}: {e}", input.display());
36            return 1;
37        }
38    };
39    let cnf = match dimacs::parse(&text) {
40        Ok(c) => c,
41        Err(e) => {
42            let _ = writeln!(err, "c error: malformed DIMACS: {e:?}");
43            return 1;
44        }
45    };
46
47    let t = std::time::Instant::now();
48    let solved = solve_structured(cnf.num_vars, &cnf.clauses);
49    let secs = t.elapsed().as_secs_f64();
50    if stats {
51        let _ = writeln!(
52            err,
53            "c stats vars={} clauses={} time={:.3}s via={:?} conflicts={}",
54            cnf.num_vars,
55            cnf.clauses.len(),
56            secs,
57            solved.via,
58            solved.conflicts
59        );
60    }
61    match solved.answer {
62        Answer::Sat(model) => {
63            let _ = writeln!(out, "s SATISFIABLE");
64            print_model(out, &model, cnf.num_vars);
65            10
66        }
67        Answer::Unsat => {
68            let _ = writeln!(out, "s UNSATISFIABLE");
69            if let Some(path) = proof_path {
70                write_proof(err, path, solved.via, cnf.num_vars, &cnf.clauses, &solved.proof);
71            }
72            20
73        }
74    }
75}
76
77/// Compile an algebraic route's refutation (GF(2) parity or GF(p) modular) to DRAT resolvent steps,
78/// or `None` if the resolution route blows past its budget (then the verdict stands on the native
79/// algebraic certificate, but no clausal proof is exported — see [`crate::xor_drat`]).
80fn algebraic_drat(via: Route, num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Vec<ProofStep>> {
81    use crate::xor_drat::{emit_modp_drat, emit_xor_drat};
82    let resolvents = match via {
83        Route::Parity => {
84            let eqs = crate::lyapunov::extract_xor(num_vars, clauses);
85            let refutation = match crate::xorsat::solve(&eqs, num_vars) {
86                crate::xorsat::XorOutcome::Unsat(s) => s,
87                crate::xorsat::XorOutcome::Sat(_) => return None,
88            };
89            emit_xor_drat(&eqs, &refutation)?
90        }
91        Route::ModP => emit_modp_drat(num_vars, clauses)?,
92        _ => return None,
93    };
94    Some(resolvents.into_iter().map(ProofStep::Rup).collect())
95}
96
97/// Write the UNSAT certificate: DRAT for a RUP-only proof (the CDCL route), DPR for a proof that
98/// carries PR symmetry steps (the symmetry route), or the algebraic GF(2)/GF(p) bridge compiled to
99/// DRAT (the parity / mod-p routes). The internal solve already verified it.
100fn write_proof(
101    err: &mut dyn Write,
102    path: &Path,
103    via: Route,
104    num_vars: usize,
105    clauses: &[Vec<Lit>],
106    steps: &[ProofStep],
107) {
108    let display = path.display();
109    // Parity / mod-p routes certify internally with a native algebraic witness and carry no clausal
110    // steps; compile their linear-dependency refutation to a strict DRAT proof on demand.
111    if matches!(via, Route::Parity | Route::ModP) {
112        match algebraic_drat(via, num_vars, clauses) {
113            Some(alg) => match proof_emit::emit_drat(num_vars, clauses, &alg) {
114                Ok(drat) => {
115                    if let Err(e) = std::fs::write(path, drat) {
116                        let _ = writeln!(err, "c error: cannot write proof {display}: {e}");
117                    } else {
118                        let _ = writeln!(err, "c proof: DRAT via the {via:?} algebraic bridge — verify with `drat-trim {display}`");
119                    }
120                }
121                Err(e) => {
122                    let _ = writeln!(err, "c warning: algebraic proof not RUP-emittable ({e:?}) — verified internally");
123                }
124            },
125            None => {
126                let _ = writeln!(
127                    err,
128                    "c warning: {via:?} DRAT exceeded the resolution budget (would blow up) — verdict certified internally only"
129                );
130            }
131        }
132        return;
133    }
134    if let Ok(drat) = proof_emit::emit_drat(num_vars, clauses, steps) {
135        if let Err(e) = std::fs::write(path, drat) {
136            let _ = writeln!(err, "c error: cannot write proof {display}: {e}");
137        }
138        return;
139    }
140    if let Ok(dpr) = proof_emit::emit_dpr(num_vars, clauses, steps) {
141        if let Err(e) = std::fs::write(path, dpr) {
142            let _ = writeln!(err, "c error: cannot write proof {display}: {e}");
143        }
144        return;
145    }
146    // Substitution-redundancy proof (the symmetry route): emit the `.sr` format, which `sr2drat`
147    // expands to plain DRAT for `drat-trim` to verify externally.
148    match proof_emit::emit_sr(num_vars, clauses, steps) {
149        Ok(sr) => {
150            if let Err(e) = std::fs::write(path, sr) {
151                let _ = writeln!(err, "c error: cannot write proof {display}: {e}");
152            } else {
153                let _ = writeln!(err, "c proof: substitution-redundancy (.sr) — verify with `sr2drat {display} | drat-trim`");
154            }
155        }
156        Err(e) => {
157            let _ = writeln!(err, "c warning: proof not exportable ({e:?}) — verified internally");
158        }
159    }
160}
161
162/// Print the model as wrapped `v` lines over variables `1..=num_vars`, terminated by `0`, per the
163/// DIMACS solution convention. Variable `i` (0-based in the model) is literal `i+1`.
164fn print_model(out: &mut dyn Write, model: &[bool], num_vars: usize) {
165    const PER_LINE: usize = 20;
166    let mut line = String::from("v");
167    let mut on_line = 0usize;
168    for v in 0..num_vars {
169        let lit = if model.get(v).copied().unwrap_or(false) { (v + 1) as i64 } else { -((v + 1) as i64) };
170        line.push(' ');
171        line.push_str(&lit.to_string());
172        on_line += 1;
173        if on_line == PER_LINE {
174            let _ = writeln!(out, "{line}");
175            line = String::from("v");
176            on_line = 0;
177        }
178    }
179    line.push_str(" 0");
180    let _ = writeln!(out, "{line}");
181}
logicaffeine_proof/satcli.rs

logicaffeine_proof/
satcli.rs
