tiny.smt.sat.solver

1pub const solver = @import("solver.zig");

1//! A SAT solver that learns a new clause from each conflict it analyzes. The solver decides whether2//! clauses over Boolean variables can all be made true, optionally under assumed literals, and3//! records evidence for each unsatisfiable answer.4//!5//! A caller adds variables and clauses, asks for an answer, and then reads a satisfying assignment,6//! or a set of assumptions that the clauses refute together and a proof that a separate check can7//! confirm. A caller that asks many questions of one formula wants each question to leave the8//! clauses as they were, and a caller that bounds its work wants limits on search time and on9//! memory.10//!11//! Each assignment can make any clause that contains the opposite literal unit or false, and a12//! formula holds far more clauses than one assignment touches. A long search meets many conflicts,13//! and a clause learned from each one makes the clause list grow for as long as the search runs. An14//! unsatisfiable answer is only as sound as the search that gave it, so each learned clause and the15//! final answer need a check that replays the reasoning.16//!17//! [MiniSat](https://doi.org/10.1007/978-3-540-24605-3_37), by Niklas Eén and Niklas Sörensson, is18//! a SAT solver that learns a clause from each conflict. The package keeps its way of solving, with19//! unsat cores and proofs: each clause of two or more literals watches two of them, each conflict20//! above decision level zero yields a learned clause, and a solve can run under assumed literals.21//!22//! Each clause of two or more literals watches two of them, and a unit clause watches its one23//! literal, so an assignment visits only the clauses that watch the literal it makes false. The24//! search decides the lowest unassigned variable and gives it the value it last held, or true for a25//! variable assigned for the first time. At each conflict above decision level zero, the solver26//! resolves back to one literal of the conflict's level, learns the resulting clause, and27//! backtracks to the highest other level among its literals. Before keeping a learned clause, the28//! solver replays the propagation that led to the conflict and checks that the clause follows, and29//! a failed check ends the solve with `error.InvalidProofTrace`.30//!31//! The solver counts the distinct decision levels among a learned clause's literals (its block32//! distance). A cap on learned clauses (`max_learned_clauses`) bounds only the learned clauses33//! whose literals span more than two decision levels (*replaceable learned clauses*), and the34//! others stay for as long as the solver holds its clauses. When their count passes the cap, the35//! solver returns to decision level zero and removes them, highest block distance first and then36//! the longest, keeping each clause that justifies a current value and the newly learned clause.37//! Under a cap, the solver keeps those clauses in fixed memory sized before the search38//! (`LearnedStore`). Under a conflict limit (`conflict_budget`), the solver keeps its proof steps39//! in fixed memory sized from the limit (`ProofTrace`). The solver analyzes each conflict in40//! scratch memory at the end of its list of assigned literals in assignment order41//! (`ConflictScratch`). After a scheduled conflict count, the solver returns to decision level zero42//! and restarts the search, and the count grows by a factor after each restart (`RestartPolicy`).43//!44//! A solve assigns its assumptions first, at decision level zero. When the assumption list is45//! nonempty, the solve removes every clause added during it when it returns, so a plain `solve`46//! keeps the clauses it learned. When no cap on learned clauses is set, a solve keeps every clause47//! from before it. For callers that nest questions, the solver keeps an assumption list of its own:48//! `assume` adds to it, and each push keeps a saved length of the assumption list that a pop49//! returns to (an *assumption frame*). After an unsatisfiable answer under assumptions, the solver50//! records as the core the assumptions it had assigned when the conflict came, which is every51//! assumption unless the conflict came while it assigned them. When that recorded core holds two or52//! more assumptions, the solver drops one assumption at a time, keeps each drop that fresh solvers53//! over the caller's clauses still refute, and certifies the final set with one more solve. Under a54//! conflict limit, those extra solves share what is left of the limit. When it runs out during the55//! drops, the answer is `.unsat` with every assumption in the core. When it runs out during the56//! certifying solve, the answer is `.unknown` with an empty core.57//!58//! The proof trace holds one step per learned clause and, after an unsatisfiable answer, a final59//! empty clause that is checked before it is recorded. Adding a variable, a clause or an60//! assumption, changing assumption frames, or starting a solve clears the recorded core and trace.61//! After a satisfiable answer, or an `.unknown` answer from the main search's conflict limit, the62//! trace keeps the steps learned during the solve without a final empty clause. After an `.unknown`63//! answer from the certifying solve of core minimization, the trace keeps the refutation under64//! every assumption of the solve, ending in the empty clause. The assignment of the last search65//! stays until the next solve. When a unit clause added after a solve has a literal that this66//! assignment makes false, every later solve skips the search and checks the final empty clause at67//! once, so it returns `error.InvalidProofTrace` for a formula that is still satisfiable.68const std = @import("std");69const proof = @import("proof.zig");70const scratch = @import("scratch.zig");71const store = @import("store.zig");72const trace = @import("trace.zig");73const types = @import("types.zig");7475const assert = std.debug.assert;7677pub const BoolValue = types.BoolValue;78pub const Literal = types.Literal;79pub const ProofArtifact = proof.ProofArtifact;80pub const ProofStep = proof.ProofStep;81pub const RestartPolicy = types.RestartPolicy;82pub const SolveStats = types.SolveStats;83pub const Status = types.Status;8485const ClauseStorage = enum {86    heap,87    pool,88};8990const Clause = struct {91    literals: []Literal,92    learned: bool,93    lbd: u32,94    storage: ClauseStorage,95    watch_a: usize,96    watch_b: usize,97};9899const ClauseRef = struct {100    index: usize,101};102103const glue_lbd_max: u32 = 2;104105const PropagationResult = union(enum) {106    consistent,107    conflict: usize,108};109110const ProbeOutcome = struct {111    status: Status,112    conflicts: usize,113};114115const ClausePropagation = union(enum) {116    kept,117    moved,118    unit: Literal,119    conflict,120};121122/// A SAT solver that learns a clause from each conflict above decision level zero over the clauses123/// a caller adds, answers under assumed literals, and records an unsat core and a proof trace after124/// each unsatisfiable answer. The package's bit-vector encoder (`bitvec.Encoder`) turns terms into125/// variables and clauses of a solver it is given, and a caller then solves and reads the answer126/// through the solver. `init` takes an allocator, and the solver allocates every list, clause copy127/// and proof step with it and frees them in `deinit`. A caller sets `conflict_budget` and128/// `max_learned_clauses`, and reads `clauses` and `has_empty_clause`. The other fields are search129/// state, which a caller reads through the solver's functions. Each clause of two or more literals130/// watches two of them, and a unit clause watches its one literal. A decision gives the variable131/// the value it last held, or true for a variable assigned for the first time. The list of assigned132/// literals in assignment order has room past the variable count for the scratch memory of conflict133/// analysis (`ConflictScratch`).134pub const Solver = struct {135    allocator: std.mem.Allocator,136    /// Every clause the solver holds: the caller's nonempty clauses and the learned clauses it137    /// keeps. An empty clause from the caller stays out of the list and sets `has_empty_clause`.138    /// Clause order changes when the solver removes a learned clause under a cap, because the last139    /// clause moves into the removed clause's place. A solve with assumptions removes the clauses140    /// added during it when it returns. `clauseCount` counts the list, and `dimacs.write` writes it141    /// with learned clauses included.142    clauses: std.ArrayList(Clause) = .empty,143    watches: std.ArrayList(std.ArrayList(ClauseRef)) = .empty,144    assignment: std.ArrayList(BoolValue) = .empty,145    saved_phase: std.ArrayList(BoolValue) = .empty,146    level: std.ArrayList(u32) = .empty,147    reason: std.ArrayList(?usize) = .empty,148    trail: std.ArrayList(Literal) = .empty,149    propagation_cursor: usize = 0,150    decision_limits: std.ArrayList(usize) = .empty,151    assumptions: std.ArrayList(Literal) = .empty,152    frames: std.ArrayList(usize) = .empty,153    last_core: std.ArrayList(Literal) = .empty,154    proof_steps: std.ArrayList(ProofStep) = .empty,155    proof_assumptions: std.ArrayList(Literal) = .empty,156    proof_base_clause_count: usize = 0,157    last_stats: SolveStats = .{},158    restart_policy: RestartPolicy = .{},159    conflicts_since_restart: usize = 0,160    next_restart_conflicts: usize = 0,161    /// The most conflicts one solve may meet before it returns `.unknown`. The default `null`162    /// leaves the search unlimited. A caller sets it before a solve to bound the search's work.163    /// While it is set, the solver keeps the solve's proof steps in fixed memory sized from it and164    /// the variable count (`ProofTrace`). The extra solves of core minimization share what is left165    /// of it after the main search.166    conflict_budget: ?usize = null,167    /// The most replaceable learned clauses the solver keeps. The default `null` leaves the learned168    /// clauses uncapped. A caller sets it before a solve to bound the memory learned clauses take.169    /// At the start of each solve, and whenever the count passes the cap during a search, the170    /// solver removes replaceable learned clauses, highest block distance first and then the171    /// longest. The solver keeps each clause that justifies a current value and the newly learned172    /// clause, so the count can pass the cap by those clauses. While it is set, the solver keeps173    /// replaceable learned clauses in fixed memory sized from the cap and the variable count174    /// (`LearnedStore`). After a caller sets it back to `null`, the next solve moves those clauses175    /// to heap memory.176    max_learned_clauses: ?usize = null,177    learned_clause_count: usize = 0,178    glue_clause_count: usize = 0,179    learned_store: ?store.Store = null,180    proof_trace: ?trace.Trace = null,181    proof_trace_slab: bool = true,182    rup_assignment: std.ArrayList(BoolValue) = .empty,183    /// True once the caller has added an empty clause. Every later solve then answers `.unsat`.184    /// `dimacs.write` writes an empty clause for it, and `lastProofArtifact` adds an empty starting185    /// clause for it. The solver's own proof checks accept every step while it is set. The default186    /// is false.187    has_empty_clause: bool = false,188    inconsistent: bool = false,189190    /// Returns an empty solver that allocates with `allocator`. A caller creates one solver per191    /// formula and hands it to the code that adds the clauses. The call allocates nothing.192    pub fn init(allocator: std.mem.Allocator) Solver {193        return .{ .allocator = allocator };194    }195196    /// Frees every clause, list, fixed store, trace and proof step, and leaves the solver197    /// undefined. The owner of a solver calls it once, when it is done with the formula. Slices198    /// from `lastUnsatCore`, `lastProofTrace` and `activeAssumptions` become invalid. Artifacts199    /// from `lastProofArtifact` stay valid, because each owns its own copy.200    pub fn deinit(self: *Solver) void {201        for (self.clauses.items) |clause| {202            if (clause.storage == .heap) self.allocator.free(clause.literals);203        }204        if (self.learned_store) |*pool| pool.deinit(self.allocator);205        self.clauses.deinit(self.allocator);206        for (self.watches.items) |*watch| {207            watch.deinit(self.allocator);208        }209        self.watches.deinit(self.allocator);210        self.assignment.deinit(self.allocator);211        self.saved_phase.deinit(self.allocator);212        self.level.deinit(self.allocator);213        self.reason.deinit(self.allocator);214        self.trail.deinit(self.allocator);215        self.decision_limits.deinit(self.allocator);216        self.assumptions.deinit(self.allocator);217        self.frames.deinit(self.allocator);218        self.last_core.deinit(self.allocator);219        self.clearProofTrace();220        if (self.proof_trace) |*owner| owner.deinit(self.allocator);221        self.proof_steps.deinit(self.allocator);222        self.proof_assumptions.deinit(self.allocator);223        self.rup_assignment.deinit(self.allocator);224        self.* = undefined;225    }226227    /// Returns the number of variables: one more than the highest variable index the solver has228    /// added or seen. A caller reports it as a size of the encoded formula. A clause or an229    /// assumption that names a higher variable raises it.230    pub fn variableCount(self: *const Solver) usize {231        return self.assignment.items.len;232    }233234    /// Returns the number of entries in `clauses`. A caller reports it as a size of the encoded235    /// formula, and `dimacs.write` prints it in its header. The count includes the learned clauses236    /// the solver keeps and leaves out an empty clause from the caller.237    pub fn clauseCount(self: *const Solver) usize {238        return self.clauses.items.len;239    }240241    /// Returns the number of learned clauses the solver holds, at every block distance. A caller242    /// checks how many learned clauses survive a capped search. The count drops when the solver243    /// removes a learned clause under a cap and when a solve with assumptions returns.244    pub fn retainedLearnedClauses(self: *const Solver) usize {245        return self.learned_clause_count;246    }247248    /// Returns the number of learned clauses whose literals span more than two decision levels. A249    /// caller compares it with `max_learned_clauses` after a capped search. These are the clauses250    /// the cap bounds.251    pub fn replaceableLearnedClauses(self: *const Solver) usize {252        assert(self.glue_clause_count <= self.learned_clause_count);253        return self.learned_clause_count - self.glue_clause_count;254    }255256    /// Sets the restart schedule for later solves. A caller that wants restarts at a different257    /// pace, such as after every conflict, sets it before solving. The schedule takes effect at the258    /// start of the next solve.259    pub fn setRestartPolicy(self: *Solver, policy: RestartPolicy) void {260        self.restart_policy = policy;261    }262263    /// Returns the restart schedule later solves use. A caller reads back the schedule that264    /// `setRestartPolicy` set, or the default.265    pub fn restartPolicy(self: *const Solver) RestartPolicy {266        return self.restart_policy;267    }268269    /// Adds one unassigned variable and returns its index, counting from 0. `bitvec.Encoder` adds a270    /// variable for each Boolean it encodes, and `dimacs.parse` adds the variable count of its271    /// header. The call clears the recorded core and trace. The call returns `error.OutOfMemory`272    /// when a list fails to grow. An index at or above 2^31 overflows the literal's packed number,273    /// so building a literal for it panics in safe builds.274    pub fn addVariable(self: *Solver) !u32 {275        self.last_core.clearRetainingCapacity();276        self.clearProofTrace();277        const variable_index: u32 = @intCast(self.assignment.items.len);278        try self.ensureVariable(variable_index);279        return variable_index;280    }281282    /// Adds a copy of `literals` as a clause and adds any variable it names that the solver lacks.283    /// `bitvec.Encoder` asserts each encoded fact through it, and `dimacs.parse` adds each clause284    /// of its input. The caller keeps `literals`. An empty slice sets `has_empty_clause`, and every285    /// later solve answers `.unsat`. The solver assigns the literal of a unit clause at once. When286    /// the literal of a unit clause is false under the assignment the last search left, every later287    /// solve skips the search and checks the final empty clause at once, so it returns288    /// `error.InvalidProofTrace` for a formula that is still satisfiable. The call clears the289    /// recorded core and trace. The call returns `error.OutOfMemory` when a copy or a list fails to290    /// grow, and then the clause is left out while variables it named may stay added.291    pub fn addClause(self: *Solver, literals: []const Literal) !void {292        self.last_core.clearRetainingCapacity();293        self.clearProofTrace();294        if (literals.len == 0) {295            self.has_empty_clause = true;296            self.inconsistent = true;297            return;298        }299        for (literals) |literal| {300            try self.ensureVariable(literal.variable());301        }302        const owned = try self.allocator.dupe(Literal, literals);303        errdefer self.allocator.free(owned);304        const clause_index = self.clauses.items.len;305        const clause = Clause{306            .literals = owned,307            .learned = false,308            .lbd = 0,309            .storage = .heap,310            .watch_a = 0,311            .watch_b = if (owned.len > 1) 1 else 0,312        };313        try self.clauses.append(self.allocator, clause);314        errdefer _ = self.clauses.pop();315        try self.addWatch(owned[0], clause_index);316        errdefer _ = self.removeWatch(owned[0], clause_index);317        if (owned.len > 1) {318            try self.addWatch(owned[1], clause_index);319        }320        if (owned.len == 1) {321            if (!try self.enqueue(owned[0], clause_index)) self.inconsistent = true;322        }323    }324325    /// Solves the clauses alone, as `solveWithAssumptions` does with an empty list. A caller that326    /// asks one question of a formula calls it. The solver's own assumption list, which `assume`327    /// fills, takes no part.328    pub fn solve(self: *Solver) !Status {329        return self.solveWithAssumptions(&.{});330    }331332    /// Saves the current length of the assumption list, so the next `popAssumptionFrame` returns333    /// the list to it. A caller that nests questions pushes a frame before it assumes the literals334    /// of an inner question. The call clears the recorded core and trace. The call returns335    /// `error.OutOfMemory` when the frame list fails to grow.336    pub fn pushAssumptionFrame(self: *Solver) !void {337        self.last_core.clearRetainingCapacity();338        self.clearProofTrace();339        try self.frames.append(self.allocator, self.assumptions.items.len);340    }341342    /// Returns the assumption list to the length the latest push saved and closes that frame. A343    /// caller that nests questions pops a frame to leave an inner question. With no frame open, the344    /// list stays as it is. The call clears the recorded core and trace in both cases.345    pub fn popAssumptionFrame(self: *Solver) void {346        self.last_core.clearRetainingCapacity();347        self.clearProofTrace();348        const frame_start = self.frames.pop() orelse return;349        self.assumptions.shrinkRetainingCapacity(frame_start);350    }351352    /// Adds `literal` to the solver's assumption list and adds its variable when the solver lacks353    /// it. `bitvec.Encoder` assumes the literal of each assumed term through it, for a later354    /// `solveWithActiveAssumptions`. The literal stays in the list until a pop past its frame or355    /// `clearAssumptionFrames`. The call clears the recorded core and trace. The call returns356    /// `error.OutOfMemory` when a list fails to grow.357    pub fn assume(self: *Solver, literal: Literal) !void {358        self.last_core.clearRetainingCapacity();359        self.clearProofTrace();360        try self.ensureVariable(literal.variable());361        try self.assumptions.append(self.allocator, literal);362    }363364    /// Empties the assumption list and closes every frame. A caller that starts a new round of365    /// questions calls it to drop every assumption and frame at once. The call clears the recorded366    /// core and trace.367    pub fn clearAssumptionFrames(self: *Solver) void {368        self.last_core.clearRetainingCapacity();369        self.clearProofTrace();370        self.assumptions.clearRetainingCapacity();371        self.frames.clearRetainingCapacity();372    }373374    /// Solves under the solver's own assumption list, as `solveWithAssumptions` does.375    /// `bitvec.Encoder.solve` calls it, so the literals assumed with `assume` take part.376    pub fn solveWithActiveAssumptions(self: *Solver) !Status {377        return self.solveWithAssumptions(self.assumptions.items);378    }379380    /// Returns the solver's assumption list, oldest first. A caller reads the assumptions in force381    /// after pushes and pops. The slice stays valid until the list changes.382    pub fn activeAssumptions(self: *const Solver) []const Literal {383        return self.assumptions.items;384    }385386    /// Returns the number of open frames. A caller checks how deep its nesting is.387    pub fn frameDepth(self: *const Solver) usize {388        return self.frames.items.len;389    }390391    /// Returns a set of the last solve's assumptions that the clauses refute together, after an392    /// unsatisfiable answer. A caller maps the core back to the named assumptions it made, to393    /// report which of them conflict. The solver first records as the core the assumptions it had394    /// assigned when the conflict came. When that recorded core holds two or more assumptions, the395    /// core is the smaller set that the extra solves of core minimization certified. The core is396    /// empty when the clauses were refuted before the search began, as by two opposite unit clauses397    /// or an empty clause, after a satisfiable or unknown answer, and after any change that clears398    /// it. A recorded core of one assumption stays as it is, because core minimization runs only399    /// for two or more, so the core can hold that assumption even when the clauses alone are400    /// unsatisfiable. A conflict while the solver assigns the assumptions records only those401    /// assigned so far, so a solve under two or more assumptions can end with a core of one and no402    /// shrinking. Under a conflict limit, the core holds every assumption when the limit ran out403    /// during the drops, and it is empty with an `.unknown` answer when the limit ran out during404    /// the certifying solve. The slice stays valid until the next change to the solver.405    pub fn lastUnsatCore(self: *const Solver) []const Literal {406        return self.last_core.items;407    }408409    /// Returns the work counts of the last solve. A caller reports them beside the answer. A solve410    /// resets them at its start. After core minimization certifies a smaller core, `proof_steps`411    /// holds the certifying solve's step count, and it is the one count core minimization sets. The412    /// other counts leave out the work of the extra solves of core minimization.413    pub fn lastSolveStats(self: *const Solver) SolveStats {414        return self.last_stats;415    }416417    /// Returns the proof steps of the last solve, in order. A caller reads the steps in place, and418    /// `lastProofArtifact` makes a copy that outlives later changes. The trace holds one step per419    /// learned clause and, after an unsatisfiable answer, a final empty clause. After a satisfiable420    /// or unknown answer, the trace can still hold the steps learned during the solve. The slices421    /// stay valid until the next change to the solver.422    pub fn lastProofTrace(self: *const Solver) []const ProofStep {423        return self.proof_steps.items;424    }425426    /// Returns true when the trace is nonempty, each step follows by unit propagation from the427    /// starting clauses, the assumptions and the earlier steps, and the last step is the empty428    /// clause. A caller confirms an unsatisfiable answer in place. The check accepts every step429    /// while `has_empty_clause` is set.430    pub fn lastProofTraceValid(self: *const Solver) bool {431        if (self.proof_steps.items.len == 0) return false;432        for (self.proof_steps.items, 0..) |step, index| {433            if (!self.rupCheck(step.literals, index)) return false;434        }435        return self.proof_steps.items[self.proof_steps.items.len - 1].literals.len == 0;436    }437438    /// Returns a copy of the clauses, assumptions and steps behind the last unsatisfiable answer,439    /// allocated with `allocator` and owned by the caller, or null when the trace is empty. A440    /// caller keeps the evidence after the solver moves on, checks it with `ProofArtifact.valid`,441    /// or writes it out. The starting clauses are every clause the solver held when the solve442    /// began, learned clauses it kept included, then an empty clause when `has_empty_clause` is443    /// set. The artifact covers the solver's variable count. After a solve that learned clauses and444    /// then answered `.sat`, or `.unknown` at the main search's conflict limit, the call returns an445    /// artifact that `ProofArtifact.valid` rejects. After an `.unknown` answer from the certifying446    /// solve of core minimization, the artifact holds the refutation under every assumption of the447    /// solve, and `ProofArtifact.valid` accepts it. The call returns `error.OutOfMemory` when a448    /// copy fails, and then frees what it copied.449    pub fn lastProofArtifact(self: *const Solver, allocator: std.mem.Allocator) !?ProofArtifact {450        if (self.proof_steps.items.len == 0) return null;451        assert(self.last_stats.proof_steps == self.proof_steps.items.len);452        var artifact = ProofArtifact.init(allocator, self.assignment.items.len);453        errdefer artifact.deinit();454        const base_count = @min(self.proof_base_clause_count, self.clauses.items.len);455        for (self.clauses.items[0..base_count]) |clause| {456            try artifact.appendClause(clause.literals);457        }458        if (self.has_empty_clause) try artifact.appendClause(&.{});459        try artifact.appendAssumptions(self.proof_assumptions.items);460        for (self.proof_steps.items) |step| {461            try artifact.appendStep(step.literals);462        }463        return artifact;464    }465466    /// Decides whether the clauses and every literal of `assumptions` can all be true, and returns467    /// `.sat`, `.unsat` or `.unknown`. A caller asks a question under temporary hypotheses and468    /// learns which of them the clauses refute together. The solve assigns the assumptions first,469    /// in order, at decision level zero, and adds any variable they name that the solver lacks.470    /// After `.unsat`, `lastUnsatCore` holds one of three sets: the assumptions the solve had471    /// assigned when the conflict came, the smaller set that core minimization certified when that472    /// recorded core holds two or more, or every assumption of the solve when a conflict limit runs473    /// out while core minimization drops assumptions. When `assumptions` is nonempty, every clause474    /// added during the solve is removed when the solve returns. The solve clears the recorded475    /// core, trace and counts only after it has made room for conflict analysis, so a failure476    /// before that point leaves the old evidence in place. The call returns `error.OutOfMemory`477    /// when an allocation fails, `error.CapacityOverflow` when a size for the solve overflows478    /// `usize`, `error.InvalidProofTrace` when a learned clause or the final step fails its check,479    /// `error.InvalidConflictGraph` when conflict analysis runs out of assigned literals to resolve480    /// on, `error.InvalidUnsatCore` when the certifying solve satisfies the core, and the errors of481    /// `ConflictScratch`. The assignment stays after the call, and `value` and `literalValue` read482    /// it.483    pub fn solveWithAssumptions(self: *Solver, assumptions: []const Literal) !Status {484        return try self.solveWithAssumptionsMode(assumptions, true);485    }486487    fn solveWithAssumptionsMode(488        self: *Solver,489        assumptions: []const Literal,490        minimize_core: bool,491    ) anyerror!Status {492        const required_variables = try self.requiredVariableCount(assumptions);493        const scratch_capacity = try self.ensureConflictScratchStorage(required_variables);494        self.clearSolveEvidence();495        errdefer self.clearSolveEvidence();496        self.conflicts_since_restart = 0;497        self.next_restart_conflicts = self.restart_policy.first_conflict_interval;498        for (assumptions) |assumption| {499            try self.ensureVariable(assumption.variable());500        }501        if (self.max_learned_clauses != null) {502            self.backtrack(0);503            self.proof_base_clause_count = 0;504            self.reduceLearned(0, null);505        }506        try self.ensureLearnedStore();507        try self.ensureProofTrace();508        var conflict_scratch: ?scratch.ConflictScratch = null;509        if (scratch_capacity) |capacity| {510            const storage = self.conflictScratchStorage(capacity);511            conflict_scratch = try scratch.ConflictScratch.init(512                storage,513                .{ .variables = capacity.variables },514            );515            conflict_scratch.?.activate();516        }517        defer if (conflict_scratch) |*owner| {518            const expected_pointer = @intFromPtr(owner.storage.ptr);519            const expected_length = owner.storage.len;520            const returned = owner.deinit();521            assert(expected_pointer == @intFromPtr(returned.ptr));522            assert(expected_length == returned.len);523        };524        const retained_clause_count = self.clauses.items.len;525        defer if (assumptions.len > 0) self.discardClausesFrom(retained_clause_count);526        self.proof_base_clause_count = retained_clause_count;527        try self.proof_assumptions.appendSlice(self.allocator, assumptions);528        self.clearSearch();529        if (self.inconsistent) {530            self.recordConflict();531            try self.recordFinalProofStep();532            return .unsat;533        }534        for (assumptions, 0..) |assumption, assumption_index| {535            try self.ensureVariable(assumption.variable());536            if (!try self.enqueue(assumption, null)) {537                self.recordConflict();538                return try self.finishAssumptionUnsat(539                    assumptions[0 .. assumption_index + 1],540                    minimize_core,541                );542            }543            switch (try self.propagate()) {544                .consistent => {},545                .conflict => {546                    self.recordConflict();547                    return try self.finishAssumptionUnsat(548                        assumptions[0 .. assumption_index + 1],549                        minimize_core,550                    );551                },552            }553        }554        while (true) {555            switch (try self.propagate()) {556                .consistent => {},557                .conflict => |clause_index| {558                    self.recordConflict();559                    if (self.decisionLevel() == 0) {560                        return try self.finishAssumptionUnsat(assumptions, minimize_core);561                    }562                    if (!try self.learnFromConflict(&conflict_scratch.?, clause_index)) {563                        if (assumptions.len == 0) self.inconsistent = true;564                        return try self.finishAssumptionUnsat(assumptions, minimize_core);565                    }566                    if (self.conflict_budget) |budget| {567                        if (self.last_stats.conflicts >= budget) return .unknown;568                    }569                    self.maybeRestart();570                    continue;571                },572            }573            if (self.nextUnassignedVariable()) |variable_index| {574                try self.newDecisionLevel();575                self.last_stats.decisions += 1;576                const decision_literal = self.decisionLiteral(variable_index);577                if (self.saved_phase.items[variable_index] != .unset) {578                    self.last_stats.phase_saved_decisions += 1;579                }580                if (!try self.enqueue(decision_literal, null)) {581                    self.recordConflict();582                    try self.recordFinalProofStep();583                    return .unsat;584                }585                continue;586            }587            return .sat;588        }589    }590591    /// Returns the value of `variable_index` in the current assignment, or null when the variable592    /// is unassigned or at or above the variable count. A caller reads a satisfying assignment593    /// after `.sat`. The values form a satisfying assignment only after `.sat`.594    pub fn value(self: *const Solver, variable_index: u32) ?bool {595        if (variable_index >= self.assignment.items.len) return null;596        return switch (self.assignment.items[variable_index]) {597            .unset => null,598            .false => false,599            .true => true,600        };601    }602603    fn finishAssumptionUnsat(604        self: *Solver,605        assumptions: []const Literal,606        minimize_core: bool,607    ) anyerror!Status {608        if (assumptions.len > 0) try self.recordUnsatCore(assumptions);609        try self.recordFinalProofStep();610        if (minimize_core and assumptions.len > 1) return try self.minimizeLastUnsatCore();611        return .unsat;612    }613614    fn minimizeLastUnsatCore(self: *Solver) anyerror!Status {615        var pool: ?usize = if (self.conflict_budget) |budget| budget -| self.last_stats.conflicts else null;616        var core: std.ArrayList(Literal) = .empty;617        defer core.deinit(self.allocator);618        try core.appendSlice(self.allocator, self.last_core.items);619        var trial: std.ArrayList(Literal) = .empty;620        defer trial.deinit(self.allocator);621        var index: usize = 0;622        while (index < core.items.len) {623            if (poolDrained(pool)) break;624            trial.clearRetainingCapacity();625            for (core.items, 0..) |literal, candidate_index| {626                if (candidate_index != index) try trial.append(self.allocator, literal);627            }628            const outcome = try self.probeStatusWithAssumptions(trial.items, pool);629            drainPool(&pool, outcome.conflicts);630            if (outcome.status == .unsat) {631                core.clearRetainingCapacity();632                try core.appendSlice(self.allocator, trial.items);633            } else {634                index += 1;635            }636        }637        if (!poolDrained(pool)) {638            var probe = try self.baseProbe(pool);639            defer probe.deinit();640            const certified = try probe.solveWithAssumptionsMode(core.items, false);641            drainPool(&pool, probe.lastSolveStats().conflicts);642            switch (certified) {643                .sat => return error.InvalidUnsatCore,644                .unknown => {645                    self.last_core.clearRetainingCapacity();646                    return .unknown;647                },648                .unsat => {649                    const base_count = self.proof_base_clause_count;650                    self.clearProofTrace();651                    self.proof_base_clause_count = base_count;652                    try self.proof_assumptions.appendSlice(self.allocator, probe.lastUnsatCore());653                    for (probe.proof_steps.items) |step| {654                        try self.appendStepStorage(step.literals);655                    }656                    self.last_stats.proof_steps = self.proof_steps.items.len;657                    try self.recordUnsatCore(probe.lastUnsatCore());658                    return .unsat;659                },660            }661        }662        try self.recordUnsatCore(self.proof_assumptions.items);663        return .unsat;664    }665666    fn poolDrained(pool: ?usize) bool {667        return if (pool) |remaining| remaining == 0 else false;668    }669670    fn drainPool(pool: *?usize, spent: usize) void {671        if (pool.*) |remaining| pool.* = remaining -| spent;672    }673674    fn probeStatusWithAssumptions(675        self: *const Solver,676        assumptions: []const Literal,677        pool: ?usize,678    ) anyerror!ProbeOutcome {679        var probe = try self.baseProbe(pool);680        defer probe.deinit();681        const status = try probe.solveWithAssumptionsMode(assumptions, false);682        return .{ .status = status, .conflicts = probe.lastSolveStats().conflicts };683    }684685    fn baseProbe(self: *const Solver, pool: ?usize) anyerror!Solver {686        var probe = Solver.init(self.allocator);687        errdefer probe.deinit();688        probe.conflict_budget = pool;689        probe.proof_trace_slab = false;690        probe.max_learned_clauses = self.max_learned_clauses;691        probe.setRestartPolicy(self.restart_policy);692        for (self.clauses.items) |clause| {693            if (!clause.learned) try probe.addClause(clause.literals);694        }695        if (self.has_empty_clause) try probe.addClause(&.{});696        return probe;697    }698699    fn recordUnsatCore(self: *Solver, assumptions: []const Literal) !void {700        self.last_core.clearRetainingCapacity();701        try self.last_core.appendSlice(self.allocator, assumptions);702    }703704    fn recordConflict(self: *Solver) void {705        self.last_stats.conflicts += 1;706        self.conflicts_since_restart += 1;707        if (self.decisionLevel() == 0) self.last_stats.root_conflicts += 1;708    }709710    fn clearProofTrace(self: *Solver) void {711        if (self.proof_trace) |*owner| {712            for (self.proof_steps.items) |step| {713                if (step.literals.len == 0) continue;714                assert(owner.owns(step.literals));715            }716            owner.clear();717        } else {718            for (self.proof_steps.items) |step| {719                self.allocator.free(step.literals);720            }721        }722        self.proof_steps.clearRetainingCapacity();723        self.proof_assumptions.clearRetainingCapacity();724        self.proof_base_clause_count = 0;725    }726727    fn clearSolveEvidence(self: *Solver) void {728        self.clearProofTrace();729        self.last_core.clearRetainingCapacity();730        self.last_stats = .{};731    }732733    fn acquireStepStorage(self: *Solver, literals: []const Literal) ![]Literal {734        if (self.proof_trace) |*owner| {735            if (literals.len == 0) return owner.acquireEmpty();736            return owner.acquire(literals);737        }738        return try self.allocator.dupe(Literal, literals);739    }740741    fn appendStepStorage(self: *Solver, literals: []const Literal) !void {742        const owned = try self.acquireStepStorage(literals);743        if (self.proof_trace != null) {744            assert(self.proof_steps.items.len < self.proof_steps.capacity);745            self.proof_steps.appendAssumeCapacity(.{ .literals = owned });746            return;747        }748        errdefer self.allocator.free(owned);749        try self.proof_steps.append(self.allocator, .{ .literals = owned });750    }751752    fn appendProofStep(self: *Solver, literals: []const Literal) !void {753        try self.appendStepStorage(literals);754        self.last_stats.proof_steps += 1;755    }756757    fn removeLastProofStep(self: *Solver) void {758        const step = self.proof_steps.pop() orelse return;759        if (self.proof_trace) |*owner| {760            owner.releaseLast(step.literals);761        } else {762            self.allocator.free(step.literals);763        }764        self.last_stats.proof_steps -= 1;765    }766767    fn recordFinalProofStep(self: *Solver) !void {768        if (!self.rupCheck(&.{}, self.proof_steps.items.len)) return error.InvalidProofTrace;769        try self.appendProofStep(&.{});770    }771772    fn traceBudget(self: *const Solver) ?usize {773        if (!self.proof_trace_slab) return null;774        return self.conflict_budget;775    }776777    fn rupCheck(self: *const Solver, literals: []const Literal, proof_step_limit: usize) bool {778        if (self.has_empty_clause) return true;779        assert(self.rup_assignment.items.len == self.assignment.items.len);780        const base_count = @min(self.proof_base_clause_count, self.clauses.items.len);781        return proof.rupCheckKnownVariablesWithClauses(782            self.rup_assignment.items,783            Clause,784            self.clauses.items[0..base_count],785            self.proof_assumptions.items,786            self.proof_steps.items,787            literals,788            proof_step_limit,789        );790    }791792    fn rupCheckConflict(self: *const Solver, literals: []const Literal, conflict: usize) bool {793        return proof.rupCheckKnownVariablesWithReasons(794            self.rup_assignment.items,795            Clause,796            self.clauses.items,797            self.proof_assumptions.items,798            literals,799            .{ .trail = self.trail.items, .reasons = self.reason.items, .conflict = conflict },800        );801    }802803    fn ensureProofTrace(self: *Solver) !void {804        assert(self.proof_steps.items.len == 0);805        const budget = self.traceBudget() orelse {806            if (self.proof_trace) |*owner| {807                owner.deinit(self.allocator);808                self.proof_trace = null;809            }810            return;811        };812        const limits = trace.Trace.Limits.inspect(budget, self.variableCount());813        const required = try trace.Trace.Capacity.derive(limits);814        if (self.proof_trace) |*existing| {815            if (existing.admits(required)) {816                try self.proof_steps.ensureTotalCapacity(self.allocator, existing.capacity.steps);817                return;818            }819            existing.deinit(self.allocator);820            self.proof_trace = null;821        }822        var fresh = try trace.Trace.init(self.allocator, limits);823        fresh.activate();824        self.proof_trace = fresh;825        try self.proof_steps.ensureTotalCapacity(self.allocator, required.steps);826    }827828    fn requiredVariableCount(829        self: *const Solver,830        assumptions: []const Literal,831    ) error{CapacityOverflow}!usize {832        var required = self.variableCount();833        for (assumptions) |assumption| {834            const assumption_variables = std.math.add(835                usize,836                @as(usize, assumption.variable()),837                1,838            ) catch return error.CapacityOverflow;839            required = @max(required, assumption_variables);840        }841        return required;842    }843844    fn ensureConflictScratchStorage(845        self: *Solver,846        required_variables: usize,847    ) !?scratch.ConflictScratch.Capacity {848        if (required_variables == 0) return null;849        const limits = scratch.ConflictScratch.Limits.inspect(required_variables);850        const required = try scratch.ConflictScratch.Capacity.derive(limits);851        try self.trail.ensureTotalCapacityPrecise(852            self.allocator,853            required.trail_capacity,854        );855        return required;856    }857858    fn conflictScratchStorage(859        self: *Solver,860        capacity: scratch.ConflictScratch.Capacity,861    ) scratch.ConflictScratch.Storage {862        assert(self.trail.items.len <= capacity.variables);863        assert(self.trail.capacity >= capacity.trail_capacity);864        const backing = self.trail.allocatedSlice()[capacity.variables..capacity.trail_capacity];865        const bytes = std.mem.sliceAsBytes(backing);866        assert(bytes.len >= capacity.storage_bytes);867        return @alignCast(bytes[0..capacity.storage_bytes]);868    }869870    fn ensureLearnedStore(self: *Solver) !void {871        const limit = self.max_learned_clauses orelse {872            try self.evacuateLearnedStore();873            return;874        };875        const limits = store.Store.Limits.inspect(limit, self.variableCount());876        const required = try store.Store.Capacity.derive(limits);877        if (self.learned_store) |*existing| {878            if (existing.admits(required)) return;879        }880        var fresh = try store.Store.init(self.allocator, limits);881        fresh.activate();882        if (self.learned_store) |*old| {883            for (self.clauses.items) |*clause| {884                if (clause.storage == .pool) {885                    assert(old.owns(clause.literals));886                    clause.literals = fresh.acquire(clause.literals);887                }888            }889            old.deinit(self.allocator);890        }891        self.learned_store = fresh;892    }893894    fn evacuateLearnedStore(self: *Solver) !void {895        if (self.learned_store == null) return;896        for (self.clauses.items) |*clause| {897            if (clause.storage == .pool) {898                const heap_copy = try self.allocator.dupe(Literal, clause.literals);899                self.learnedPool().release(clause.literals);900                clause.literals = heap_copy;901                clause.storage = .heap;902            }903        }904        self.learnedPool().deinit(self.allocator);905        self.learned_store = null;906    }907908    fn maybeRestart(self: *Solver) void {909        if (self.next_restart_conflicts != 0 and910            self.decisionLevel() > 0 and911            self.conflicts_since_restart >= self.next_restart_conflicts)912        {913            self.backtrack(0);914            self.last_stats.restarts += 1;915            self.conflicts_since_restart = 0;916            if (self.restart_policy.growth > 1) {917                self.next_restart_conflicts = std.math.mul(918                    usize,919                    self.next_restart_conflicts,920                    self.restart_policy.growth,921                ) catch std.math.maxInt(usize);922            }923        }924        const limit = self.max_learned_clauses orelse return;925        if (self.replaceableLearnedClauses() <= limit) return;926        assert(self.clauses.items.len > 0);927        if (self.decisionLevel() > 0) {928            self.backtrack(0);929            self.last_stats.restarts += 1;930            self.conflicts_since_restart = 0;931        }932        const just_learned = self.clauses.items.len - 1;933        const protected = if (just_learned >= self.proof_base_clause_count) just_learned else null;934        self.reduceLearned(self.proof_base_clause_count, protected);935    }936937    fn reduceLearned(self: *Solver, first_candidate: usize, protected: ?usize) void {938        const limit = self.max_learned_clauses orelse return;939        assert(self.decisionLevel() == 0);940        assert(first_candidate >= self.proof_base_clause_count);941        assert(self.learned_clause_count == self.countLearnedClauses());942        assert(self.glue_clause_count == self.countGlueClauses());943        var bound = self.clauses.items.len;944        while (self.replaceableLearnedClauses() > limit and bound > 0) : (bound -= 1) {945            const victim = self.selectVictim(first_candidate, protected) orelse break;946            self.removeLearnedClause(victim);947            self.last_stats.evicted_clauses += 1;948        }949    }950951    fn selectVictim(self: *const Solver, first_candidate: usize, protected: ?usize) ?usize {952        assert(first_candidate <= self.clauses.items.len);953        var worst: ?usize = null;954        for (self.clauses.items[first_candidate..], first_candidate..) |clause, clause_index| {955            if (!clause.learned) continue;956            if (clause.lbd <= glue_lbd_max) continue;957            if (protected == clause_index) continue;958            if (self.clauseLocked(clause_index)) continue;959            if (worst) |current| {960                if (self.evictsBefore(clause_index, current)) worst = clause_index;961            } else {962                worst = clause_index;963            }964        }965        return worst;966    }967968    fn evictsBefore(self: *const Solver, left_index: usize, right_index: usize) bool {969        const left = self.clauses.items[left_index];970        const right = self.clauses.items[right_index];971        if (left.lbd != right.lbd) return left.lbd > right.lbd;972        return left.literals.len > right.literals.len;973    }974975    fn countLearnedClauses(self: *const Solver) usize {976        var count: usize = 0;977        for (self.clauses.items) |clause| {978            if (clause.learned) count += 1;979        }980        return count;981    }982983    fn countGlueClauses(self: *const Solver) usize {984        var count: usize = 0;985        for (self.clauses.items) |clause| {986            if (clause.learned and clause.lbd <= glue_lbd_max) count += 1;987        }988        return count;989    }990991    /// Returns the value of `literal` in the current assignment: `.true`, `.false`, or `.unset`992    /// when its variable is unassigned or at or above the variable count. `bitvec.Encoder` reads993    /// each Boolean of a model through it. The values form a satisfying assignment only after994    /// `.sat`.995    pub fn literalValue(self: *const Solver, literal: Literal) BoolValue {996        if (literal.variable() >= self.assignment.items.len) return .unset;997        const assigned = self.assignment.items[literal.variable()];998        return if (literal.isPositive()) assigned else assigned.invert();999    }10001001    fn ensureVariable(self: *Solver, variable_index: u32) !void {1002        const needed = @as(usize, variable_index) + 1;1003        while (self.assignment.items.len < needed) {1004            try self.assignment.append(self.allocator, .unset);1005            errdefer _ = self.assignment.pop();1006            try self.saved_phase.append(self.allocator, .unset);1007            errdefer _ = self.saved_phase.pop();1008            try self.level.append(self.allocator, 0);1009            errdefer _ = self.level.pop();1010            try self.reason.append(self.allocator, null);1011            errdefer _ = self.reason.pop();1012            try self.rup_assignment.append(self.allocator, .unset);1013            errdefer _ = self.rup_assignment.pop();1014            try self.watches.append(self.allocator, .empty);1015            errdefer {1016                var removed = self.watches.pop().?;1017                removed.deinit(self.allocator);1018            }1019            try self.watches.append(self.allocator, .empty);1020        }1021    }10221023    fn addWatch(self: *Solver, literal: Literal, clause_index: usize) !void {1024        try self.watches.items[literal.index()].append(self.allocator, .{ .index = clause_index });1025    }10261027    fn removeWatch(self: *Solver, literal: Literal, clause_index: usize) bool {1028        const watch = &self.watches.items[literal.index()];1029        for (watch.items, 0..) |clause_ref, index| {1030            if (clause_ref.index == clause_index) {1031                _ = watch.swapRemove(index);1032                return true;1033            }1034        }1035        return false;1036    }10371038    fn patchWatch(self: *Solver, literal: Literal, from_index: usize, to_index: usize) void {1039        const watch = &self.watches.items[literal.index()];1040        for (watch.items) |*clause_ref| {1041            if (clause_ref.index == from_index) {1042                clause_ref.index = to_index;1043                return;1044            }1045        }1046        unreachable;1047    }10481049    fn clauseLocked(self: *const Solver, clause_index: usize) bool {1050        assert(clause_index < self.clauses.items.len);1051        for (self.trail.items) |trail_literal| {1052            const variable_index = trail_literal.variable();1053            if (self.reason.items[variable_index]) |reason_index| {1054                if (reason_index == clause_index) return true;1055            }1056        }1057        return false;1058    }10591060    fn removeLearnedClause(self: *Solver, clause_index: usize) void {1061        assert(self.decisionLevel() == 0);1062        assert(clause_index >= self.proof_base_clause_count);1063        assert(clause_index < self.clauses.items.len);1064        const clause = self.clauses.items[clause_index];1065        assert(clause.learned);1066        assert(!self.clauseLocked(clause_index));1067        const removed_first = self.removeWatch(clause.literals[clause.watch_a], clause_index);1068        assert(removed_first);1069        if (clause.watch_b != clause.watch_a) {1070            const removed_second = self.removeWatch(clause.literals[clause.watch_b], clause_index);1071            assert(removed_second);1072        }1073        const last_index = self.clauses.items.len - 1;1074        _ = self.clauses.swapRemove(clause_index);1075        if (clause_index != last_index) {1076            const moved = self.clauses.items[clause_index];1077            self.patchWatch(moved.literals[moved.watch_a], last_index, clause_index);1078            if (moved.watch_b != moved.watch_a) {1079                self.patchWatch(moved.literals[moved.watch_b], last_index, clause_index);1080            }1081            for (self.trail.items) |trail_literal| {1082                const variable_index = trail_literal.variable();1083                if (self.reason.items[variable_index]) |reason_index| {1084                    if (reason_index == last_index) {1085                        self.reason.items[variable_index] = clause_index;1086                    }1087                }1088            }1089        }1090        assert(self.learned_clause_count > 0);1091        self.learned_clause_count -= 1;1092        if (clause.lbd <= glue_lbd_max) {1093            assert(self.glue_clause_count > 0);1094            self.glue_clause_count -= 1;1095        }1096        self.freeClauseLiterals(clause);1097    }10981099    fn clearSearch(self: *Solver) void {1100        for (self.assignment.items) |*item| item.* = .unset;1101        for (self.level.items) |*item| item.* = 0;1102        for (self.reason.items) |*item| item.* = null;1103        self.trail.clearRetainingCapacity();1104        self.decision_limits.clearRetainingCapacity();1105        self.propagation_cursor = 0;1106        for (self.clauses.items, 0..) |clause, clause_index| {1107            if (clause.literals.len == 1) {1108                if (!(self.enqueue(clause.literals[0], clause_index) catch false)) {1109                    self.inconsistent = true;1110                    return;1111                }1112            }1113        }1114    }11151116    fn discardClausesFrom(self: *Solver, retained_clause_count: usize) void {1117        while (self.clauses.items.len > retained_clause_count) {1118            const clause_index = self.clauses.items.len - 1;1119            const clause = self.clauses.pop().?;1120            _ = self.removeWatch(clause.literals[clause.watch_a], clause_index);1121            if (clause.watch_b != clause.watch_a) {1122                _ = self.removeWatch(clause.literals[clause.watch_b], clause_index);1123            }1124            if (clause.learned) {1125                assert(self.learned_clause_count > 0);1126                self.learned_clause_count -= 1;1127                if (clause.lbd <= glue_lbd_max) {1128                    assert(self.glue_clause_count > 0);1129                    self.glue_clause_count -= 1;1130                }1131            }1132            self.freeClauseLiterals(clause);1133        }1134    }11351136    fn freeClauseLiterals(self: *Solver, clause: Clause) void {1137        switch (clause.storage) {1138            .heap => self.allocator.free(clause.literals),1139            .pool => self.learnedPool().release(clause.literals),1140        }1141    }11421143    fn learnedPool(self: *Solver) *store.Store {1144        assert(self.learned_store != null);1145        return &self.learned_store.?;1146    }11471148    fn decisionLevel(self: *const Solver) u32 {1149        return @intCast(self.decision_limits.items.len);1150    }11511152    fn newDecisionLevel(self: *Solver) !void {1153        try self.decision_limits.append(self.allocator, self.trail.items.len);1154        const level = self.decisionLevel();1155        if (level > self.last_stats.max_decision_level) {1156            self.last_stats.max_decision_level = level;1157        }1158    }11591160    fn backtrack(self: *Solver, target_level: u32) void {1161        while (self.decisionLevel() > target_level) {1162            const start = self.decision_limits.pop().?;1163            var index = self.trail.items.len;1164            while (index > start) {1165                index -= 1;1166                const variable_index = self.trail.items[index].variable();1167                self.assignment.items[variable_index] = .unset;1168                self.reason.items[variable_index] = null;1169                self.level.items[variable_index] = 0;1170            }1171            self.trail.shrinkRetainingCapacity(start);1172            if (self.propagation_cursor > start) self.propagation_cursor = start;1173        }1174    }11751176    fn enqueue(self: *Solver, literal: Literal, reason: ?usize) !bool {1177        const variable_index = literal.variable();1178        assert(variable_index < self.variableCount());1179        const current = self.literalValue(literal);1180        if (current == .true) return true;1181        if (current == .false) return false;1182        self.assignment.items[variable_index] = BoolValue.fromBool(literal.isPositive());1183        self.saved_phase.items[variable_index] = self.assignment.items[variable_index];1184        self.level.items[variable_index] = self.decisionLevel();1185        self.reason.items[variable_index] = reason;1186        try self.trail.append(self.allocator, literal);1187        return true;1188    }11891190    fn propagate(self: *Solver) !PropagationResult {1191        while (self.propagation_cursor < self.trail.items.len) {1192            const literal = self.trail.items[self.propagation_cursor];1193            self.propagation_cursor += 1;1194            const false_literal = literal.negated();1195            const watch = &self.watches.items[false_literal.index()];1196            var index: usize = 0;1197            while (index < watch.items.len) {1198                const clause_index = watch.items[index].index;1199                const update = try self.propagateClause(clause_index, false_literal);1200                switch (update) {1201                    .moved => {1202                        _ = watch.swapRemove(index);1203                    },1204                    .kept => {1205                        index += 1;1206                    },1207                    .unit => |unit_literal| {1208                        if (!try self.enqueue(unit_literal, clause_index)) {1209                            return .{ .conflict = clause_index };1210                        }1211                        self.last_stats.propagations += 1;1212                        index += 1;1213                    },1214                    .conflict => return .{ .conflict = clause_index },1215                }1216            }1217        }1218        return .consistent;1219    }12201221    fn propagateClause(1222        self: *Solver,1223        clause_index: usize,1224        false_literal: Literal,1225    ) !ClausePropagation {1226        var clause = &self.clauses.items[clause_index];1227        const false_watch_is_a = clause.literals[clause.watch_a].raw == false_literal.raw;1228        const false_watch = if (false_watch_is_a) clause.watch_a else clause.watch_b;1229        const other_watch = if (false_watch_is_a) clause.watch_b else clause.watch_a;1230        const other_literal = clause.literals[other_watch];1231        if (self.literalValue(other_literal) == .true) return .kept;1232        for (clause.literals, 0..) |candidate, candidate_index| {1233            if (candidate_index == other_watch or candidate_index == false_watch) continue;1234            if (self.literalValue(candidate) != .false) {1235                if (false_watch_is_a) {1236                    clause.watch_a = candidate_index;1237                } else {1238                    clause.watch_b = candidate_index;1239                }1240                try self.addWatch(candidate, clause_index);1241                return .moved;1242            }1243        }1244        return switch (self.literalValue(other_literal)) {1245            .unset => .{ .unit = other_literal },1246            .false => .conflict,1247            .true => .kept,1248        };1249    }12501251    fn learnFromConflict(1252        self: *Solver,1253        owner: *scratch.ConflictScratch,1254        clause_index: usize,1255    ) !bool {1256        assert(owner.capacity.variables == self.variableCount());1257        const storage = self.conflictScratchStorage(owner.capacity);1258        assert(storage.ptr == owner.storage.ptr);1259        assert(storage.len == owner.storage.len);1260        var loan: scratch.ConflictScratch.Loan = undefined;1261        try owner.acquire(self.variableCount(), &loan);1262        defer owner.release(&loan) catch unreachable;1263        const conflict_level = self.decisionLevel();1264        var path_count: usize = 0;1265        var clause_ref = clause_index;1266        var cursor = self.trail.items.len;1267        var resolved_literal: ?Literal = null;1268        while (true) {1269            try loan.recordResolution();1270            const clause = self.clauses.items[clause_ref];1271            for (clause.literals) |literal| {1272                const variable_index = literal.variable();1273                if (!try loan.markSeen(variable_index)) continue;1274                if (self.level.items[variable_index] == conflict_level) {1275                    path_count += 1;1276                } else {1277                    try loan.append(literal);1278                }1279            }1280            while (cursor > 0) {1281                cursor -= 1;1282                const trail_literal = self.trail.items[cursor];1283                if (try loan.isSeen(trail_literal.variable())) {1284                    resolved_literal = trail_literal;1285                    break;1286                }1287            }1288            const pivot = resolved_literal orelse return error.InvalidConflictGraph;1289            try loan.clearSeen(pivot.variable());1290            path_count -= 1;1291            if (path_count == 0) {1292                try loan.append(pivot.negated());1293                break;1294            }1295            clause_ref = self.reason.items[pivot.variable()] orelse {1296                try loan.append(pivot.negated());1297                break;1298            };1299        }1300        const learned = try loan.literals();1301        var backtrack_level: u32 = 0;1302        for (learned) |literal| {1303            const literal_level = self.level.items[literal.variable()];1304            if (literal_level != conflict_level and literal_level > backtrack_level) {1305                backtrack_level = literal_level;1306            }1307        }1308        const lbd = self.blockDistance(learned);1309        if (!self.rupCheckConflict(learned, clause_index)) return error.InvalidProofTrace;1310        self.backtrack(backtrack_level);1311        const assert_literal = learned[learned.len - 1];1312        try self.addLearnedClause(learned, lbd);1313        return try self.enqueue(assert_literal, self.clauses.items.len - 1);1314    }13151316    fn blockDistance(self: *const Solver, literals: []const Literal) u32 {1317        assert(literals.len > 0);1318        var distinct: u32 = 0;1319        for (literals, 0..) |literal, index| {1320            const literal_level = self.level.items[literal.variable()];1321            var counted = false;1322            for (literals[0..index]) |prior| {1323                if (self.level.items[prior.variable()] == literal_level) {1324                    counted = true;1325                    break;1326                }1327            }1328            if (!counted) distinct += 1;1329        }1330        assert(distinct >= 1);1331        assert(distinct <= literals.len);1332        return distinct;1333    }13341335    fn addLearnedClause(self: *Solver, literals: []const Literal, lbd: u32) !void {1336        assert(lbd >= 1);1337        assert(lbd <= literals.len);1338        try self.appendProofStep(literals);1339        errdefer self.removeLastProofStep();1340        const pooled = self.learned_store != null and lbd > glue_lbd_max;1341        const owned = if (pooled)1342            self.learnedPool().acquire(literals)1343        else1344            try self.allocator.dupe(Literal, literals);1345        errdefer if (pooled) self.learnedPool().release(owned) else self.allocator.free(owned);1346        const clause_index = self.clauses.items.len;1347        const clause = Clause{1348            .literals = owned,1349            .learned = true,1350            .lbd = lbd,1351            .storage = if (pooled) .pool else .heap,1352            .watch_a = 0,1353            .watch_b = if (owned.len > 1) 1 else 0,1354        };1355        try self.clauses.append(self.allocator, clause);1356        errdefer _ = self.clauses.pop();1357        try self.addWatch(owned[0], clause_index);1358        errdefer _ = self.removeWatch(owned[0], clause_index);1359        if (owned.len > 1) {1360            try self.addWatch(owned[1], clause_index);1361        }1362        self.learned_clause_count += 1;1363        if (lbd <= glue_lbd_max) self.glue_clause_count += 1;1364        self.last_stats.learned_clauses += 1;1365    }13661367    fn nextUnassignedVariable(self: *const Solver) ?u32 {1368        for (self.assignment.items, 0..) |assigned_value, index| {1369            if (assigned_value == .unset) return @intCast(index);1370        }1371        return null;1372    }13731374    fn decisionLiteral(self: *const Solver, variable_index: u32) Literal {1375        return switch (self.saved_phase.items[variable_index]) {1376            .false => Literal.negative(variable_index),1377            .true, .unset => Literal.positive(variable_index),1378        };1379    }1380};13811382fn countWatchRefs(solver: *const Solver, literal: Literal, clause_index: usize) usize {1383    var count: usize = 0;1384    for (solver.watches.items[literal.index()].items) |clause_ref| {1385        if (clause_ref.index == clause_index) count += 1;1386    }1387    return count;1388}13891390fn expectWatchInvariant(solver: *const Solver) !void {1391    var total_refs: usize = 0;1392    for (solver.watches.items) |watch| {1393        for (watch.items) |clause_ref| {1394            try std.testing.expect(clause_ref.index < solver.clauses.items.len);1395        }1396        total_refs += watch.items.len;1397    }1398    var expected_refs: usize = 0;1399    for (solver.clauses.items, 0..) |clause, clause_index| {1400        const first = clause.literals[clause.watch_a];1401        if (clause.watch_b != clause.watch_a) {1402            expected_refs += 2;1403            const second = clause.literals[clause.watch_b];1404            if (second.raw == first.raw) {1405                try std.testing.expectEqual(1406                    @as(usize, 2),1407                    countWatchRefs(solver, first, clause_index),1408                );1409            } else {1410                try std.testing.expectEqual(1411                    @as(usize, 1),1412                    countWatchRefs(solver, first, clause_index),1413                );1414                try std.testing.expectEqual(1415                    @as(usize, 1),1416                    countWatchRefs(solver, second, clause_index),1417                );1418            }1419        } else {1420            expected_refs += 1;1421            try std.testing.expectEqual(1422                @as(usize, 1),1423                countWatchRefs(solver, first, clause_index),1424            );1425        }1426    }1427    try std.testing.expectEqual(expected_refs, total_refs);1428}14291430fn expectReasonInvariant(solver: *const Solver) !void {1431    for (solver.trail.items) |trail_literal| {1432        const variable_index = trail_literal.variable();1433        if (solver.reason.items[variable_index]) |reason_index| {1434            try std.testing.expect(reason_index < solver.clauses.items.len);1435            var found = false;1436            for (solver.clauses.items[reason_index].literals) |literal| {1437                if (literal.raw == trail_literal.raw) found = true;1438            }1439            try std.testing.expect(found);1440        }1441    }1442}14431444fn appendStoreClause(solver: *Solver, literals: []const Literal, lbd: u32) !usize {1445    for (literals) |literal| try solver.ensureVariable(literal.variable());1446    const owned = try solver.allocator.dupe(Literal, literals);1447    const clause_index = solver.clauses.items.len;1448    try solver.clauses.append(solver.allocator, .{1449        .literals = owned,1450        .learned = true,1451        .lbd = lbd,1452        .storage = .heap,1453        .watch_a = 0,1454        .watch_b = if (owned.len > 1) 1 else 0,1455    });1456    try solver.addWatch(owned[0], clause_index);1457    if (owned.len > 1) try solver.addWatch(owned[1], clause_index);1458    solver.learned_clause_count += 1;1459    if (lbd <= glue_lbd_max) solver.glue_clause_count += 1;1460    return clause_index;1461}14621463fn retainedShapes(solver: *const Solver, buffer: [][2]u32) usize {1464    var count: usize = 0;1465    for (solver.clauses.items) |clause| {1466        if (!clause.learned) continue;1467        buffer[count] = .{ clause.lbd, @intCast(clause.literals.len) };1468        count += 1;1469    }1470    std.mem.sort([2]u32, buffer[0..count], {}, shapeLessThan);1471    return count;1472}14731474fn shapeLessThan(context: void, left: [2]u32, right: [2]u32) bool {1475    _ = context;1476    if (left[0] != right[0]) return left[0] < right[0];1477    return left[1] < right[1];1478}14791480test "eviction removes worst lbd first then longest and never glue" {1481    comptime {1482        @stardustClaim(1483            @import("alloc_phase").capacity.witness(@import("./root.zig").LearnedStore, "smt_victim_order"),1484            null,1485            null,1486            null,1487            null,1488            null,1489            null,1490        );1491    }14921493    var solver = Solver.init(std.testing.allocator);1494    defer solver.deinit();1495    for (0..7) |_| _ = try solver.addVariable();1496    try solver.addClause(&.{ Literal.positive(0), Literal.positive(1) });1497    _ = try appendStoreClause(&solver, &.{1498        Literal.positive(0), Literal.negative(1), Literal.positive(2),1499    }, 5);1500    _ = try appendStoreClause(&solver, &.{1501        Literal.negative(0), Literal.positive(1), Literal.negative(2), Literal.positive(3),1502        Literal.negative(3), Literal.positive(4), Literal.positive(5),1503    }, 3);1504    _ = try appendStoreClause(&solver, &.{1505        Literal.negative(4), Literal.positive(5), Literal.negative(6), Literal.positive(6),1506    }, 3);1507    _ = try appendStoreClause(&solver, &.{ Literal.negative(5), Literal.positive(6) }, 2);1508    _ = try appendStoreClause(&solver, &.{Literal.negative(6)}, 1);1509    try std.testing.expectEqual(@as(usize, 5), solver.retainedLearnedClauses());1510    try std.testing.expectEqual(@as(usize, 3), solver.replaceableLearnedClauses());15111512    solver.max_learned_clauses = 1;1513    solver.reduceLearned(1, null);1514    try std.testing.expectEqual(@as(usize, 1), solver.replaceableLearnedClauses());1515    try std.testing.expectEqual(@as(usize, 2), solver.last_stats.evicted_clauses);1516    var shapes: [8][2]u32 = undefined;1517    var shape_count = retainedShapes(&solver, &shapes);1518    try std.testing.expectEqual(@as(usize, 3), shape_count);1519    try std.testing.expectEqualSlices(u32, &.{ 1, 1 }, &shapes[0]);1520    try std.testing.expectEqualSlices(u32, &.{ 2, 2 }, &shapes[1]);1521    try std.testing.expectEqualSlices(u32, &.{ 3, 4 }, &shapes[2]);1522    try expectWatchInvariant(&solver);15231524    solver.max_learned_clauses = 0;1525    solver.reduceLearned(1, null);1526    try std.testing.expectEqual(@as(usize, 0), solver.replaceableLearnedClauses());1527    try std.testing.expectEqual(@as(usize, 2), solver.retainedLearnedClauses());1528    try std.testing.expectEqual(@as(usize, 3), solver.last_stats.evicted_clauses);1529    shape_count = retainedShapes(&solver, &shapes);1530    try std.testing.expectEqual(@as(usize, 2), shape_count);1531    try std.testing.expectEqualSlices(u32, &.{ 1, 1 }, &shapes[0]);1532    try std.testing.expectEqualSlices(u32, &.{ 2, 2 }, &shapes[1]);1533    try expectWatchInvariant(&solver);1534}15351536test "eviction skips locked and protected clauses" {1537    var solver = Solver.init(std.testing.allocator);1538    defer solver.deinit();1539    for (0..3) |_| _ = try solver.addVariable();1540    const locked_index = try appendStoreClause(&solver, &.{1541        Literal.positive(0), Literal.positive(1),1542    }, 5);1543    const protected_index = try appendStoreClause(&solver, &.{1544        Literal.positive(1), Literal.positive(2),1545    }, 4);1546    const victim_index = try appendStoreClause(&solver, &.{1547        Literal.positive(2), Literal.positive(0),1548    }, 3);1549    _ = victim_index;1550    try std.testing.expect(try solver.enqueue(Literal.positive(0), locked_index));1551    try std.testing.expect(solver.clauseLocked(locked_index));15521553    solver.max_learned_clauses = 0;1554    solver.reduceLearned(0, protected_index);1555    try std.testing.expectEqual(@as(usize, 2), solver.retainedLearnedClauses());1556    try std.testing.expectEqual(@as(usize, 2), solver.replaceableLearnedClauses());1557    try std.testing.expectEqual(@as(usize, 1), solver.last_stats.evicted_clauses);1558    var shapes: [4][2]u32 = undefined;1559    const shape_count = retainedShapes(&solver, &shapes);1560    try std.testing.expectEqual(@as(usize, 2), shape_count);1561    try std.testing.expectEqualSlices(u32, &.{ 4, 2 }, &shapes[0]);1562    try std.testing.expectEqualSlices(u32, &.{ 5, 2 }, &shapes[1]);1563}15641565test "bounded solve preserves status and proof under eviction" {1566    comptime {1567        @stardustClaim(1568            @import("alloc_phase").capacity.witness(@import("./root.zig").LearnedStore, "smt_bounded_solve"),1569            null,1570            null,1571            null,1572            null,1573            null,1574            null,1575        );1576    }1577    comptime {1578        @stardustClaim(1579            @import("alloc_phase").capacity.witness(@import("./root.zig").ProofTrace, "smt_trace_bounded_solve"),1580            null,1581            null,1582            null,1583            null,1584            null,1585            null,1586        );1587    }15881589    var solver = Solver.init(std.testing.allocator);1590    defer solver.deinit();1591    const learned_limit: usize = 6;1592    solver.max_learned_clauses = learned_limit;1593    solver.conflict_budget = 200_000;1594    solver.setRestartPolicy(.{ .first_conflict_interval = 1, .growth = 2 });1595    const pigeons: u32 = 5;1596    const holes: u32 = 4;1597    for (0..pigeons * holes) |_| _ = try solver.addVariable();1598    for (0..pigeons) |pigeon| {1599        var placement: [holes]Literal = undefined;1600        for (&placement, 0..) |*literal, hole| {1601            literal.* = Literal.positive(@intCast(pigeon * holes + hole));1602        }1603        try solver.addClause(&placement);1604    }1605    for (0..holes) |hole| {1606        for (0..pigeons) |first| {1607            for (first + 1..pigeons) |second| {1608                try solver.addClause(&.{1609                    Literal.negative(@intCast(first * holes + hole)),1610                    Literal.negative(@intCast(second * holes + hole)),1611                });1612            }1613        }1614    }1615    try std.testing.expectEqual(Status.unsat, try solver.solve());1616    const first_stats = solver.lastSolveStats();1617    try std.testing.expect(first_stats.evicted_clauses > 0);1618    try std.testing.expect(solver.replaceableLearnedClauses() <= learned_limit + 1);1619    try std.testing.expect(solver.lastProofTraceValid());1620    try expectPooledStorageInvariant(&solver);1621    try std.testing.expectEqual(Status.unsat, try solver.solve());1622    try std.testing.expect(solver.replaceableLearnedClauses() <= learned_limit + 1);1623    try std.testing.expect(solver.lastProofTraceValid());1624    try expectPooledStorageInvariant(&solver);1625}16261627fn expectPooledStorageInvariant(solver: *Solver) !void {1628    const pool = solver.learnedPool();1629    var pooled_clauses: usize = 0;1630    for (solver.clauses.items) |clause| {1631        switch (clause.storage) {1632            .pool => {1633                pooled_clauses += 1;1634                try std.testing.expect(clause.learned);1635                try std.testing.expect(clause.lbd > glue_lbd_max);1636                try std.testing.expect(pool.owns(clause.literals));1637            },1638            .heap => try std.testing.expect(!pool.owns(clause.literals)),1639        }1640    }1641    try std.testing.expectEqual(1642        solver.replaceableLearnedClauses(),1643        pooled_clauses,1644    );1645    try std.testing.expectEqual(1646        pool.capacity.slots - pooled_clauses,1647        pool.freeSlots(),1648    );1649}16501651test "learned store pool survives variable growth and cap removal" {1652    comptime {1653        @stardustClaim(1654            @import("alloc_phase").capacity.witness(@import("./root.zig").LearnedStore, "smt_pool_lifecycle"),1655            null,1656            null,1657            null,1658            null,1659            null,1660            null,1661        );1662    }16631664    var solver = Solver.init(std.testing.allocator);1665    defer solver.deinit();1666    solver.max_learned_clauses = 2;1667    solver.setRestartPolicy(.{ .first_conflict_interval = 1, .growth = 1 });1668    const a = try solver.addVariable();1669    const b = try solver.addVariable();1670    const c = try solver.addVariable();1671    try solver.addClause(&.{ Literal.negative(a), Literal.negative(b), Literal.positive(c) });1672    try solver.addClause(&.{ Literal.negative(a), Literal.negative(b), Literal.negative(c) });1673    try std.testing.expectEqual(Status.sat, try solver.solve());1674    const first_capacity = solver.learnedPool().capacity;1675    try std.testing.expectEqual(@as(usize, 3 + 1 + 2), first_capacity.slots);16761677    for (0..4) |_| _ = try solver.addVariable();1678    try std.testing.expectEqual(Status.sat, try solver.solve());1679    const grown_capacity = solver.learnedPool().capacity;1680    try std.testing.expectEqual(@as(usize, 7 + 1 + 2), grown_capacity.slots);1681    try std.testing.expectEqual(@as(usize, 7), grown_capacity.slot_width);1682    try expectPooledStorageInvariant(&solver);1683    try expectWatchInvariant(&solver);16841685    solver.max_learned_clauses = null;1686    try std.testing.expectEqual(Status.sat, try solver.solve());1687    try std.testing.expect(solver.learned_store == null);1688    for (solver.clauses.items) |clause| {1689        try std.testing.expectEqual(ClauseStorage.heap, clause.storage);1690    }1691    try expectWatchInvariant(&solver);1692}16931694fn expectTraceStorageInvariant(solver: *const Solver) !void {1695    const owner = &solver.proof_trace.?;1696    try std.testing.expectEqual(solver.proof_steps.items.len, owner.step_count);1697    var slab_literals: usize = 0;1698    for (solver.proof_steps.items) |step| {1699        if (step.literals.len == 0) continue;1700        try std.testing.expect(owner.owns(step.literals));1701        slab_literals += step.literals.len;1702    }1703    try std.testing.expectEqual(slab_literals, owner.literal_count);1704    try std.testing.expect(owner.step_count <= owner.capacity.steps);1705}17061707test "budgeted solve keeps proof steps in the trace slab" {1708    comptime {1709        @stardustClaim(1710            @import("alloc_phase").capacity.witness(@import("./root.zig").ProofTrace, "smt_trace_slab_solve"),1711            null,1712            null,1713            null,1714            null,1715            null,1716            null,1717        );1718    }17191720    var solver = Solver.init(std.testing.allocator);1721    defer solver.deinit();1722    solver.conflict_budget = 64;1723    const a = try solver.addVariable();1724    const b = try solver.addVariable();1725    const c = try solver.addVariable();1726    try solver.addClause(&.{ Literal.positive(a), Literal.positive(b) });1727    try solver.addClause(&.{ Literal.positive(a), Literal.negative(b) });1728    try solver.addClause(&.{ Literal.negative(a), Literal.positive(c) });1729    try solver.addClause(&.{ Literal.negative(a), Literal.negative(c) });1730    try std.testing.expectEqual(Status.unsat, try solver.solve());1731    try std.testing.expect(solver.lastProofTraceValid());1732    try std.testing.expect(solver.proof_steps.items.len >= 2);1733    try expectTraceStorageInvariant(&solver);17341735    const first_slab = solver.proof_trace.?.slab.ptr;1736    try std.testing.expectEqual(Status.unsat, try solver.solve());1737    try std.testing.expect(solver.lastProofTraceValid());1738    try expectTraceStorageInvariant(&solver);1739    try std.testing.expectEqual(first_slab, solver.proof_trace.?.slab.ptr);1740}17411742test "proof trace survives budget growth and removal" {1743    comptime {1744        @stardustClaim(1745            @import("alloc_phase").capacity.witness(@import("./root.zig").ProofTrace, "smt_trace_lifecycle"),1746            null,1747            null,1748            null,1749            null,1750            null,1751            null,1752        );1753    }17541755    var solver = Solver.init(std.testing.allocator);1756    defer solver.deinit();1757    solver.conflict_budget = 4;1758    const a = try solver.addVariable();1759    const b = try solver.addVariable();1760    try solver.addClause(&.{ Literal.positive(a), Literal.positive(b) });1761    try solver.addClause(&.{ Literal.positive(a), Literal.negative(b) });1762    try solver.addClause(&.{ Literal.negative(a), Literal.positive(b) });1763    try solver.addClause(&.{ Literal.negative(a), Literal.negative(b) });1764    try std.testing.expectEqual(Status.unsat, try solver.solve());1765    try std.testing.expect(solver.lastProofTraceValid());1766    const first_capacity = solver.proof_trace.?.capacity;1767    try std.testing.expectEqual(@as(usize, 6), first_capacity.steps);1768    try expectTraceStorageInvariant(&solver);17691770    solver.conflict_budget = 32;1771    try std.testing.expectEqual(Status.unsat, try solver.solve());1772    try std.testing.expect(solver.lastProofTraceValid());1773    try std.testing.expectEqual(@as(usize, 34), solver.proof_trace.?.capacity.steps);1774    try expectTraceStorageInvariant(&solver);17751776    solver.conflict_budget = null;1777    try std.testing.expectEqual(Status.unsat, try solver.solve());1778    try std.testing.expect(solver.lastProofTraceValid());1779    try std.testing.expect(solver.proof_trace == null);1780    for (solver.proof_steps.items) |step| {1781        std.mem.doNotOptimizeAway(step.literals.len);1782    }1783}17841785test "entry eviction enforces a newly set cap" {1786    var solver = Solver.init(std.testing.allocator);1787    defer solver.deinit();1788    const a = try solver.addVariable();1789    const b = try solver.addVariable();1790    try solver.addClause(&.{ Literal.positive(a), Literal.positive(b) });1791    _ = try appendStoreClause(&solver, &.{ Literal.positive(a), Literal.negative(b) }, 4);1792    _ = try appendStoreClause(&solver, &.{ Literal.negative(a), Literal.positive(b) }, 3);1793    try std.testing.expectEqual(@as(usize, 2), solver.replaceableLearnedClauses());1794    solver.max_learned_clauses = 0;1795    try std.testing.expectEqual(Status.sat, try solver.solve());1796    try std.testing.expectEqual(@as(usize, 0), solver.replaceableLearnedClauses());1797    try std.testing.expectEqual(@as(usize, 0), solver.retainedLearnedClauses());1798    try std.testing.expectEqual(@as(usize, 2), solver.lastSolveStats().evicted_clauses);1799    try expectWatchInvariant(&solver);1800}18011802test "removing a learned clause preserves base prefix and behavior" {1803    var solver = Solver.init(std.testing.allocator);1804    defer solver.deinit();1805    const a = try solver.addVariable();1806    const b = try solver.addVariable();1807    const c = try solver.addVariable();1808    _ = c;1809    try solver.addClause(&.{ Literal.negative(a), Literal.negative(b), Literal.positive(2) });1810    try solver.addClause(&.{ Literal.negative(a), Literal.negative(b), Literal.negative(2) });1811    try std.testing.expectEqual(Status.sat, try solver.solve());1812    try std.testing.expectEqual(@as(usize, 3), solver.clauses.items.len);1813    try std.testing.expect(solver.clauses.items[2].learned);1814    const base_first = solver.clauses.items[0].literals;1815    const base_second = solver.clauses.items[1].literals;1816    solver.backtrack(0);1817    solver.removeLearnedClause(2);1818    try std.testing.expectEqual(@as(usize, 2), solver.clauses.items.len);1819    try std.testing.expectEqual(base_first.ptr, solver.clauses.items[0].literals.ptr);1820    try std.testing.expectEqual(base_second.ptr, solver.clauses.items[1].literals.ptr);1821    try expectWatchInvariant(&solver);1822    try expectReasonInvariant(&solver);1823    try std.testing.expectEqual(Status.sat, try solver.solve());1824}18251826test "removing a middle learned clause patches the moved clause" {1827    var solver = Solver.init(std.testing.allocator);1828    defer solver.deinit();1829    const pigeons: u32 = 4;1830    const holes: u32 = 3;1831    for (0..pigeons * holes) |_| _ = try solver.addVariable();1832    for (0..pigeons) |pigeon| {1833        var placement: [holes]Literal = undefined;1834        for (&placement, 0..) |*literal, hole| {1835            literal.* = Literal.positive(@intCast(pigeon * holes + hole));1836        }1837        try solver.addClause(&placement);1838    }1839    for (0..holes) |hole| {1840        for (0..pigeons) |first| {1841            for (first + 1..pigeons) |second| {1842                try solver.addClause(&.{1843                    Literal.negative(@intCast(first * holes + hole)),1844                    Literal.negative(@intCast(second * holes + hole)),1845                });1846            }1847        }1848    }1849    const base_count = solver.clauses.items.len;1850    try std.testing.expectEqual(Status.unsat, try solver.solve());1851    try std.testing.expectEqual(@as(u32, 0), solver.decisionLevel());1852    try std.testing.expect(solver.clauses.items.len > base_count + 1);1853    var candidate: ?usize = null;1854    for (base_count..solver.clauses.items.len - 1) |clause_index| {1855        if (!solver.clauseLocked(clause_index)) {1856            candidate = clause_index;1857            break;1858        }1859    }1860    const removed_index = candidate.?;1861    const last_index = solver.clauses.items.len - 1;1862    const moved_literals = solver.clauses.items[last_index].literals;1863    solver.removeLearnedClause(removed_index);1864    try std.testing.expectEqual(last_index, solver.clauses.items.len);1865    try std.testing.expectEqual(moved_literals.ptr, solver.clauses.items[removed_index].literals.ptr);1866    try expectWatchInvariant(&solver);1867    try expectReasonInvariant(&solver);1868    try std.testing.expectEqual(Status.unsat, try solver.solve());1869}18701871test "learned clause records single-level block distance" {1872    var solver = Solver.init(std.testing.allocator);1873    defer solver.deinit();1874    const a = try solver.addVariable();1875    const b = try solver.addVariable();1876    try solver.addClause(&.{ Literal.positive(a), Literal.positive(b) });1877    try solver.addClause(&.{ Literal.negative(a), Literal.positive(b) });1878    try solver.addClause(&.{ Literal.positive(a), Literal.negative(b) });1879    try solver.addClause(&.{ Literal.negative(a), Literal.negative(b) });1880    try std.testing.expectEqual(Status.unsat, try solver.solve());1881    var learned_count: usize = 0;1882    for (solver.clauses.items) |clause| {1883        if (clause.learned) {1884            learned_count += 1;1885            try std.testing.expectEqual(@as(u32, 1), clause.lbd);1886        } else {1887            try std.testing.expectEqual(@as(u32, 0), clause.lbd);1888        }1889    }1890    try std.testing.expect(learned_count > 0);1891}18921893test "learned clause records multi-level block distance" {1894    var solver = Solver.init(std.testing.allocator);1895    defer solver.deinit();1896    const a = try solver.addVariable();1897    const b = try solver.addVariable();1898    const c = try solver.addVariable();1899    try solver.addClause(&.{ Literal.negative(a), Literal.negative(b), Literal.positive(c) });1900    try solver.addClause(&.{ Literal.negative(a), Literal.negative(b), Literal.negative(c) });1901    try std.testing.expectEqual(Status.sat, try solver.solve());1902    var learned_count: usize = 0;1903    for (solver.clauses.items) |clause| {1904        if (clause.learned) {1905            learned_count += 1;1906            try std.testing.expectEqual(@as(usize, 2), clause.literals.len);1907            try std.testing.expectEqual(@as(u32, 2), clause.lbd);1908        }1909    }1910    try std.testing.expectEqual(@as(usize, 1), learned_count);1911}