tiny.smt.Solver

1/// A SAT solver that learns a clause from each conflict above decision level zero over the clauses2/// a caller adds, answers under assumed literals, and records an unsat core and a proof trace after3/// each unsatisfiable answer. The package's bit-vector encoder (`bitvec.Encoder`) turns terms into4/// variables and clauses of a solver it is given, and a caller then solves and reads the answer5/// through the solver. `init` takes an allocator, and the solver allocates every list, clause copy6/// and proof step with it and frees them in `deinit`. A caller sets `conflict_budget` and7/// `max_learned_clauses`, and reads `clauses` and `has_empty_clause`. The other fields are search8/// state, which a caller reads through the solver's functions. Each clause of two or more literals9/// watches two of them, and a unit clause watches its one literal. A decision gives the variable10/// the value it last held, or true for a variable assigned for the first time. The list of assigned11/// literals in assignment order has room past the variable count for the scratch memory of conflict12/// analysis (`ConflictScratch`).13pub const Solver = struct {14    allocator: std.mem.Allocator,15    /// Every clause the solver holds: the caller's nonempty clauses and the learned clauses it16    /// keeps. An empty clause from the caller stays out of the list and sets `has_empty_clause`.17    /// Clause order changes when the solver removes a learned clause under a cap, because the last18    /// clause moves into the removed clause's place. A solve with assumptions removes the clauses19    /// added during it when it returns. `clauseCount` counts the list, and `dimacs.write` writes it20    /// with learned clauses included.21    clauses: std.ArrayList(Clause) = .empty,22    watches: std.ArrayList(std.ArrayList(ClauseRef)) = .empty,23    assignment: std.ArrayList(BoolValue) = .empty,24    saved_phase: std.ArrayList(BoolValue) = .empty,25    level: std.ArrayList(u32) = .empty,26    reason: std.ArrayList(?usize) = .empty,27    trail: std.ArrayList(Literal) = .empty,28    propagation_cursor: usize = 0,29    decision_limits: std.ArrayList(usize) = .empty,30    assumptions: std.ArrayList(Literal) = .empty,31    frames: std.ArrayList(usize) = .empty,32    last_core: std.ArrayList(Literal) = .empty,33    proof_steps: std.ArrayList(ProofStep) = .empty,34    proof_assumptions: std.ArrayList(Literal) = .empty,35    proof_base_clause_count: usize = 0,36    last_stats: SolveStats = .{},37    restart_policy: RestartPolicy = .{},38    conflicts_since_restart: usize = 0,39    next_restart_conflicts: usize = 0,40    /// The most conflicts one solve may meet before it returns `.unknown`. The default `null`41    /// leaves the search unlimited. A caller sets it before a solve to bound the search's work.42    /// While it is set, the solver keeps the solve's proof steps in fixed memory sized from it and43    /// the variable count (`ProofTrace`). The extra solves of core minimization share what is left44    /// of it after the main search.45    conflict_budget: ?usize = null,46    /// The most replaceable learned clauses the solver keeps. The default `null` leaves the learned47    /// clauses uncapped. A caller sets it before a solve to bound the memory learned clauses take.48    /// At the start of each solve, and whenever the count passes the cap during a search, the49    /// solver removes replaceable learned clauses, highest block distance first and then the50    /// longest. The solver keeps each clause that justifies a current value and the newly learned51    /// clause, so the count can pass the cap by those clauses. While it is set, the solver keeps52    /// replaceable learned clauses in fixed memory sized from the cap and the variable count53    /// (`LearnedStore`). After a caller sets it back to `null`, the next solve moves those clauses54    /// to heap memory.55    max_learned_clauses: ?usize = null,56    learned_clause_count: usize = 0,57    glue_clause_count: usize = 0,58    learned_store: ?store.Store = null,59    proof_trace: ?trace.Trace = null,60    proof_trace_slab: bool = true,61    rup_assignment: std.ArrayList(BoolValue) = .empty,62    /// True once the caller has added an empty clause. Every later solve then answers `.unsat`.63    /// `dimacs.write` writes an empty clause for it, and `lastProofArtifact` adds an empty starting64    /// clause for it. The solver's own proof checks accept every step while it is set. The default65    /// is false.66    has_empty_clause: bool = false,67    inconsistent: bool = false,6869    /// Returns an empty solver that allocates with `allocator`. A caller creates one solver per70    /// formula and hands it to the code that adds the clauses. The call allocates nothing.71    pub fn init(allocator: std.mem.Allocator) Solver {72        return .{ .allocator = allocator };73    }7475    /// Frees every clause, list, fixed store, trace and proof step, and leaves the solver76    /// undefined. The owner of a solver calls it once, when it is done with the formula. Slices77    /// from `lastUnsatCore`, `lastProofTrace` and `activeAssumptions` become invalid. Artifacts78    /// from `lastProofArtifact` stay valid, because each owns its own copy.79    pub fn deinit(self: *Solver) void {80        for (self.clauses.items) |clause| {81            if (clause.storage == .heap) self.allocator.free(clause.literals);82        }83        if (self.learned_store) |*pool| pool.deinit(self.allocator);84        self.clauses.deinit(self.allocator);85        for (self.watches.items) |*watch| {86            watch.deinit(self.allocator);87        }88        self.watches.deinit(self.allocator);89        self.assignment.deinit(self.allocator);90        self.saved_phase.deinit(self.allocator);91        self.level.deinit(self.allocator);92        self.reason.deinit(self.allocator);93        self.trail.deinit(self.allocator);94        self.decision_limits.deinit(self.allocator);95        self.assumptions.deinit(self.allocator);96        self.frames.deinit(self.allocator);97        self.last_core.deinit(self.allocator);98        self.clearProofTrace();99        if (self.proof_trace) |*owner| owner.deinit(self.allocator);100        self.proof_steps.deinit(self.allocator);101        self.proof_assumptions.deinit(self.allocator);102        self.rup_assignment.deinit(self.allocator);103        self.* = undefined;104    }105106    /// Returns the number of variables: one more than the highest variable index the solver has107    /// added or seen. A caller reports it as a size of the encoded formula. A clause or an108    /// assumption that names a higher variable raises it.109    pub fn variableCount(self: *const Solver) usize {110        return self.assignment.items.len;111    }112113    /// Returns the number of entries in `clauses`. A caller reports it as a size of the encoded114    /// formula, and `dimacs.write` prints it in its header. The count includes the learned clauses115    /// the solver keeps and leaves out an empty clause from the caller.116    pub fn clauseCount(self: *const Solver) usize {117        return self.clauses.items.len;118    }119120    /// Returns the number of learned clauses the solver holds, at every block distance. A caller121    /// checks how many learned clauses survive a capped search. The count drops when the solver122    /// removes a learned clause under a cap and when a solve with assumptions returns.123    pub fn retainedLearnedClauses(self: *const Solver) usize {124        return self.learned_clause_count;125    }126127    /// Returns the number of learned clauses whose literals span more than two decision levels. A128    /// caller compares it with `max_learned_clauses` after a capped search. These are the clauses129    /// the cap bounds.130    pub fn replaceableLearnedClauses(self: *const Solver) usize {131        assert(self.glue_clause_count <= self.learned_clause_count);132        return self.learned_clause_count - self.glue_clause_count;133    }134135    /// Sets the restart schedule for later solves. A caller that wants restarts at a different136    /// pace, such as after every conflict, sets it before solving. The schedule takes effect at the137    /// start of the next solve.138    pub fn setRestartPolicy(self: *Solver, policy: RestartPolicy) void {139        self.restart_policy = policy;140    }141142    /// Returns the restart schedule later solves use. A caller reads back the schedule that143    /// `setRestartPolicy` set, or the default.144    pub fn restartPolicy(self: *const Solver) RestartPolicy {145        return self.restart_policy;146    }147148    /// Adds one unassigned variable and returns its index, counting from 0. `bitvec.Encoder` adds a149    /// variable for each Boolean it encodes, and `dimacs.parse` adds the variable count of its150    /// header. The call clears the recorded core and trace. The call returns `error.OutOfMemory`151    /// when a list fails to grow. An index at or above 2^31 overflows the literal's packed number,152    /// so building a literal for it panics in safe builds.153    pub fn addVariable(self: *Solver) !u32 {154        self.last_core.clearRetainingCapacity();155        self.clearProofTrace();156        const variable_index: u32 = @intCast(self.assignment.items.len);157        try self.ensureVariable(variable_index);158        return variable_index;159    }160161    /// Adds a copy of `literals` as a clause and adds any variable it names that the solver lacks.162    /// `bitvec.Encoder` asserts each encoded fact through it, and `dimacs.parse` adds each clause163    /// of its input. The caller keeps `literals`. An empty slice sets `has_empty_clause`, and every164    /// later solve answers `.unsat`. The solver assigns the literal of a unit clause at once. When165    /// the literal of a unit clause is false under the assignment the last search left, every later166    /// solve skips the search and checks the final empty clause at once, so it returns167    /// `error.InvalidProofTrace` for a formula that is still satisfiable. The call clears the168    /// recorded core and trace. The call returns `error.OutOfMemory` when a copy or a list fails to169    /// grow, and then the clause is left out while variables it named may stay added.170    pub fn addClause(self: *Solver, literals: []const Literal) !void {171        self.last_core.clearRetainingCapacity();172        self.clearProofTrace();173        if (literals.len == 0) {174            self.has_empty_clause = true;175            self.inconsistent = true;176            return;177        }178        for (literals) |literal| {179            try self.ensureVariable(literal.variable());180        }181        const owned = try self.allocator.dupe(Literal, literals);182        errdefer self.allocator.free(owned);183        const clause_index = self.clauses.items.len;184        const clause = Clause{185            .literals = owned,186            .learned = false,187            .lbd = 0,188            .storage = .heap,189            .watch_a = 0,190            .watch_b = if (owned.len > 1) 1 else 0,191        };192        try self.clauses.append(self.allocator, clause);193        errdefer _ = self.clauses.pop();194        try self.addWatch(owned[0], clause_index);195        errdefer _ = self.removeWatch(owned[0], clause_index);196        if (owned.len > 1) {197            try self.addWatch(owned[1], clause_index);198        }199        if (owned.len == 1) {200            if (!try self.enqueue(owned[0], clause_index)) self.inconsistent = true;201        }202    }203204    /// Solves the clauses alone, as `solveWithAssumptions` does with an empty list. A caller that205    /// asks one question of a formula calls it. The solver's own assumption list, which `assume`206    /// fills, takes no part.207    pub fn solve(self: *Solver) !Status {208        return self.solveWithAssumptions(&.{});209    }210211    /// Saves the current length of the assumption list, so the next `popAssumptionFrame` returns212    /// the list to it. A caller that nests questions pushes a frame before it assumes the literals213    /// of an inner question. The call clears the recorded core and trace. The call returns214    /// `error.OutOfMemory` when the frame list fails to grow.215    pub fn pushAssumptionFrame(self: *Solver) !void {216        self.last_core.clearRetainingCapacity();217        self.clearProofTrace();218        try self.frames.append(self.allocator, self.assumptions.items.len);219    }220221    /// Returns the assumption list to the length the latest push saved and closes that frame. A222    /// caller that nests questions pops a frame to leave an inner question. With no frame open, the223    /// list stays as it is. The call clears the recorded core and trace in both cases.224    pub fn popAssumptionFrame(self: *Solver) void {225        self.last_core.clearRetainingCapacity();226        self.clearProofTrace();227        const frame_start = self.frames.pop() orelse return;228        self.assumptions.shrinkRetainingCapacity(frame_start);229    }230231    /// Adds `literal` to the solver's assumption list and adds its variable when the solver lacks232    /// it. `bitvec.Encoder` assumes the literal of each assumed term through it, for a later233    /// `solveWithActiveAssumptions`. The literal stays in the list until a pop past its frame or234    /// `clearAssumptionFrames`. The call clears the recorded core and trace. The call returns235    /// `error.OutOfMemory` when a list fails to grow.236    pub fn assume(self: *Solver, literal: Literal) !void {237        self.last_core.clearRetainingCapacity();238        self.clearProofTrace();239        try self.ensureVariable(literal.variable());240        try self.assumptions.append(self.allocator, literal);241    }242243    /// Empties the assumption list and closes every frame. A caller that starts a new round of244    /// questions calls it to drop every assumption and frame at once. The call clears the recorded245    /// core and trace.246    pub fn clearAssumptionFrames(self: *Solver) void {247        self.last_core.clearRetainingCapacity();248        self.clearProofTrace();249        self.assumptions.clearRetainingCapacity();250        self.frames.clearRetainingCapacity();251    }252253    /// Solves under the solver's own assumption list, as `solveWithAssumptions` does.254    /// `bitvec.Encoder.solve` calls it, so the literals assumed with `assume` take part.255    pub fn solveWithActiveAssumptions(self: *Solver) !Status {256        return self.solveWithAssumptions(self.assumptions.items);257    }258259    /// Returns the solver's assumption list, oldest first. A caller reads the assumptions in force260    /// after pushes and pops. The slice stays valid until the list changes.261    pub fn activeAssumptions(self: *const Solver) []const Literal {262        return self.assumptions.items;263    }264265    /// Returns the number of open frames. A caller checks how deep its nesting is.266    pub fn frameDepth(self: *const Solver) usize {267        return self.frames.items.len;268    }269270    /// Returns a set of the last solve's assumptions that the clauses refute together, after an271    /// unsatisfiable answer. A caller maps the core back to the named assumptions it made, to272    /// report which of them conflict. The solver first records as the core the assumptions it had273    /// assigned when the conflict came. When that recorded core holds two or more assumptions, the274    /// core is the smaller set that the extra solves of core minimization certified. The core is275    /// empty when the clauses were refuted before the search began, as by two opposite unit clauses276    /// or an empty clause, after a satisfiable or unknown answer, and after any change that clears277    /// it. A recorded core of one assumption stays as it is, because core minimization runs only278    /// for two or more, so the core can hold that assumption even when the clauses alone are279    /// unsatisfiable. A conflict while the solver assigns the assumptions records only those280    /// assigned so far, so a solve under two or more assumptions can end with a core of one and no281    /// shrinking. Under a conflict limit, the core holds every assumption when the limit ran out282    /// during the drops, and it is empty with an `.unknown` answer when the limit ran out during283    /// the certifying solve. The slice stays valid until the next change to the solver.284    pub fn lastUnsatCore(self: *const Solver) []const Literal {285        return self.last_core.items;286    }287288    /// Returns the work counts of the last solve. A caller reports them beside the answer. A solve289    /// resets them at its start. After core minimization certifies a smaller core, `proof_steps`290    /// holds the certifying solve's step count, and it is the one count core minimization sets. The291    /// other counts leave out the work of the extra solves of core minimization.292    pub fn lastSolveStats(self: *const Solver) SolveStats {293        return self.last_stats;294    }295296    /// Returns the proof steps of the last solve, in order. A caller reads the steps in place, and297    /// `lastProofArtifact` makes a copy that outlives later changes. The trace holds one step per298    /// learned clause and, after an unsatisfiable answer, a final empty clause. After a satisfiable299    /// or unknown answer, the trace can still hold the steps learned during the solve. The slices300    /// stay valid until the next change to the solver.301    pub fn lastProofTrace(self: *const Solver) []const ProofStep {302        return self.proof_steps.items;303    }304305    /// Returns true when the trace is nonempty, each step follows by unit propagation from the306    /// starting clauses, the assumptions and the earlier steps, and the last step is the empty307    /// clause. A caller confirms an unsatisfiable answer in place. The check accepts every step308    /// while `has_empty_clause` is set.309    pub fn lastProofTraceValid(self: *const Solver) bool {310        if (self.proof_steps.items.len == 0) return false;311        for (self.proof_steps.items, 0..) |step, index| {312            if (!self.rupCheck(step.literals, index)) return false;313        }314        return self.proof_steps.items[self.proof_steps.items.len - 1].literals.len == 0;315    }316317    /// Returns a copy of the clauses, assumptions and steps behind the last unsatisfiable answer,318    /// allocated with `allocator` and owned by the caller, or null when the trace is empty. A319    /// caller keeps the evidence after the solver moves on, checks it with `ProofArtifact.valid`,320    /// or writes it out. The starting clauses are every clause the solver held when the solve321    /// began, learned clauses it kept included, then an empty clause when `has_empty_clause` is322    /// set. The artifact covers the solver's variable count. After a solve that learned clauses and323    /// then answered `.sat`, or `.unknown` at the main search's conflict limit, the call returns an324    /// artifact that `ProofArtifact.valid` rejects. After an `.unknown` answer from the certifying325    /// solve of core minimization, the artifact holds the refutation under every assumption of the326    /// solve, and `ProofArtifact.valid` accepts it. The call returns `error.OutOfMemory` when a327    /// copy fails, and then frees what it copied.328    pub fn lastProofArtifact(self: *const Solver, allocator: std.mem.Allocator) !?ProofArtifact {329        if (self.proof_steps.items.len == 0) return null;330        assert(self.last_stats.proof_steps == self.proof_steps.items.len);331        var artifact = ProofArtifact.init(allocator, self.assignment.items.len);332        errdefer artifact.deinit();333        const base_count = @min(self.proof_base_clause_count, self.clauses.items.len);334        for (self.clauses.items[0..base_count]) |clause| {335            try artifact.appendClause(clause.literals);336        }337        if (self.has_empty_clause) try artifact.appendClause(&.{});338        try artifact.appendAssumptions(self.proof_assumptions.items);339        for (self.proof_steps.items) |step| {340            try artifact.appendStep(step.literals);341        }342        return artifact;343    }344345    /// Decides whether the clauses and every literal of `assumptions` can all be true, and returns346    /// `.sat`, `.unsat` or `.unknown`. A caller asks a question under temporary hypotheses and347    /// learns which of them the clauses refute together. The solve assigns the assumptions first,348    /// in order, at decision level zero, and adds any variable they name that the solver lacks.349    /// After `.unsat`, `lastUnsatCore` holds one of three sets: the assumptions the solve had350    /// assigned when the conflict came, the smaller set that core minimization certified when that351    /// recorded core holds two or more, or every assumption of the solve when a conflict limit runs352    /// out while core minimization drops assumptions. When `assumptions` is nonempty, every clause353    /// added during the solve is removed when the solve returns. The solve clears the recorded354    /// core, trace and counts only after it has made room for conflict analysis, so a failure355    /// before that point leaves the old evidence in place. The call returns `error.OutOfMemory`356    /// when an allocation fails, `error.CapacityOverflow` when a size for the solve overflows357    /// `usize`, `error.InvalidProofTrace` when a learned clause or the final step fails its check,358    /// `error.InvalidConflictGraph` when conflict analysis runs out of assigned literals to resolve359    /// on, `error.InvalidUnsatCore` when the certifying solve satisfies the core, and the errors of360    /// `ConflictScratch`. The assignment stays after the call, and `value` and `literalValue` read361    /// it.362    pub fn solveWithAssumptions(self: *Solver, assumptions: []const Literal) !Status {363        return try self.solveWithAssumptionsMode(assumptions, true);364    }365366    fn solveWithAssumptionsMode(367        self: *Solver,368        assumptions: []const Literal,369        minimize_core: bool,370    ) anyerror!Status {371        const required_variables = try self.requiredVariableCount(assumptions);372        const scratch_capacity = try self.ensureConflictScratchStorage(required_variables);373        self.clearSolveEvidence();374        errdefer self.clearSolveEvidence();375        self.conflicts_since_restart = 0;376        self.next_restart_conflicts = self.restart_policy.first_conflict_interval;377        for (assumptions) |assumption| {378            try self.ensureVariable(assumption.variable());379        }380        if (self.max_learned_clauses != null) {381            self.backtrack(0);382            self.proof_base_clause_count = 0;383            self.reduceLearned(0, null);384        }385        try self.ensureLearnedStore();386        try self.ensureProofTrace();387        var conflict_scratch: ?scratch.ConflictScratch = null;388        if (scratch_capacity) |capacity| {389            const storage = self.conflictScratchStorage(capacity);390            conflict_scratch = try scratch.ConflictScratch.init(391                storage,392                .{ .variables = capacity.variables },393            );394            conflict_scratch.?.activate();395        }396        defer if (conflict_scratch) |*owner| {397            const expected_pointer = @intFromPtr(owner.storage.ptr);398            const expected_length = owner.storage.len;399            const returned = owner.deinit();400            assert(expected_pointer == @intFromPtr(returned.ptr));401            assert(expected_length == returned.len);402        };403        const retained_clause_count = self.clauses.items.len;404        defer if (assumptions.len > 0) self.discardClausesFrom(retained_clause_count);405        self.proof_base_clause_count = retained_clause_count;406        try self.proof_assumptions.appendSlice(self.allocator, assumptions);407        self.clearSearch();408        if (self.inconsistent) {409            self.recordConflict();410            try self.recordFinalProofStep();411            return .unsat;412        }413        for (assumptions, 0..) |assumption, assumption_index| {414            try self.ensureVariable(assumption.variable());415            if (!try self.enqueue(assumption, null)) {416                self.recordConflict();417                return try self.finishAssumptionUnsat(418                    assumptions[0 .. assumption_index + 1],419                    minimize_core,420                );421            }422            switch (try self.propagate()) {423                .consistent => {},424                .conflict => {425                    self.recordConflict();426                    return try self.finishAssumptionUnsat(427                        assumptions[0 .. assumption_index + 1],428                        minimize_core,429                    );430                },431            }432        }433        while (true) {434            switch (try self.propagate()) {435                .consistent => {},436                .conflict => |clause_index| {437                    self.recordConflict();438                    if (self.decisionLevel() == 0) {439                        return try self.finishAssumptionUnsat(assumptions, minimize_core);440                    }441                    if (!try self.learnFromConflict(&conflict_scratch.?, clause_index)) {442                        if (assumptions.len == 0) self.inconsistent = true;443                        return try self.finishAssumptionUnsat(assumptions, minimize_core);444                    }445                    if (self.conflict_budget) |budget| {446                        if (self.last_stats.conflicts >= budget) return .unknown;447                    }448                    self.maybeRestart();449                    continue;450                },451            }452            if (self.nextUnassignedVariable()) |variable_index| {453                try self.newDecisionLevel();454                self.last_stats.decisions += 1;455                const decision_literal = self.decisionLiteral(variable_index);456                if (self.saved_phase.items[variable_index] != .unset) {457                    self.last_stats.phase_saved_decisions += 1;458                }459                if (!try self.enqueue(decision_literal, null)) {460                    self.recordConflict();461                    try self.recordFinalProofStep();462                    return .unsat;463                }464                continue;465            }466            return .sat;467        }468    }469470    /// Returns the value of `variable_index` in the current assignment, or null when the variable471    /// is unassigned or at or above the variable count. A caller reads a satisfying assignment472    /// after `.sat`. The values form a satisfying assignment only after `.sat`.473    pub fn value(self: *const Solver, variable_index: u32) ?bool {474        if (variable_index >= self.assignment.items.len) return null;475        return switch (self.assignment.items[variable_index]) {476            .unset => null,477            .false => false,478            .true => true,479        };480    }481482    fn finishAssumptionUnsat(483        self: *Solver,484        assumptions: []const Literal,485        minimize_core: bool,486    ) anyerror!Status {487        if (assumptions.len > 0) try self.recordUnsatCore(assumptions);488        try self.recordFinalProofStep();489        if (minimize_core and assumptions.len > 1) return try self.minimizeLastUnsatCore();490        return .unsat;491    }492493    fn minimizeLastUnsatCore(self: *Solver) anyerror!Status {494        var pool: ?usize = if (self.conflict_budget) |budget| budget -| self.last_stats.conflicts else null;495        var core: std.ArrayList(Literal) = .empty;496        defer core.deinit(self.allocator);497        try core.appendSlice(self.allocator, self.last_core.items);498        var trial: std.ArrayList(Literal) = .empty;499        defer trial.deinit(self.allocator);500        var index: usize = 0;501        while (index < core.items.len) {502            if (poolDrained(pool)) break;503            trial.clearRetainingCapacity();504            for (core.items, 0..) |literal, candidate_index| {505                if (candidate_index != index) try trial.append(self.allocator, literal);506            }507            const outcome = try self.probeStatusWithAssumptions(trial.items, pool);508            drainPool(&pool, outcome.conflicts);509            if (outcome.status == .unsat) {510                core.clearRetainingCapacity();511                try core.appendSlice(self.allocator, trial.items);512            } else {513                index += 1;514            }515        }516        if (!poolDrained(pool)) {517            var probe = try self.baseProbe(pool);518            defer probe.deinit();519            const certified = try probe.solveWithAssumptionsMode(core.items, false);520            drainPool(&pool, probe.lastSolveStats().conflicts);521            switch (certified) {522                .sat => return error.InvalidUnsatCore,523                .unknown => {524                    self.last_core.clearRetainingCapacity();525                    return .unknown;526                },527                .unsat => {528                    const base_count = self.proof_base_clause_count;529                    self.clearProofTrace();530                    self.proof_base_clause_count = base_count;531                    try self.proof_assumptions.appendSlice(self.allocator, probe.lastUnsatCore());532                    for (probe.proof_steps.items) |step| {533                        try self.appendStepStorage(step.literals);534                    }535                    self.last_stats.proof_steps = self.proof_steps.items.len;536                    try self.recordUnsatCore(probe.lastUnsatCore());537                    return .unsat;538                },539            }540        }541        try self.recordUnsatCore(self.proof_assumptions.items);542        return .unsat;543    }544545    fn poolDrained(pool: ?usize) bool {546        return if (pool) |remaining| remaining == 0 else false;547    }548549    fn drainPool(pool: *?usize, spent: usize) void {550        if (pool.*) |remaining| pool.* = remaining -| spent;551    }552553    fn probeStatusWithAssumptions(554        self: *const Solver,555        assumptions: []const Literal,556        pool: ?usize,557    ) anyerror!ProbeOutcome {558        var probe = try self.baseProbe(pool);559        defer probe.deinit();560        const status = try probe.solveWithAssumptionsMode(assumptions, false);561        return .{ .status = status, .conflicts = probe.lastSolveStats().conflicts };562    }563564    fn baseProbe(self: *const Solver, pool: ?usize) anyerror!Solver {565        var probe = Solver.init(self.allocator);566        errdefer probe.deinit();567        probe.conflict_budget = pool;568        probe.proof_trace_slab = false;569        probe.max_learned_clauses = self.max_learned_clauses;570        probe.setRestartPolicy(self.restart_policy);571        for (self.clauses.items) |clause| {572            if (!clause.learned) try probe.addClause(clause.literals);573        }574        if (self.has_empty_clause) try probe.addClause(&.{});575        return probe;576    }577578    fn recordUnsatCore(self: *Solver, assumptions: []const Literal) !void {579        self.last_core.clearRetainingCapacity();580        try self.last_core.appendSlice(self.allocator, assumptions);581    }582583    fn recordConflict(self: *Solver) void {584        self.last_stats.conflicts += 1;585        self.conflicts_since_restart += 1;586        if (self.decisionLevel() == 0) self.last_stats.root_conflicts += 1;587    }588589    fn clearProofTrace(self: *Solver) void {590        if (self.proof_trace) |*owner| {591            for (self.proof_steps.items) |step| {592                if (step.literals.len == 0) continue;593                assert(owner.owns(step.literals));594            }595            owner.clear();596        } else {597            for (self.proof_steps.items) |step| {598                self.allocator.free(step.literals);599            }600        }601        self.proof_steps.clearRetainingCapacity();602        self.proof_assumptions.clearRetainingCapacity();603        self.proof_base_clause_count = 0;604    }605606    fn clearSolveEvidence(self: *Solver) void {607        self.clearProofTrace();608        self.last_core.clearRetainingCapacity();609        self.last_stats = .{};610    }611612    fn acquireStepStorage(self: *Solver, literals: []const Literal) ![]Literal {613        if (self.proof_trace) |*owner| {614            if (literals.len == 0) return owner.acquireEmpty();615            return owner.acquire(literals);616        }617        return try self.allocator.dupe(Literal, literals);618    }619620    fn appendStepStorage(self: *Solver, literals: []const Literal) !void {621        const owned = try self.acquireStepStorage(literals);622        if (self.proof_trace != null) {623            assert(self.proof_steps.items.len < self.proof_steps.capacity);624            self.proof_steps.appendAssumeCapacity(.{ .literals = owned });625            return;626        }627        errdefer self.allocator.free(owned);628        try self.proof_steps.append(self.allocator, .{ .literals = owned });629    }630631    fn appendProofStep(self: *Solver, literals: []const Literal) !void {632        try self.appendStepStorage(literals);633        self.last_stats.proof_steps += 1;634    }635636    fn removeLastProofStep(self: *Solver) void {637        const step = self.proof_steps.pop() orelse return;638        if (self.proof_trace) |*owner| {639            owner.releaseLast(step.literals);640        } else {641            self.allocator.free(step.literals);642        }643        self.last_stats.proof_steps -= 1;644    }645646    fn recordFinalProofStep(self: *Solver) !void {647        if (!self.rupCheck(&.{}, self.proof_steps.items.len)) return error.InvalidProofTrace;648        try self.appendProofStep(&.{});649    }650651    fn traceBudget(self: *const Solver) ?usize {652        if (!self.proof_trace_slab) return null;653        return self.conflict_budget;654    }655656    fn rupCheck(self: *const Solver, literals: []const Literal, proof_step_limit: usize) bool {657        if (self.has_empty_clause) return true;658        assert(self.rup_assignment.items.len == self.assignment.items.len);659        const base_count = @min(self.proof_base_clause_count, self.clauses.items.len);660        return proof.rupCheckKnownVariablesWithClauses(661            self.rup_assignment.items,662            Clause,663            self.clauses.items[0..base_count],664            self.proof_assumptions.items,665            self.proof_steps.items,666            literals,667            proof_step_limit,668        );669    }670671    fn rupCheckConflict(self: *const Solver, literals: []const Literal, conflict: usize) bool {672        return proof.rupCheckKnownVariablesWithReasons(673            self.rup_assignment.items,674            Clause,675            self.clauses.items,676            self.proof_assumptions.items,677            literals,678            .{ .trail = self.trail.items, .reasons = self.reason.items, .conflict = conflict },679        );680    }681682    fn ensureProofTrace(self: *Solver) !void {683        assert(self.proof_steps.items.len == 0);684        const budget = self.traceBudget() orelse {685            if (self.proof_trace) |*owner| {686                owner.deinit(self.allocator);687                self.proof_trace = null;688            }689            return;690        };691        const limits = trace.Trace.Limits.inspect(budget, self.variableCount());692        const required = try trace.Trace.Capacity.derive(limits);693        if (self.proof_trace) |*existing| {694            if (existing.admits(required)) {695                try self.proof_steps.ensureTotalCapacity(self.allocator, existing.capacity.steps);696                return;697            }698            existing.deinit(self.allocator);699            self.proof_trace = null;700        }701        var fresh = try trace.Trace.init(self.allocator, limits);702        fresh.activate();703        self.proof_trace = fresh;704        try self.proof_steps.ensureTotalCapacity(self.allocator, required.steps);705    }706707    fn requiredVariableCount(708        self: *const Solver,709        assumptions: []const Literal,710    ) error{CapacityOverflow}!usize {711        var required = self.variableCount();712        for (assumptions) |assumption| {713            const assumption_variables = std.math.add(714                usize,715                @as(usize, assumption.variable()),716                1,717            ) catch return error.CapacityOverflow;718            required = @max(required, assumption_variables);719        }720        return required;721    }722723    fn ensureConflictScratchStorage(724        self: *Solver,725        required_variables: usize,726    ) !?scratch.ConflictScratch.Capacity {727        if (required_variables == 0) return null;728        const limits = scratch.ConflictScratch.Limits.inspect(required_variables);729        const required = try scratch.ConflictScratch.Capacity.derive(limits);730        try self.trail.ensureTotalCapacityPrecise(731            self.allocator,732            required.trail_capacity,733        );734        return required;735    }736737    fn conflictScratchStorage(738        self: *Solver,739        capacity: scratch.ConflictScratch.Capacity,740    ) scratch.ConflictScratch.Storage {741        assert(self.trail.items.len <= capacity.variables);742        assert(self.trail.capacity >= capacity.trail_capacity);743        const backing = self.trail.allocatedSlice()[capacity.variables..capacity.trail_capacity];744        const bytes = std.mem.sliceAsBytes(backing);745        assert(bytes.len >= capacity.storage_bytes);746        return @alignCast(bytes[0..capacity.storage_bytes]);747    }748749    fn ensureLearnedStore(self: *Solver) !void {750        const limit = self.max_learned_clauses orelse {751            try self.evacuateLearnedStore();752            return;753        };754        const limits = store.Store.Limits.inspect(limit, self.variableCount());755        const required = try store.Store.Capacity.derive(limits);756        if (self.learned_store) |*existing| {757            if (existing.admits(required)) return;758        }759        var fresh = try store.Store.init(self.allocator, limits);760        fresh.activate();761        if (self.learned_store) |*old| {762            for (self.clauses.items) |*clause| {763                if (clause.storage == .pool) {764                    assert(old.owns(clause.literals));765                    clause.literals = fresh.acquire(clause.literals);766                }767            }768            old.deinit(self.allocator);769        }770        self.learned_store = fresh;771    }772773    fn evacuateLearnedStore(self: *Solver) !void {774        if (self.learned_store == null) return;775        for (self.clauses.items) |*clause| {776            if (clause.storage == .pool) {777                const heap_copy = try self.allocator.dupe(Literal, clause.literals);778                self.learnedPool().release(clause.literals);779                clause.literals = heap_copy;780                clause.storage = .heap;781            }782        }783        self.learnedPool().deinit(self.allocator);784        self.learned_store = null;785    }786787    fn maybeRestart(self: *Solver) void {788        if (self.next_restart_conflicts != 0 and789            self.decisionLevel() > 0 and790            self.conflicts_since_restart >= self.next_restart_conflicts)791        {792            self.backtrack(0);793            self.last_stats.restarts += 1;794            self.conflicts_since_restart = 0;795            if (self.restart_policy.growth > 1) {796                self.next_restart_conflicts = std.math.mul(797                    usize,798                    self.next_restart_conflicts,799                    self.restart_policy.growth,800                ) catch std.math.maxInt(usize);801            }802        }803        const limit = self.max_learned_clauses orelse return;804        if (self.replaceableLearnedClauses() <= limit) return;805        assert(self.clauses.items.len > 0);806        if (self.decisionLevel() > 0) {807            self.backtrack(0);808            self.last_stats.restarts += 1;809            self.conflicts_since_restart = 0;810        }811        const just_learned = self.clauses.items.len - 1;812        const protected = if (just_learned >= self.proof_base_clause_count) just_learned else null;813        self.reduceLearned(self.proof_base_clause_count, protected);814    }815816    fn reduceLearned(self: *Solver, first_candidate: usize, protected: ?usize) void {817        const limit = self.max_learned_clauses orelse return;818        assert(self.decisionLevel() == 0);819        assert(first_candidate >= self.proof_base_clause_count);820        assert(self.learned_clause_count == self.countLearnedClauses());821        assert(self.glue_clause_count == self.countGlueClauses());822        var bound = self.clauses.items.len;823        while (self.replaceableLearnedClauses() > limit and bound > 0) : (bound -= 1) {824            const victim = self.selectVictim(first_candidate, protected) orelse break;825            self.removeLearnedClause(victim);826            self.last_stats.evicted_clauses += 1;827        }828    }829830    fn selectVictim(self: *const Solver, first_candidate: usize, protected: ?usize) ?usize {831        assert(first_candidate <= self.clauses.items.len);832        var worst: ?usize = null;833        for (self.clauses.items[first_candidate..], first_candidate..) |clause, clause_index| {834            if (!clause.learned) continue;835            if (clause.lbd <= glue_lbd_max) continue;836            if (protected == clause_index) continue;837            if (self.clauseLocked(clause_index)) continue;838            if (worst) |current| {839                if (self.evictsBefore(clause_index, current)) worst = clause_index;840            } else {841                worst = clause_index;842            }843        }844        return worst;845    }846847    fn evictsBefore(self: *const Solver, left_index: usize, right_index: usize) bool {848        const left = self.clauses.items[left_index];849        const right = self.clauses.items[right_index];850        if (left.lbd != right.lbd) return left.lbd > right.lbd;851        return left.literals.len > right.literals.len;852    }853854    fn countLearnedClauses(self: *const Solver) usize {855        var count: usize = 0;856        for (self.clauses.items) |clause| {857            if (clause.learned) count += 1;858        }859        return count;860    }861862    fn countGlueClauses(self: *const Solver) usize {863        var count: usize = 0;864        for (self.clauses.items) |clause| {865            if (clause.learned and clause.lbd <= glue_lbd_max) count += 1;866        }867        return count;868    }869870    /// Returns the value of `literal` in the current assignment: `.true`, `.false`, or `.unset`871    /// when its variable is unassigned or at or above the variable count. `bitvec.Encoder` reads872    /// each Boolean of a model through it. The values form a satisfying assignment only after873    /// `.sat`.874    pub fn literalValue(self: *const Solver, literal: Literal) BoolValue {875        if (literal.variable() >= self.assignment.items.len) return .unset;876        const assigned = self.assignment.items[literal.variable()];877        return if (literal.isPositive()) assigned else assigned.invert();878    }879880    fn ensureVariable(self: *Solver, variable_index: u32) !void {881        const needed = @as(usize, variable_index) + 1;882        while (self.assignment.items.len < needed) {883            try self.assignment.append(self.allocator, .unset);884            errdefer _ = self.assignment.pop();885            try self.saved_phase.append(self.allocator, .unset);886            errdefer _ = self.saved_phase.pop();887            try self.level.append(self.allocator, 0);888            errdefer _ = self.level.pop();889            try self.reason.append(self.allocator, null);890            errdefer _ = self.reason.pop();891            try self.rup_assignment.append(self.allocator, .unset);892            errdefer _ = self.rup_assignment.pop();893            try self.watches.append(self.allocator, .empty);894            errdefer {895                var removed = self.watches.pop().?;896                removed.deinit(self.allocator);897            }898            try self.watches.append(self.allocator, .empty);899        }900    }901902    fn addWatch(self: *Solver, literal: Literal, clause_index: usize) !void {903        try self.watches.items[literal.index()].append(self.allocator, .{ .index = clause_index });904    }905906    fn removeWatch(self: *Solver, literal: Literal, clause_index: usize) bool {907        const watch = &self.watches.items[literal.index()];908        for (watch.items, 0..) |clause_ref, index| {909            if (clause_ref.index == clause_index) {910                _ = watch.swapRemove(index);911                return true;912            }913        }914        return false;915    }916917    fn patchWatch(self: *Solver, literal: Literal, from_index: usize, to_index: usize) void {918        const watch = &self.watches.items[literal.index()];919        for (watch.items) |*clause_ref| {920            if (clause_ref.index == from_index) {921                clause_ref.index = to_index;922                return;923            }924        }925        unreachable;926    }927928    fn clauseLocked(self: *const Solver, clause_index: usize) bool {929        assert(clause_index < self.clauses.items.len);930        for (self.trail.items) |trail_literal| {931            const variable_index = trail_literal.variable();932            if (self.reason.items[variable_index]) |reason_index| {933                if (reason_index == clause_index) return true;934            }935        }936        return false;937    }938939    fn removeLearnedClause(self: *Solver, clause_index: usize) void {940        assert(self.decisionLevel() == 0);941        assert(clause_index >= self.proof_base_clause_count);942        assert(clause_index < self.clauses.items.len);943        const clause = self.clauses.items[clause_index];944        assert(clause.learned);945        assert(!self.clauseLocked(clause_index));946        const removed_first = self.removeWatch(clause.literals[clause.watch_a], clause_index);947        assert(removed_first);948        if (clause.watch_b != clause.watch_a) {949            const removed_second = self.removeWatch(clause.literals[clause.watch_b], clause_index);950            assert(removed_second);951        }952        const last_index = self.clauses.items.len - 1;953        _ = self.clauses.swapRemove(clause_index);954        if (clause_index != last_index) {955            const moved = self.clauses.items[clause_index];956            self.patchWatch(moved.literals[moved.watch_a], last_index, clause_index);957            if (moved.watch_b != moved.watch_a) {958                self.patchWatch(moved.literals[moved.watch_b], last_index, clause_index);959            }960            for (self.trail.items) |trail_literal| {961                const variable_index = trail_literal.variable();962                if (self.reason.items[variable_index]) |reason_index| {963                    if (reason_index == last_index) {964                        self.reason.items[variable_index] = clause_index;965                    }966                }967            }968        }969        assert(self.learned_clause_count > 0);970        self.learned_clause_count -= 1;971        if (clause.lbd <= glue_lbd_max) {972            assert(self.glue_clause_count > 0);973            self.glue_clause_count -= 1;974        }975        self.freeClauseLiterals(clause);976    }977978    fn clearSearch(self: *Solver) void {979        for (self.assignment.items) |*item| item.* = .unset;980        for (self.level.items) |*item| item.* = 0;981        for (self.reason.items) |*item| item.* = null;982        self.trail.clearRetainingCapacity();983        self.decision_limits.clearRetainingCapacity();984        self.propagation_cursor = 0;985        for (self.clauses.items, 0..) |clause, clause_index| {986            if (clause.literals.len == 1) {987                if (!(self.enqueue(clause.literals[0], clause_index) catch false)) {988                    self.inconsistent = true;989                    return;990                }991            }992        }993    }994995    fn discardClausesFrom(self: *Solver, retained_clause_count: usize) void {996        while (self.clauses.items.len > retained_clause_count) {997            const clause_index = self.clauses.items.len - 1;998            const clause = self.clauses.pop().?;999            _ = self.removeWatch(clause.literals[clause.watch_a], clause_index);1000            if (clause.watch_b != clause.watch_a) {1001                _ = self.removeWatch(clause.literals[clause.watch_b], clause_index);1002            }1003            if (clause.learned) {1004                assert(self.learned_clause_count > 0);1005                self.learned_clause_count -= 1;1006                if (clause.lbd <= glue_lbd_max) {1007                    assert(self.glue_clause_count > 0);1008                    self.glue_clause_count -= 1;1009                }1010            }1011            self.freeClauseLiterals(clause);1012        }1013    }10141015    fn freeClauseLiterals(self: *Solver, clause: Clause) void {1016        switch (clause.storage) {1017            .heap => self.allocator.free(clause.literals),1018            .pool => self.learnedPool().release(clause.literals),1019        }1020    }10211022    fn learnedPool(self: *Solver) *store.Store {1023        assert(self.learned_store != null);1024        return &self.learned_store.?;1025    }10261027    fn decisionLevel(self: *const Solver) u32 {1028        return @intCast(self.decision_limits.items.len);1029    }10301031    fn newDecisionLevel(self: *Solver) !void {1032        try self.decision_limits.append(self.allocator, self.trail.items.len);1033        const level = self.decisionLevel();1034        if (level > self.last_stats.max_decision_level) {1035            self.last_stats.max_decision_level = level;1036        }1037    }10381039    fn backtrack(self: *Solver, target_level: u32) void {1040        while (self.decisionLevel() > target_level) {1041            const start = self.decision_limits.pop().?;1042            var index = self.trail.items.len;1043            while (index > start) {1044                index -= 1;1045                const variable_index = self.trail.items[index].variable();1046                self.assignment.items[variable_index] = .unset;1047                self.reason.items[variable_index] = null;1048                self.level.items[variable_index] = 0;1049            }1050            self.trail.shrinkRetainingCapacity(start);1051            if (self.propagation_cursor > start) self.propagation_cursor = start;1052        }1053    }10541055    fn enqueue(self: *Solver, literal: Literal, reason: ?usize) !bool {1056        const variable_index = literal.variable();1057        assert(variable_index < self.variableCount());1058        const current = self.literalValue(literal);1059        if (current == .true) return true;1060        if (current == .false) return false;1061        self.assignment.items[variable_index] = BoolValue.fromBool(literal.isPositive());1062        self.saved_phase.items[variable_index] = self.assignment.items[variable_index];1063        self.level.items[variable_index] = self.decisionLevel();1064        self.reason.items[variable_index] = reason;1065        try self.trail.append(self.allocator, literal);1066        return true;1067    }10681069    fn propagate(self: *Solver) !PropagationResult {1070        while (self.propagation_cursor < self.trail.items.len) {1071            const literal = self.trail.items[self.propagation_cursor];1072            self.propagation_cursor += 1;1073            const false_literal = literal.negated();1074            const watch = &self.watches.items[false_literal.index()];1075            var index: usize = 0;1076            while (index < watch.items.len) {1077                const clause_index = watch.items[index].index;1078                const update = try self.propagateClause(clause_index, false_literal);1079                switch (update) {1080                    .moved => {1081                        _ = watch.swapRemove(index);1082                    },1083                    .kept => {1084                        index += 1;1085                    },1086                    .unit => |unit_literal| {1087                        if (!try self.enqueue(unit_literal, clause_index)) {1088                            return .{ .conflict = clause_index };1089                        }1090                        self.last_stats.propagations += 1;1091                        index += 1;1092                    },1093                    .conflict => return .{ .conflict = clause_index },1094                }1095            }1096        }1097        return .consistent;1098    }10991100    fn propagateClause(1101        self: *Solver,1102        clause_index: usize,1103        false_literal: Literal,1104    ) !ClausePropagation {1105        var clause = &self.clauses.items[clause_index];1106        const false_watch_is_a = clause.literals[clause.watch_a].raw == false_literal.raw;1107        const false_watch = if (false_watch_is_a) clause.watch_a else clause.watch_b;1108        const other_watch = if (false_watch_is_a) clause.watch_b else clause.watch_a;1109        const other_literal = clause.literals[other_watch];1110        if (self.literalValue(other_literal) == .true) return .kept;1111        for (clause.literals, 0..) |candidate, candidate_index| {1112            if (candidate_index == other_watch or candidate_index == false_watch) continue;1113            if (self.literalValue(candidate) != .false) {1114                if (false_watch_is_a) {1115                    clause.watch_a = candidate_index;1116                } else {1117                    clause.watch_b = candidate_index;1118                }1119                try self.addWatch(candidate, clause_index);1120                return .moved;1121            }1122        }1123        return switch (self.literalValue(other_literal)) {1124            .unset => .{ .unit = other_literal },1125            .false => .conflict,1126            .true => .kept,1127        };1128    }11291130    fn learnFromConflict(1131        self: *Solver,1132        owner: *scratch.ConflictScratch,1133        clause_index: usize,1134    ) !bool {1135        assert(owner.capacity.variables == self.variableCount());1136        const storage = self.conflictScratchStorage(owner.capacity);1137        assert(storage.ptr == owner.storage.ptr);1138        assert(storage.len == owner.storage.len);1139        var loan: scratch.ConflictScratch.Loan = undefined;1140        try owner.acquire(self.variableCount(), &loan);1141        defer owner.release(&loan) catch unreachable;1142        const conflict_level = self.decisionLevel();1143        var path_count: usize = 0;1144        var clause_ref = clause_index;1145        var cursor = self.trail.items.len;1146        var resolved_literal: ?Literal = null;1147        while (true) {1148            try loan.recordResolution();1149            const clause = self.clauses.items[clause_ref];1150            for (clause.literals) |literal| {1151                const variable_index = literal.variable();1152                if (!try loan.markSeen(variable_index)) continue;1153                if (self.level.items[variable_index] == conflict_level) {1154                    path_count += 1;1155                } else {1156                    try loan.append(literal);1157                }1158            }1159            while (cursor > 0) {1160                cursor -= 1;1161                const trail_literal = self.trail.items[cursor];1162                if (try loan.isSeen(trail_literal.variable())) {1163                    resolved_literal = trail_literal;1164                    break;1165                }1166            }1167            const pivot = resolved_literal orelse return error.InvalidConflictGraph;1168            try loan.clearSeen(pivot.variable());1169            path_count -= 1;1170            if (path_count == 0) {1171                try loan.append(pivot.negated());1172                break;1173            }1174            clause_ref = self.reason.items[pivot.variable()] orelse {1175                try loan.append(pivot.negated());1176                break;1177            };1178        }1179        const learned = try loan.literals();1180        var backtrack_level: u32 = 0;1181        for (learned) |literal| {1182            const literal_level = self.level.items[literal.variable()];1183            if (literal_level != conflict_level and literal_level > backtrack_level) {1184                backtrack_level = literal_level;1185            }1186        }1187        const lbd = self.blockDistance(learned);1188        if (!self.rupCheckConflict(learned, clause_index)) return error.InvalidProofTrace;1189        self.backtrack(backtrack_level);1190        const assert_literal = learned[learned.len - 1];1191        try self.addLearnedClause(learned, lbd);1192        return try self.enqueue(assert_literal, self.clauses.items.len - 1);1193    }11941195    fn blockDistance(self: *const Solver, literals: []const Literal) u32 {1196        assert(literals.len > 0);1197        var distinct: u32 = 0;1198        for (literals, 0..) |literal, index| {1199            const literal_level = self.level.items[literal.variable()];1200            var counted = false;1201            for (literals[0..index]) |prior| {1202                if (self.level.items[prior.variable()] == literal_level) {1203                    counted = true;1204                    break;1205                }1206            }1207            if (!counted) distinct += 1;1208        }1209        assert(distinct >= 1);1210        assert(distinct <= literals.len);1211        return distinct;1212    }12131214    fn addLearnedClause(self: *Solver, literals: []const Literal, lbd: u32) !void {1215        assert(lbd >= 1);1216        assert(lbd <= literals.len);1217        try self.appendProofStep(literals);1218        errdefer self.removeLastProofStep();1219        const pooled = self.learned_store != null and lbd > glue_lbd_max;1220        const owned = if (pooled)1221            self.learnedPool().acquire(literals)1222        else1223            try self.allocator.dupe(Literal, literals);1224        errdefer if (pooled) self.learnedPool().release(owned) else self.allocator.free(owned);1225        const clause_index = self.clauses.items.len;1226        const clause = Clause{1227            .literals = owned,1228            .learned = true,1229            .lbd = lbd,1230            .storage = if (pooled) .pool else .heap,1231            .watch_a = 0,1232            .watch_b = if (owned.len > 1) 1 else 0,1233        };1234        try self.clauses.append(self.allocator, clause);1235        errdefer _ = self.clauses.pop();1236        try self.addWatch(owned[0], clause_index);1237        errdefer _ = self.removeWatch(owned[0], clause_index);1238        if (owned.len > 1) {1239            try self.addWatch(owned[1], clause_index);1240        }1241        self.learned_clause_count += 1;1242        if (lbd <= glue_lbd_max) self.glue_clause_count += 1;1243        self.last_stats.learned_clauses += 1;1244    }12451246    fn nextUnassignedVariable(self: *const Solver) ?u32 {1247        for (self.assignment.items, 0..) |assigned_value, index| {1248            if (assigned_value == .unset) return @intCast(index);1249        }1250        return null;1251    }12521253    fn decisionLiteral(self: *const Solver, variable_index: u32) Literal {1254        return switch (self.saved_phase.items[variable_index]) {1255            .false => Literal.negative(variable_index),1256            .true, .unset => Literal.positive(variable_index),1257        };1258    }1259};

1pub const Solver = sat.Solver;