tiny.smt.sat

1pub const sat = @import("sat/root.zig");

1//! A SAT solver that learns a new clause from each conflict it analyzes, with the types a caller2//! builds clauses from and reads answers and evidence through. A caller builds clauses from3//! literals over numbered variables and asks whether they can all be true, optionally under assumed4//! literals. After a no, a caller wants the assumptions the refutation used and evidence that a5//! separate check can confirm on its own. Questions asked of one formula share the solver's6//! 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 since8//! changed.9//!10//! [MiniSat](https://doi.org/10.1007/978-3-540-24605-3_37), by Niklas Eén and Niklas Sörensson, is11//! 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 zero13//! 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 clauses16//! learned under those assumptions included. When no cap on learned clauses is set, a solve keeps17//! every clause from before it. While a cap on learned clauses is set, every solve starts by18//! removing the learned clauses over the cap, clauses from earlier solves included. For callers19//! that nest questions, the solver keeps an assumption list of its own, and each push keeps a saved20//! length of the assumption list that a pop returns to (an *assumption frame*). After a no under21//! assumptions, the solver reports a set of assumptions that the clauses refute together22//! (`Solver.lastUnsatCore`). The set can hold an assumption the no does not need in two cases: when23//! the solver records a core of a single assumption, and when a conflict limit runs out while the24//! 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 and27//! 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 clauses29//! over the formula and the earlier clauses of the trace, and the clause passes when that30//! propagation reaches a conflict (Reverse Unit Propagation). `Solver.lastProofArtifact` copies the31//! clauses, assumptions and steps behind one unsatisfiable answer (a *proof artifact*), and32//! `ProofArtifact.valid` checks that copy again without the solver. The clauses of that copy are33//! every clause the solver held when the solve began, learned clauses it kept included. Adding a34//! variable, a clause or an assumption, changing assumption frames, or solving again clears the35//! 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's38//! proof steps in fixed memory sized from that limit (`ProofTrace`). A caller that bounds memory39//! sets a cap on learned clauses, and the solver then keeps the learned clauses it may remove in40//! fixed memory sized from that cap (`LearnedStore`). The solver analyzes each conflict in scratch41//! memory that it sets aside at the start of each solve (`ConflictScratch`). The namespace holds42//! the solver (`Solver`) with its literal, status, statistics, restart and proof types, and it43//! re-exports `Solver`, `Literal`, `Status`, `BoolValue`, `SolveStats`, `RestartPolicy`,44//! `ProofClause`, `ProofStep`, `ProofArtifact` and the three fixed memories by name. The files45//! split the parts: `solver` holds the solver, `types` the value types, `store`, `trace` and46//! `scratch` the three fixed memories, and a proof file the proof types.47const proof = @import("proof.zig");48pub const scratch = @import("scratch.zig");49pub const solver = @import("solver.zig");50pub const store = @import("store.zig");51pub const trace = @import("trace.zig");52pub const types = @import("types.zig");5354pub const BoolValue = types.BoolValue;55pub const Literal = types.Literal;56pub const ProofArtifact = proof.ProofArtifact;57pub const ProofClause = proof.ProofClause;58pub const ProofStep = proof.ProofStep;59pub const RestartPolicy = types.RestartPolicy;60pub const Solver = solver.Solver;61pub const SolveStats = types.SolveStats;62pub const Status = types.Status;6364pub const LearnedStore = @import("store.zig").Store;65pub const ProofTrace = @import("trace.zig").Trace;66pub const ConflictScratch = scratch.ConflictScratch;