lib/smt/src/sat/solver.zig
daab053ee43316e1809a84551d573ddd1e5bf3d2
1 //! A SAT solver that learns a new clause from each conflict it analyzes. The solver decides whether
2 //! clauses over Boolean variables can all be made true, optionally under assumed literals, and
3 //! 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 can
7 //! confirm. A caller that asks many questions of one formula wants each question to leave the
8 //! clauses as they were, and a caller that bounds its work wants limits on search time and on
9 //! memory.
10 //!
11 //! Each assignment can make any clause that contains the opposite literal unit or false, and a
12 //! 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. An
14 //! unsatisfiable answer is only as sound as the search that gave it, so each learned clause and the
15 //! 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, is
18 //! a SAT solver that learns a clause from each conflict. The package keeps its way of solving, with
19 //! unsat cores and proofs: each clause of two or more literals watches two of them, each conflict
20 //! 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 one
23 //! literal, so an assignment visits only the clauses that watch the literal it makes false. The
24 //! search decides the lowest unassigned variable and gives it the value it last held, or true for a
25 //! variable assigned for the first time. At each conflict above decision level zero, the solver
26 //! resolves back to one literal of the conflict's level, learns the resulting clause, and
27 //! backtracks to the highest other level among its literals. Before keeping a learned clause, the
28 //! solver replays the propagation that led to the conflict and checks that the clause follows, and
29 //! 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 block
32 //! distance). A cap on learned clauses (`max_learned_clauses`) bounds only the learned clauses
33 //! whose literals span more than two decision levels (*replaceable learned clauses*), and the
34 //! others stay for as long as the solver holds its clauses. When their count passes the cap, the
35 //! solver returns to decision level zero and removes them, highest block distance first and then
36 //! 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 search
38 //! (`LearnedStore`). Under a conflict limit (`conflict_budget`), the solver keeps its proof steps
39 //! in fixed memory sized from the limit (`ProofTrace`). The solver analyzes each conflict in
40 //! scratch memory at the end of its list of assigned literals in assignment order
41 //! (`ConflictScratch`). After a scheduled conflict count, the solver returns to decision level zero
42 //! 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 is
45 //! 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 clause
47 //! 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 pop
49 //! returns to (an *assumption frame*). After an unsatisfiable answer under assumptions, the solver
50 //! records as the core the assumptions it had assigned when the conflict came, which is every
51 //! assumption unless the conflict came while it assigned them. When that recorded core holds two or
52 //! more assumptions, the solver drops one assumption at a time, keeps each drop that fresh solvers
53 //! over the caller's clauses still refute, and certifies the final set with one more solve. Under a
54 //! conflict limit, those extra solves share what is left of the limit. When it runs out during the
55 //! drops, the answer is `.unsat` with every assumption in the core. When it runs out during the
56 //! 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 final
59 //! empty clause that is checked before it is recorded. Adding a variable, a clause or an
60 //! 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, the
62 //! 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 under
64 //! every assumption of the solve, ending in the empty clause. The assignment of the last search
65 //! stays until the next solve. When a unit clause added after a solve has a literal that this
66 //! assignment makes false, every later solve skips the search and checks the final empty clause at
67 //! once, so it returns `error.InvalidProofTrace` for a formula that is still satisfiable.
68 const std = @import("std");
69 const proof = @import("proof.zig");
70 const scratch = @import("scratch.zig");
71 const store = @import("store.zig");
72 const trace = @import("trace.zig");
73 const types = @import("types.zig");
74
75 const assert = std.debug.assert;
76
77 pub const BoolValue = types.BoolValue;
78 pub const Literal = types.Literal;
79 pub const ProofArtifact = proof.ProofArtifact;
80 pub const ProofStep = proof.ProofStep;
81 pub const RestartPolicy = types.RestartPolicy;
82 pub const SolveStats = types.SolveStats;
83 pub const Status = types.Status;
84
85 const ClauseStorage = enum {
86 heap,
87 pool,
88 };
89
90 const Clause = struct {
91 literals: []Literal,
92 learned: bool,
93 lbd: u32,
94 storage: ClauseStorage,
95 watch_a: usize,
96 watch_b: usize,
97 };
98
99 const ClauseRef = struct {
100 index: usize,
101 };
102
103 const glue_lbd_max: u32 = 2;
104
105 const PropagationResult = union(enum) {
106 consistent,
107 conflict: usize,
108 };
109
110 const ProbeOutcome = struct {
111 status: Status,
112 conflicts: usize,
113 };
114
115 const ClausePropagation = union(enum) {
116 kept,
117 moved,
118 unit: Literal,
119 conflict,
120 };
121
122 /// A SAT solver that learns a clause from each conflict above decision level zero over the clauses
123 /// a caller adds, answers under assumed literals, and records an unsat core and a proof trace after
124 /// each unsatisfiable answer. The package's bit-vector encoder (`bitvec.Encoder`) turns terms into
125 /// variables and clauses of a solver it is given, and a caller then solves and reads the answer
126 /// through the solver. `init` takes an allocator, and the solver allocates every list, clause copy
127 /// and proof step with it and frees them in `deinit`. A caller sets `conflict_budget` and
128 /// `max_learned_clauses`, and reads `clauses` and `has_empty_clause`. The other fields are search
129 /// state, which a caller reads through the solver's functions. Each clause of two or more literals
130 /// watches two of them, and a unit clause watches its one literal. A decision gives the variable
131 /// the value it last held, or true for a variable assigned for the first time. The list of assigned
132 /// literals in assignment order has room past the variable count for the scratch memory of conflict
133 /// analysis (`ConflictScratch`).
134 pub const Solver = struct {
135 allocator: std.mem.Allocator,
136 /// Every clause the solver holds: the caller's nonempty clauses and the learned clauses it
137 /// 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 last
139 /// clause moves into the removed clause's place. A solve with assumptions removes the clauses
140 /// added during it when it returns. `clauseCount` counts the list, and `dimacs.write` writes it
141 /// 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 and
164 /// the variable count (`ProofTrace`). The extra solves of core minimization share what is left
165 /// 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 learned
168 /// 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, the
170 /// solver removes replaceable learned clauses, highest block distance first and then the
171 /// longest. The solver keeps each clause that justifies a current value and the newly learned
172 /// clause, so the count can pass the cap by those clauses. While it is set, the solver keeps
173 /// replaceable learned clauses in fixed memory sized from the cap and the variable count
174 /// (`LearnedStore`). After a caller sets it back to `null`, the next solve moves those clauses
175 /// 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 starting
185 /// clause for it. The solver's own proof checks accept every step while it is set. The default
186 /// is false.
187 has_empty_clause: bool = false,
188 inconsistent: bool = false,
189
190 /// Returns an empty solver that allocates with `allocator`. A caller creates one solver per
191 /// 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 }
195
196 /// Frees every clause, list, fixed store, trace and proof step, and leaves the solver
197 /// undefined. The owner of a solver calls it once, when it is done with the formula. Slices
198 /// from `lastUnsatCore`, `lastProofTrace` and `activeAssumptions` become invalid. Artifacts
199 /// 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 }
226
227 /// Returns the number of variables: one more than the highest variable index the solver has
228 /// added or seen. A caller reports it as a size of the encoded formula. A clause or an
229 /// assumption that names a higher variable raises it.
230 pub fn variableCount(self: *const Solver) usize {
231 return self.assignment.items.len;
232 }
233
234 /// Returns the number of entries in `clauses`. A caller reports it as a size of the encoded
235 /// formula, and `dimacs.write` prints it in its header. The count includes the learned clauses
236 /// 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 }
240
241 /// Returns the number of learned clauses the solver holds, at every block distance. A caller
242 /// checks how many learned clauses survive a capped search. The count drops when the solver
243 /// 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 }
247
248 /// Returns the number of learned clauses whose literals span more than two decision levels. A
249 /// caller compares it with `max_learned_clauses` after a capped search. These are the clauses
250 /// 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 }
255
256 /// Sets the restart schedule for later solves. A caller that wants restarts at a different
257 /// pace, such as after every conflict, sets it before solving. The schedule takes effect at the
258 /// start of the next solve.
259 pub fn setRestartPolicy(self: *Solver, policy: RestartPolicy) void {
260 self.restart_policy = policy;
261 }
262
263 /// Returns the restart schedule later solves use. A caller reads back the schedule that
264 /// `setRestartPolicy` set, or the default.
265 pub fn restartPolicy(self: *const Solver) RestartPolicy {
266 return self.restart_policy;
267 }
268
269 /// Adds one unassigned variable and returns its index, counting from 0. `bitvec.Encoder` adds a
270 /// variable for each Boolean it encodes, and `dimacs.parse` adds the variable count of its
271 /// 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 }
281
282 /// 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 clause
284 /// of its input. The caller keeps `literals`. An empty slice sets `has_empty_clause`, and every
285 /// later solve answers `.unsat`. The solver assigns the literal of a unit clause at once. When
286 /// the literal of a unit clause is false under the assignment the last search left, every later
287 /// solve skips the search and checks the final empty clause at once, so it returns
288 /// `error.InvalidProofTrace` for a formula that is still satisfiable. The call clears the
289 /// recorded core and trace. The call returns `error.OutOfMemory` when a copy or a list fails to
290 /// 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 }
324
325 /// Solves the clauses alone, as `solveWithAssumptions` does with an empty list. A caller that
326 /// 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 }
331
332 /// Saves the current length of the assumption list, so the next `popAssumptionFrame` returns
333 /// the list to it. A caller that nests questions pushes a frame before it assumes the literals
334 /// of an inner question. The call clears the recorded core and trace. The call returns
335 /// `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 }
341
342 /// Returns the assumption list to the length the latest push saved and closes that frame. A
343 /// caller that nests questions pops a frame to leave an inner question. With no frame open, the
344 /// 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 }
351
352 /// Adds `literal` to the solver's assumption list and adds its variable when the solver lacks
353 /// it. `bitvec.Encoder` assumes the literal of each assumed term through it, for a later
354 /// `solveWithActiveAssumptions`. The literal stays in the list until a pop past its frame or
355 /// `clearAssumptionFrames`. The call clears the recorded core and trace. The call returns
356 /// `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 }
363
364 /// Empties the assumption list and closes every frame. A caller that starts a new round of
365 /// questions calls it to drop every assumption and frame at once. The call clears the recorded
366 /// 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 }
373
374 /// 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 }
379
380 /// Returns the solver's assumption list, oldest first. A caller reads the assumptions in force
381 /// 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 }
385
386 /// 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 }
390
391 /// Returns a set of the last solve's assumptions that the clauses refute together, after an
392 /// unsatisfiable answer. A caller maps the core back to the named assumptions it made, to
393 /// report which of them conflict. The solver first records as the core the assumptions it had
394 /// assigned when the conflict came. When that recorded core holds two or more assumptions, the
395 /// core is the smaller set that the extra solves of core minimization certified. The core is
396 /// empty when the clauses were refuted before the search began, as by two opposite unit clauses
397 /// or an empty clause, after a satisfiable or unknown answer, and after any change that clears
398 /// it. A recorded core of one assumption stays as it is, because core minimization runs only
399 /// for two or more, so the core can hold that assumption even when the clauses alone are
400 /// unsatisfiable. A conflict while the solver assigns the assumptions records only those
401 /// assigned so far, so a solve under two or more assumptions can end with a core of one and no
402 /// shrinking. Under a conflict limit, the core holds every assumption when the limit ran out
403 /// during the drops, and it is empty with an `.unknown` answer when the limit ran out during
404 /// 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 }
408
409 /// Returns the work counts of the last solve. A caller reports them beside the answer. A solve
410 /// 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. The
412 /// 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 }
416
417 /// Returns the proof steps of the last solve, in order. A caller reads the steps in place, and
418 /// `lastProofArtifact` makes a copy that outlives later changes. The trace holds one step per
419 /// learned clause and, after an unsatisfiable answer, a final empty clause. After a satisfiable
420 /// or unknown answer, the trace can still hold the steps learned during the solve. The slices
421 /// 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 }
425
426 /// Returns true when the trace is nonempty, each step follows by unit propagation from the
427 /// starting clauses, the assumptions and the earlier steps, and the last step is the empty
428 /// clause. A caller confirms an unsatisfiable answer in place. The check accepts every step
429 /// 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 }
437
438 /// 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. A
440 /// 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 solve
442 /// began, learned clauses it kept included, then an empty clause when `has_empty_clause` is
443 /// set. The artifact covers the solver's variable count. After a solve that learned clauses and
444 /// then answered `.sat`, or `.unknown` at the main search's conflict limit, the call returns an
445 /// artifact that `ProofArtifact.valid` rejects. After an `.unknown` answer from the certifying
446 /// solve of core minimization, the artifact holds the refutation under every assumption of the
447 /// solve, and `ProofArtifact.valid` accepts it. The call returns `error.OutOfMemory` when a
448 /// 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 }
465
466 /// Decides whether the clauses and every literal of `assumptions` can all be true, and returns
467 /// `.sat`, `.unsat` or `.unknown`. A caller asks a question under temporary hypotheses and
468 /// 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 had
471 /// assigned when the conflict came, the smaller set that core minimization certified when that
472 /// recorded core holds two or more, or every assumption of the solve when a conflict limit runs
473 /// out while core minimization drops assumptions. When `assumptions` is nonempty, every clause
474 /// added during the solve is removed when the solve returns. The solve clears the recorded
475 /// core, trace and counts only after it has made room for conflict analysis, so a failure
476 /// 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 overflows
478 /// `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 resolve
480 /// on, `error.InvalidUnsatCore` when the certifying solve satisfies the core, and the errors of
481 /// `ConflictScratch`. The assignment stays after the call, and `value` and `literalValue` read
482 /// it.
483 pub fn solveWithAssumptions(self: *Solver, assumptions: []const Literal) !Status {
484 return try self.solveWithAssumptionsMode(assumptions, true);
485 }
486
487 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 }
590
591 /// Returns the value of `variable_index` in the current assignment, or null when the variable
592 /// is unassigned or at or above the variable count. A caller reads a satisfying assignment
593 /// 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 }
602
603 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 }
613
614 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 }
665
666 fn poolDrained(pool: ?usize) bool {
667 return if (pool) |remaining| remaining == 0 else false;
668 }
669
670 fn drainPool(pool: *?usize, spent: usize) void {
671 if (pool.*) |remaining| pool.* = remaining -| spent;
672 }
673
674 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 }
684
685 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 }
698
699 fn recordUnsatCore(self: *Solver, assumptions: []const Literal) !void {
700 self.last_core.clearRetainingCapacity();
701 try self.last_core.appendSlice(self.allocator, assumptions);
702 }
703
704 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 }
709
710 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 }
726
727 fn clearSolveEvidence(self: *Solver) void {
728 self.clearProofTrace();
729 self.last_core.clearRetainingCapacity();
730 self.last_stats = .{};
731 }
732
733 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 }
740
741 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 }
751
752 fn appendProofStep(self: *Solver, literals: []const Literal) !void {
753 try self.appendStepStorage(literals);
754 self.last_stats.proof_steps += 1;
755 }
756
757 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 }
766
767 fn recordFinalProofStep(self: *Solver) !void {
768 if (!self.rupCheck(&.{}, self.proof_steps.items.len)) return error.InvalidProofTrace;
769 try self.appendProofStep(&.{});
770 }
771
772 fn traceBudget(self: *const Solver) ?usize {
773 if (!self.proof_trace_slab) return null;
774 return self.conflict_budget;
775 }
776
777 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 }
791
792 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 }
802
803 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 }
827
828 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 }
843
844 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 }
857
858 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 }
869
870 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 }
893
894 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 }
907
908 fn maybeRestart(self: *Solver) void {
909 if (self.next_restart_conflicts != 0 and
910 self.decisionLevel() > 0 and
911 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 }
936
937 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 }
950
951 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 }
967
968 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 }
974
975 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 }
982
983 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 }
990
991 /// 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` reads
993 /// each Boolean of a model through it. The values form a satisfying assignment only after
994 /// `.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 }
1000
1001 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 }
1022
1023 fn addWatch(self: *Solver, literal: Literal, clause_index: usize) !void {
1024 try self.watches.items[literal.index()].append(self.allocator, .{ .index = clause_index });
1025 }
1026
1027 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 }
1037
1038 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 }
1048
1049 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 }
1059
1060 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 }
1098
1099 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 }
1115
1116 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 }
1135
1136 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 }
1142
1143 fn learnedPool(self: *Solver) *store.Store {
1144 assert(self.learned_store != null);
1145 return &self.learned_store.?;
1146 }
1147
1148 fn decisionLevel(self: *const Solver) u32 {
1149 return @intCast(self.decision_limits.items.len);
1150 }
1151
1152 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 }
1159
1160 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 }
1175
1176 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 }
1189
1190 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 }
1220
1221 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 }
1250
1251 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 }
1315
1316 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 }
1334
1335 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 else
1344 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 }
1366
1367 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 }
1373
1374 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 };
1381
1382 fn 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 }
1389
1390 fn 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 }
1429
1430 fn 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 }
1443
1444 fn 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 }
1462
1463 fn 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 }
1473
1474 fn 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 }
1479
1480 test "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 }
1492
1493 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());
1511
1512 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);
1523
1524 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 }
1535
1536 test "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));
1552
1553 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 }
1564
1565 test "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 }
1588
1589 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 }
1626
1627 fn 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 }
1650
1651 test "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 }
1663
1664 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);
1676
1677 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);
1684
1685 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 }
1693
1694 fn 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 }
1706
1707 test "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 }
1719
1720 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);
1734
1735 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 }
1741
1742 test "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 }
1754
1755 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);
1769
1770 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);
1775
1776 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 }
1784
1785 test "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 }
1801
1802 test "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 }
1825
1826 test "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 }
1870
1871 test "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 }
1892
1893 test "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 }