lib/smt/src/sat/test.zig
daab053ee43316e1809a84551d573ddd1e5bf3d2
1 const namespace = @import("root.zig");
2 const std = @import("std");
3
4 const proof_module = @import("proof.zig");
5 const scratch_module = namespace.scratch;
6 const solver_module = namespace.solver;
7 const store_module = namespace.store;
8 const trace_module = namespace.trace;
9 const types_module = namespace.types;
10 const BoolValue = namespace.BoolValue;
11 const ConflictScratch = namespace.ConflictScratch;
12 const Literal = namespace.Literal;
13 const ProofArtifact = namespace.ProofArtifact;
14 const ProofClause = namespace.ProofClause;
15 const ProofStep = namespace.ProofStep;
16 const RestartPolicy = namespace.RestartPolicy;
17 const Solver = namespace.Solver;
18 const SolveStats = namespace.SolveStats;
19 const Status = namespace.Status;
20
21 test {
22 std.testing.refAllDecls(types_module);
23 std.testing.refAllDecls(proof_module);
24 std.testing.refAllDecls(scratch_module);
25 std.testing.refAllDecls(solver_module);
26 std.testing.refAllDecls(store_module);
27 std.testing.refAllDecls(trace_module);
28 }
29
30 test "sat solver accepts simple satisfiable clauses" {
31 var solver = Solver.init(std.testing.allocator);
32 defer solver.deinit();
33 const a = try solver.addVariable();
34 const b = try solver.addVariable();
35 try solver.addClause(&.{ Literal.positive(a), Literal.positive(b) });
36 try solver.addClause(&.{Literal.negative(a)});
37 try std.testing.expectEqual(Status.sat, try solver.solve());
38 try std.testing.expectEqual(false, solver.value(a).?);
39 try std.testing.expectEqual(true, solver.value(b).?);
40 }
41
42 test "sat solver reports decision stats" {
43 var solver = Solver.init(std.testing.allocator);
44 defer solver.deinit();
45 _ = try solver.addVariable();
46 try std.testing.expectEqual(Status.sat, try solver.solve());
47 const stats = solver.lastSolveStats();
48 try std.testing.expectEqual(@as(usize, 1), stats.decisions);
49 try std.testing.expectEqual(@as(usize, 0), stats.phase_saved_decisions);
50 try std.testing.expectEqual(@as(u32, 1), stats.max_decision_level);
51 try std.testing.expectEqual(@as(usize, 0), stats.conflicts);
52 try std.testing.expectEqual(@as(usize, 0), stats.root_conflicts);
53 }
54
55 test "sat solver saves phases across solves" {
56 var solver = Solver.init(std.testing.allocator);
57 defer solver.deinit();
58 const a = try solver.addVariable();
59 const b = try solver.addVariable();
60 try solver.addClause(&.{ Literal.positive(a), Literal.positive(b) });
61 try std.testing.expectEqual(
62 Status.sat,
63 try solver.solveWithAssumptions(&.{Literal.negative(a)}),
64 );
65 try std.testing.expectEqual(false, solver.value(a).?);
66 try std.testing.expectEqual(true, solver.value(b).?);
67 try std.testing.expectEqual(Status.sat, try solver.solve());
68 try std.testing.expectEqual(false, solver.value(a).?);
69 try std.testing.expectEqual(true, solver.value(b).?);
70 const stats = solver.lastSolveStats();
71 try std.testing.expect(stats.phase_saved_decisions > 0);
72 }
73
74 test "sat solver detects unsatisfiable unit conflict" {
75 var solver = Solver.init(std.testing.allocator);
76 defer solver.deinit();
77 const a = try solver.addVariable();
78 try solver.addClause(&.{Literal.positive(a)});
79 try solver.addClause(&.{Literal.negative(a)});
80 try std.testing.expectEqual(Status.unsat, try solver.solve());
81 try std.testing.expectEqual(@as(usize, 0), solver.lastUnsatCore().len);
82 try std.testing.expectEqual(@as(usize, 1), solver.lastProofTrace().len);
83 try std.testing.expectEqual(@as(usize, 0), solver.lastProofTrace()[0].literals.len);
84 try std.testing.expect(solver.lastProofTraceValid());
85 const stats = solver.lastSolveStats();
86 try std.testing.expectEqual(@as(usize, 1), stats.conflicts);
87 try std.testing.expectEqual(@as(usize, 1), stats.root_conflicts);
88 try std.testing.expectEqual(@as(usize, 1), stats.proof_steps);
89 }
90
91 test "base inconsistency keeps artifact scope broader than its empty core" {
92 var solver = Solver.init(std.testing.allocator);
93 defer solver.deinit();
94 const a = try solver.addVariable();
95 const b = try solver.addVariable();
96 try solver.addClause(&.{Literal.positive(a)});
97 try solver.addClause(&.{Literal.negative(a)});
98 const assumption = Literal.positive(b);
99 try std.testing.expectEqual(
100 Status.unsat,
101 try solver.solveWithAssumptions(&.{assumption}),
102 );
103 try std.testing.expectEqual(@as(usize, 0), solver.lastUnsatCore().len);
104 var artifact = (try solver.lastProofArtifact(std.testing.allocator)).?;
105 defer artifact.deinit();
106 try std.testing.expectEqualSlices(
107 Literal,
108 &.{assumption},
109 artifact.assumptions.items,
110 );
111 try std.testing.expect(try artifact.valid());
112 }
113
114 test "sat solver conflict scratch preserves binary implication learning" {
115 comptime {
116 @stardustClaim(
117 @import("alloc_phase").capacity.witness(ConflictScratch, "smt_conflict_scratch_solver_semantics"),
118 null,
119 null,
120 null,
121 null,
122 null,
123 null,
124 );
125 }
126
127 var solver = Solver.init(std.testing.allocator);
128 defer solver.deinit();
129 const a = try solver.addVariable();
130 const b = try solver.addVariable();
131 try solver.addClause(&.{ Literal.positive(a), Literal.positive(b) });
132 try solver.addClause(&.{ Literal.negative(a), Literal.positive(b) });
133 try solver.addClause(&.{ Literal.positive(a), Literal.negative(b) });
134 try solver.addClause(&.{ Literal.negative(a), Literal.negative(b) });
135 try std.testing.expectEqual(Status.unsat, try solver.solve());
136 const proof = solver.lastProofTrace();
137 try std.testing.expect(proof.len > 1);
138 try std.testing.expectEqual(@as(usize, 0), proof[proof.len - 1].literals.len);
139 try std.testing.expect(solver.lastProofTraceValid());
140 const stats = solver.lastSolveStats();
141 try std.testing.expect(stats.propagations > 0);
142 try std.testing.expect(stats.conflicts > 0);
143 try std.testing.expect(stats.learned_clauses > 0);
144 try std.testing.expectEqual(proof.len, stats.proof_steps);
145 try std.testing.expect(stats.max_decision_level > 0);
146 try std.testing.expect(stats.root_conflicts > 0);
147 const scratch_capacity = try ConflictScratch.Capacity.derive(.{ .variables = 2 });
148 const scratch_pointer = solver.trail.allocatedSlice()[scratch_capacity.variables..].ptr;
149 try std.testing.expect(solver.trail.capacity >= scratch_capacity.trail_capacity);
150 try std.testing.expectEqual(Status.unsat, try solver.solve());
151 try std.testing.expectEqual(
152 scratch_pointer,
153 solver.trail.allocatedSlice()[scratch_capacity.variables..].ptr,
154 );
155 const repeated_proof = solver.lastProofTrace();
156 try std.testing.expect(repeated_proof.len > 0);
157 try std.testing.expectEqual(@as(usize, 0), repeated_proof[repeated_proof.len - 1].literals.len);
158 try std.testing.expect(solver.lastProofTraceValid());
159 }
160
161 test "conflict scratch growth rejects before solve evidence mutation and retries" {
162 comptime {
163 @stardustClaim(
164 @import("alloc_phase").capacity.witness(ConflictScratch, "smt_conflict_scratch_solver_admission"),
165 null,
166 null,
167 null,
168 null,
169 null,
170 null,
171 );
172 }
173
174 var failing = std.testing.FailingAllocator.init(std.testing.allocator, .{});
175 var solver = Solver.init(failing.allocator());
176 defer solver.deinit();
177 const a = try solver.addVariable();
178 const b = try solver.addVariable();
179 try solver.addClause(&.{ Literal.positive(a), Literal.positive(b) });
180 try solver.addClause(&.{ Literal.negative(a), Literal.positive(b) });
181 try solver.addClause(&.{ Literal.positive(a), Literal.negative(b) });
182 try solver.addClause(&.{ Literal.negative(a), Literal.negative(b) });
183 try std.testing.expectEqual(Status.unsat, try solver.solve());
184 try std.testing.expect(solver.lastProofTraceValid());
185 const proof_pointer = solver.lastProofTrace().ptr;
186 const proof_length = solver.lastProofTrace().len;
187 const scratch_capacity = try ConflictScratch.Capacity.derive(.{ .variables = 2 });
188 const scratch_pointer = solver.trail.allocatedSlice()[scratch_capacity.variables..].ptr;
189 const trail_capacity = solver.trail.capacity;
190
191 failing.fail_index = failing.alloc_index;
192 try std.testing.expectError(
193 error.OutOfMemory,
194 solver.solveWithAssumptions(&.{Literal.positive(10)}),
195 );
196 try std.testing.expectEqual(proof_pointer, solver.lastProofTrace().ptr);
197 try std.testing.expectEqual(proof_length, solver.lastProofTrace().len);
198 try std.testing.expect(solver.lastProofTraceValid());
199 try std.testing.expectEqual(
200 scratch_pointer,
201 solver.trail.allocatedSlice()[scratch_capacity.variables..].ptr,
202 );
203 try std.testing.expectEqual(trail_capacity, solver.trail.capacity);
204
205 failing.fail_index = std.math.maxInt(usize);
206 failing.resize_fail_index = std.math.maxInt(usize);
207 try std.testing.expectEqual(
208 Status.unsat,
209 try solver.solveWithAssumptions(&.{Literal.positive(10)}),
210 );
211 const grown = try ConflictScratch.Capacity.derive(.{ .variables = 11 });
212 try std.testing.expect(solver.trail.capacity >= grown.trail_capacity);
213 try std.testing.expect(solver.lastProofTraceValid());
214 }
215
216 test "sat solver exports independent proof artifact" {
217 var solver = Solver.init(std.testing.allocator);
218 defer solver.deinit();
219 const a = try solver.addVariable();
220 const b = try solver.addVariable();
221 try solver.addClause(&.{ Literal.positive(a), Literal.positive(b) });
222 try solver.addClause(&.{ Literal.negative(a), Literal.positive(b) });
223 try solver.addClause(&.{ Literal.positive(a), Literal.negative(b) });
224 try solver.addClause(&.{ Literal.negative(a), Literal.negative(b) });
225 try std.testing.expectEqual(Status.unsat, try solver.solve());
226 var artifact = (try solver.lastProofArtifact(std.testing.allocator)).?;
227 defer artifact.deinit();
228 try std.testing.expect(try artifact.valid());
229 _ = try solver.addVariable();
230 try std.testing.expectEqual(@as(usize, 0), solver.lastProofTrace().len);
231 try std.testing.expect(try artifact.valid());
232 }
233
234 test "sat proof artifact rejects unproven empty step" {
235 var artifact = ProofArtifact.init(std.testing.allocator, 1);
236 defer artifact.deinit();
237 try artifact.appendStep(&.{});
238 try std.testing.expectEqual(false, try artifact.valid());
239 }
240
241 test "sat proof artifact records assumptions" {
242 var solver = Solver.init(std.testing.allocator);
243 defer solver.deinit();
244 const a = try solver.addVariable();
245 const b = try solver.addVariable();
246 try solver.addClause(&.{ Literal.positive(a), Literal.positive(b) });
247 try std.testing.expectEqual(
248 Status.unsat,
249 try solver.solveWithAssumptions(&.{ Literal.negative(a), Literal.negative(b) }),
250 );
251 var artifact = (try solver.lastProofArtifact(std.testing.allocator)).?;
252 defer artifact.deinit();
253 try std.testing.expectEqual(@as(usize, 2), artifact.assumptions.items.len);
254 try std.testing.expect(try artifact.valid());
255 }
256
257 test "sat solver clears proof trace after satisfiable solve" {
258 var solver = Solver.init(std.testing.allocator);
259 defer solver.deinit();
260 const a = try solver.addVariable();
261 const b = try solver.addVariable();
262 try solver.addClause(&.{ Literal.positive(a), Literal.positive(b) });
263 try std.testing.expectEqual(
264 Status.unsat,
265 try solver.solveWithAssumptions(&.{ Literal.negative(a), Literal.negative(b) }),
266 );
267 try std.testing.expect(solver.lastProofTraceValid());
268 try std.testing.expectEqual(Status.sat, try solver.solve());
269 try std.testing.expectEqual(@as(usize, 0), solver.lastProofTrace().len);
270 try std.testing.expectEqual(false, solver.lastProofTraceValid());
271 }
272
273 test "sat solver restarts after learned conflicts" {
274 var solver = Solver.init(std.testing.allocator);
275 defer solver.deinit();
276 solver.setRestartPolicy(.{ .first_conflict_interval = 1, .growth = 1 });
277 const a = try solver.addVariable();
278 const b = try solver.addVariable();
279 const c = try solver.addVariable();
280 try solver.addClause(&.{ Literal.negative(a), Literal.negative(b), Literal.positive(c) });
281 try solver.addClause(&.{ Literal.negative(a), Literal.negative(b), Literal.negative(c) });
282 try solver.addClause(&.{ Literal.positive(a), Literal.positive(b) });
283 try std.testing.expectEqual(Status.sat, try solver.solve());
284 const stats = solver.lastSolveStats();
285 try std.testing.expect(stats.restarts > 0);
286 try std.testing.expect(stats.learned_clauses > 0);
287 }
288
289 test "sat solver supports assumptions" {
290 var solver = Solver.init(std.testing.allocator);
291 defer solver.deinit();
292 const a = try solver.addVariable();
293 const b = try solver.addVariable();
294 try solver.addClause(&.{ Literal.positive(a), Literal.positive(b) });
295 try std.testing.expectEqual(
296 Status.sat,
297 try solver.solveWithAssumptions(&.{Literal.negative(a)}),
298 );
299 try std.testing.expectEqual(true, solver.value(b).?);
300 try std.testing.expectEqual(
301 Status.unsat,
302 try solver.solveWithAssumptions(&.{ Literal.negative(a), Literal.negative(b) }),
303 );
304 try std.testing.expectEqualSlices(
305 Literal,
306 &.{ Literal.negative(a), Literal.negative(b) },
307 solver.lastUnsatCore(),
308 );
309 }
310
311 test "sat solver prunes irrelevant assumptions from unsat core" {
312 var solver = Solver.init(std.testing.allocator);
313 defer solver.deinit();
314 const a = try solver.addVariable();
315 const b = try solver.addVariable();
316 const c = try solver.addVariable();
317 try solver.addClause(&.{Literal.positive(a)});
318 const assumptions = [_]Literal{ Literal.negative(b), Literal.negative(a), Literal.negative(c) };
319 try std.testing.expectEqual(Status.unsat, try solver.solveWithAssumptions(&assumptions));
320 try std.testing.expectEqualSlices(Literal, &.{Literal.negative(a)}, solver.lastUnsatCore());
321 var artifact = (try solver.lastProofArtifact(std.testing.allocator)).?;
322 defer artifact.deinit();
323 try std.testing.expectEqualSlices(Literal, &.{Literal.negative(a)}, artifact.assumptions.items);
324 try std.testing.expect(try artifact.valid());
325 }
326
327 test "sat solver keeps core proof scope and step statistics aligned" {
328 var solver = Solver.init(std.testing.allocator);
329 defer solver.deinit();
330 const a = try solver.addVariable();
331 const b = try solver.addVariable();
332 const c = try solver.addVariable();
333 try solver.addClause(&.{ Literal.negative(a), Literal.positive(b), Literal.positive(c) });
334 try solver.addClause(&.{ Literal.negative(a), Literal.positive(b), Literal.negative(c) });
335 try solver.addClause(&.{ Literal.negative(a), Literal.negative(b), Literal.positive(c) });
336 try solver.addClause(&.{ Literal.negative(a), Literal.negative(b), Literal.negative(c) });
337 const assumptions = [_]Literal{ Literal.positive(a), Literal.negative(b) };
338
339 solver.conflict_budget = 4;
340 try std.testing.expectEqual(Status.unsat, try solver.solveWithAssumptions(&assumptions));
341 try std.testing.expectEqualSlices(Literal, &assumptions, solver.lastUnsatCore());
342 var budgeted = (try solver.lastProofArtifact(std.testing.allocator)).?;
343 defer budgeted.deinit();
344 try std.testing.expectEqualSlices(Literal, solver.lastUnsatCore(), budgeted.assumptions.items);
345 try std.testing.expectEqual(budgeted.steps.items.len, solver.lastSolveStats().proof_steps);
346
347 solver.conflict_budget = null;
348 try std.testing.expectEqual(Status.unsat, try solver.solveWithAssumptions(&assumptions));
349 try std.testing.expectEqualSlices(Literal, &.{Literal.positive(a)}, solver.lastUnsatCore());
350 var complete = (try solver.lastProofArtifact(std.testing.allocator)).?;
351 defer complete.deinit();
352 try std.testing.expectEqualSlices(Literal, solver.lastUnsatCore(), complete.assumptions.items);
353 try std.testing.expectEqual(complete.steps.items.len, solver.lastSolveStats().proof_steps);
354 }
355
356 fn checkSolveAllocationFailureEvidence(allocator: std.mem.Allocator) !void {
357 var solver = Solver.init(allocator);
358 defer solver.deinit();
359 const pigeons: u32 = 4;
360 const holes: u32 = 3;
361 for (0..pigeons * holes) |_| _ = try solver.addVariable();
362 for (0..pigeons) |pigeon| {
363 var placement: [holes]Literal = undefined;
364 for (&placement, 0..) |*literal, hole| {
365 literal.* = Literal.positive(@intCast(pigeon * holes + hole));
366 }
367 try solver.addClause(&placement);
368 }
369 for (0..holes) |hole| {
370 for (0..pigeons) |first| {
371 for (first + 1..pigeons) |second| {
372 try solver.addClause(&.{
373 Literal.negative(@intCast(first * holes + hole)),
374 Literal.negative(@intCast(second * holes + hole)),
375 });
376 }
377 }
378 }
379 const assumptions = [_]Literal{
380 Literal.positive(0),
381 Literal.negative(1),
382 };
383 const status = solver.solveWithAssumptions(&assumptions) catch |failure| {
384 try std.testing.expectEqual(@as(usize, 0), solver.lastProofTrace().len);
385 try std.testing.expectEqual(@as(usize, 0), solver.lastUnsatCore().len);
386 try std.testing.expectEqual(@as(usize, 0), solver.lastSolveStats().proof_steps);
387 try std.testing.expect((try solver.lastProofArtifact(std.testing.allocator)) == null);
388 return failure;
389 };
390 try std.testing.expectEqual(Status.unsat, status);
391 try std.testing.expectEqual(
392 solver.lastProofTrace().len,
393 solver.lastSolveStats().proof_steps,
394 );
395 }
396
397 test "sat solver clears proof evidence on every allocation failure" {
398 try std.testing.checkAllAllocationFailures(
399 std.testing.allocator,
400 checkSolveAllocationFailureEvidence,
401 .{},
402 );
403 }
404
405 test "sat solver reports unknown when core certification exhausts budget" {
406 var solver = Solver.init(std.testing.allocator);
407 defer solver.deinit();
408 const a = try solver.addVariable();
409 const b = try solver.addVariable();
410 const c = try solver.addVariable();
411 const d = try solver.addVariable();
412 const e = try solver.addVariable();
413 try solver.addClause(&.{ Literal.negative(a), Literal.positive(b), Literal.positive(c) });
414 try solver.addClause(&.{ Literal.negative(a), Literal.positive(b), Literal.negative(c) });
415 try solver.addClause(&.{ Literal.negative(a), Literal.negative(b), Literal.positive(c) });
416 try solver.addClause(&.{ Literal.negative(a), Literal.negative(b), Literal.negative(c) });
417 const assumptions = [_]Literal{ Literal.positive(d), Literal.positive(a), Literal.positive(e) };
418 solver.conflict_budget = 9;
419 try std.testing.expectEqual(Status.unknown, try solver.solveWithAssumptions(&assumptions));
420 try std.testing.expectEqual(@as(usize, 0), solver.lastUnsatCore().len);
421 solver.conflict_budget = null;
422 try std.testing.expectEqual(Status.unsat, try solver.solveWithAssumptions(&assumptions));
423 try std.testing.expectEqualSlices(Literal, &.{Literal.positive(a)}, solver.lastUnsatCore());
424 }
425
426 test "sat solver keeps assumptions through learned conflicts" {
427 var solver = Solver.init(std.testing.allocator);
428 defer solver.deinit();
429 const a = try solver.addVariable();
430 const b = try solver.addVariable();
431 const c = try solver.addVariable();
432 try solver.addClause(&.{ Literal.negative(a), Literal.positive(b), Literal.positive(c) });
433 try solver.addClause(&.{ Literal.negative(a), Literal.positive(b), Literal.negative(c) });
434 try solver.addClause(&.{ Literal.negative(a), Literal.negative(b), Literal.positive(c) });
435 try solver.addClause(&.{ Literal.negative(a), Literal.negative(b), Literal.negative(c) });
436 try std.testing.expectEqual(
437 Status.unsat,
438 try solver.solveWithAssumptions(&.{Literal.positive(a)}),
439 );
440 try std.testing.expectEqualSlices(Literal, &.{Literal.positive(a)}, solver.lastUnsatCore());
441 try std.testing.expectEqual(Status.sat, try solver.solve());
442 try std.testing.expectEqual(false, solver.value(a).?);
443 }
444
445 test "sat solver supports nested assumption frames" {
446 var solver = Solver.init(std.testing.allocator);
447 defer solver.deinit();
448 const a = try solver.addVariable();
449 const b = try solver.addVariable();
450 try solver.addClause(&.{ Literal.positive(a), Literal.positive(b) });
451 try solver.pushAssumptionFrame();
452 try solver.assume(Literal.negative(a));
453 try std.testing.expectEqual(@as(usize, 1), solver.frameDepth());
454 try std.testing.expectEqualSlices(Literal, &.{Literal.negative(a)}, solver.activeAssumptions());
455 try std.testing.expectEqual(Status.sat, try solver.solveWithActiveAssumptions());
456 try std.testing.expectEqual(true, solver.value(b).?);
457 try solver.pushAssumptionFrame();
458 try solver.assume(Literal.negative(b));
459 try std.testing.expectEqual(@as(usize, 2), solver.frameDepth());
460 try std.testing.expectEqual(Status.unsat, try solver.solveWithActiveAssumptions());
461 try std.testing.expectEqualSlices(
462 Literal,
463 &.{ Literal.negative(a), Literal.negative(b) },
464 solver.lastUnsatCore(),
465 );
466 solver.popAssumptionFrame();
467 try std.testing.expectEqual(@as(usize, 1), solver.frameDepth());
468 try std.testing.expectEqualSlices(Literal, &.{Literal.negative(a)}, solver.activeAssumptions());
469 try std.testing.expectEqual(@as(usize, 0), solver.lastUnsatCore().len);
470 try std.testing.expectEqual(Status.sat, try solver.solveWithActiveAssumptions());
471 try std.testing.expectEqual(true, solver.value(b).?);
472 solver.popAssumptionFrame();
473 try std.testing.expectEqual(@as(usize, 0), solver.frameDepth());
474 try std.testing.expectEqual(@as(usize, 0), solver.activeAssumptions().len);
475 try std.testing.expectEqual(Status.sat, try solver.solveWithActiveAssumptions());
476 }
477
478 test "conflict budget returns unknown instead of spinning" {
479 var solver = Solver.init(std.testing.allocator);
480 defer solver.deinit();
481 var variables: [8]u32 = undefined;
482 for (&variables) |*variable| variable.* = try solver.addVariable();
483 for (0..variables.len - 1) |index| {
484 const a = variables[index];
485 const b = variables[index + 1];
486 try solver.addClause(&.{ Literal.positive(a), Literal.positive(b) });
487 try solver.addClause(&.{ Literal.positive(a), Literal.negative(b) });
488 try solver.addClause(&.{ Literal.negative(a), Literal.positive(b) });
489 try solver.addClause(&.{ Literal.negative(a), Literal.negative(b) });
490 }
491 solver.conflict_budget = 1;
492 try std.testing.expectEqual(Status.unknown, try solver.solve());
493 try std.testing.expect(solver.lastSolveStats().conflicts >= 1);
494 solver.conflict_budget = null;
495 try std.testing.expectEqual(Status.unsat, try solver.solve());
496 }
497
498 test "conflict budget preserves genuine results within budget" {
499 var solver = Solver.init(std.testing.allocator);
500 defer solver.deinit();
501 const a = try solver.addVariable();
502 const b = try solver.addVariable();
503 try solver.addClause(&.{ Literal.positive(a), Literal.positive(b) });
504 solver.conflict_budget = 64;
505 try std.testing.expectEqual(Status.sat, try solver.solve());
506 }