lib/smt/src/sat/root.zig

daab053ee43316e1809a84551d573ddd1e5bf3d2

 1 //! A SAT solver that learns a new clause from each conflict it analyzes, with the types a caller
 2 //! builds clauses from and reads answers and evidence through. A caller builds clauses from
 3 //! literals over numbered variables and asks whether they can all be true, optionally under assumed
 4 //! literals. After a no, a caller wants the assumptions the refutation used and evidence that a
 5 //! separate check can confirm on its own. Questions asked of one formula share the solver's
 6 //! clauses, and evidence describes the formula of one solve, so any later change to the clauses,
 7 //! the variables or the assumptions makes the evidence describe a formula the solver has since
 8 //! changed.
 9 //!
10 //! [MiniSat](https://doi.org/10.1007/978-3-540-24605-3_37), by Niklas Eén and Niklas Sörensson, is
11 //! a SAT solver that learns a clause from each conflict. The namespace keeps its way of solving:
12 //! each clause of two or more literals watches two of them, each conflict above decision level zero
13 //! yields a learned clause, and a solve can run under assumed literals.
14 //!
15 //! A solve under assumptions discards every clause added during it when it completes, the clauses
16 //! learned under those assumptions included. When no cap on learned clauses is set, a solve keeps
17 //! every clause from before it. While a cap on learned clauses is set, every solve starts by
18 //! removing the learned clauses over the cap, clauses from earlier solves included. For callers
19 //! that nest questions, the solver keeps an assumption list of its own, and each push keeps a saved
20 //! length of the assumption list that a pop returns to (an *assumption frame*). After a no under
21 //! assumptions, the solver reports a set of assumptions that the clauses refute together
22 //! (`Solver.lastUnsatCore`). The set can hold an assumption the no does not need in two cases: when
23 //! the solver records a core of a single assumption, and when a conflict limit runs out while the
24 //! solver shrinks the core, which leaves every assumption in it.
25 //!
26 //! After each unsatisfiable answer, the solver keeps a trace for that solve's clauses and
27 //! assumptions: a list of clauses that ends in the empty clause. To check one clause of the trace,
28 //! a checker assumes its literals false together with the assumptions and propagates unit clauses
29 //! over the formula and the earlier clauses of the trace, and the clause passes when that
30 //! propagation reaches a conflict (Reverse Unit Propagation). `Solver.lastProofArtifact` copies the
31 //! clauses, assumptions and steps behind one unsatisfiable answer (a *proof artifact*), and
32 //! `ProofArtifact.valid` checks that copy again without the solver. The clauses of that copy are
33 //! every clause the solver held when the solve began, learned clauses it kept included. Adding a
34 //! variable, a clause or an assumption, changing assumption frames, or solving again clears the
35 //! recorded core and trace, so evidence holds only until the next change to the solver.
36 //!
37 //! A caller that bounds the search sets a conflict limit, and the solver then keeps each solve's
38 //! proof steps in fixed memory sized from that limit (`ProofTrace`). A caller that bounds memory
39 //! sets a cap on learned clauses, and the solver then keeps the learned clauses it may remove in
40 //! fixed memory sized from that cap (`LearnedStore`). The solver analyzes each conflict in scratch
41 //! memory that it sets aside at the start of each solve (`ConflictScratch`). The namespace holds
42 //! the solver (`Solver`) with its literal, status, statistics, restart and proof types, and it
43 //! re-exports `Solver`, `Literal`, `Status`, `BoolValue`, `SolveStats`, `RestartPolicy`,
44 //! `ProofClause`, `ProofStep`, `ProofArtifact` and the three fixed memories by name. The files
45 //! split the parts: `solver` holds the solver, `types` the value types, `store`, `trace` and
46 //! `scratch` the three fixed memories, and a proof file the proof types.
47 const proof = @import("proof.zig");
48 pub const scratch = @import("scratch.zig");
49 pub const solver = @import("solver.zig");
50 pub const store = @import("store.zig");
51 pub const trace = @import("trace.zig");
52 pub const types = @import("types.zig");
53 
54 pub const BoolValue = types.BoolValue;
55 pub const Literal = types.Literal;
56 pub const ProofArtifact = proof.ProofArtifact;
57 pub const ProofClause = proof.ProofClause;
58 pub const ProofStep = proof.ProofStep;
59 pub const RestartPolicy = types.RestartPolicy;
60 pub const Solver = solver.Solver;
61 pub const SolveStats = types.SolveStats;
62 pub const Status = types.Status;
63 
64 pub const LearnedStore = @import("store.zig").Store;
65 pub const ProofTrace = @import("trace.zig").Trace;
66 pub const ConflictScratch = scratch.ConflictScratch;