lib/smt/src/sat/proof.zig
daab053ee43316e1809a84551d573ddd1e5bf3d2
1 const std = @import("std");
2 const types = @import("types.zig");
3
4 pub const BoolValue = types.BoolValue;
5 pub const Literal = types.Literal;
6
7 /// One step of a proof trace: a clause that has to follow from the starting clauses, the
8 /// assumptions and the earlier steps by unit propagation. A caller walks the steps of the last
9 /// solve through `Solver.lastProofTrace`, and code that writes or checks a proof walks the steps of
10 /// a `ProofArtifact`. The last step of a complete refutation is the empty clause.
11 pub const ProofStep = struct {
12 /// The literals of the step's clause, and an empty slice for the empty clause. In the solver's
13 /// trace the solver owns them, and they stay valid until the next change to the solver. In a
14 /// `ProofArtifact` the artifact owns its own copy.
15 literals: []Literal,
16 };
17
18 /// One starting clause of a `ProofArtifact`: a clause the checker takes as given. Code that writes
19 /// a proof or checks its scope walks the starting clauses.
20 pub const ProofClause = struct {
21 /// The literals of the clause, owned by the artifact and freed by `ProofArtifact.deinit`.
22 literals: []Literal,
23 };
24
25 /// The clauses, assumptions and steps behind one unsatisfiable answer, copied out of the solver and
26 /// owned by the caller. A caller keeps it as the evidence of an unsatisfiable answer after the
27 /// solver moves on, checks it with `valid`, and writes it out as text. A proof reader and tests
28 /// also build artifacts by hand with `init` and the append functions. The artifact allocates every
29 /// copy with the allocator given to `init` and frees them in `deinit`. The artifact shares no
30 /// memory with the solver, so it stays usable after the solver changes or is freed.
31 pub const ProofArtifact = struct {
32 allocator: std.mem.Allocator,
33 /// The number of variables the artifact covers. Every literal has to name a variable below it,
34 /// or `valid` returns false. `Solver.lastProofArtifact` sets it to the solver's variable count.
35 variable_count: usize,
36 /// The starting clauses, in order. From `Solver.lastProofArtifact` they are every clause the
37 /// solver held when the solve began, learned clauses it kept included, then an empty clause
38 /// when the caller had added one. `appendClause` adds one at the end.
39 clauses: std.ArrayList(ProofClause) = .empty,
40 /// The literals assumed true for the refutation. From `Solver.lastProofArtifact` they are the
41 /// solve's assumptions, cut down to the smaller set that core minimization certified when it
42 /// finished. They can be more than `Solver.lastUnsatCore` reports, because the artifact keeps
43 /// every assumption of the solve unless core minimization certified a smaller set. When the
44 /// clauses were refuted before the search began, as by two opposite unit clauses, the core is
45 /// empty and the artifact keeps every assumption. When a conflict comes while the solver
46 /// assigns the first of two or more assumptions, the core holds that one assumption, core
47 /// minimization leaves it as it is, and the artifact keeps every assumption. When a conflict
48 /// limit runs out during the certifying solve of core minimization, the core is empty and the
49 /// artifact keeps every assumption.
50 assumptions: std.ArrayList(Literal) = .empty,
51 /// The proof steps in order, each checked against the starting clauses, the assumptions and the
52 /// steps before it. `appendStep` adds one at the end.
53 steps: std.ArrayList(ProofStep) = .empty,
54
55 /// Returns an empty artifact over `variable_count` variables that allocates with `allocator`.
56 /// Code that builds an artifact by hand, such as a proof reader, starts from it. The call
57 /// allocates nothing.
58 pub fn init(allocator: std.mem.Allocator, variable_count: usize) ProofArtifact {
59 return .{ .allocator = allocator, .variable_count = variable_count };
60 }
61
62 /// Frees every clause and step copy and the three lists with the artifact's allocator. The
63 /// owner of an artifact calls it once, when it is done with the evidence. The artifact is
64 /// undefined afterward.
65 pub fn deinit(self: *ProofArtifact) void {
66 for (self.clauses.items) |clause| {
67 self.allocator.free(clause.literals);
68 }
69 self.clauses.deinit(self.allocator);
70 self.assumptions.deinit(self.allocator);
71 for (self.steps.items) |step| {
72 self.allocator.free(step.literals);
73 }
74 self.steps.deinit(self.allocator);
75 self.* = undefined;
76 }
77
78 /// Copies `literals` and adds the copy as the last starting clause. A proof reader calls it
79 /// once per starting clause, in file order. The caller keeps `literals`. The call returns
80 /// `error.OutOfMemory` when the copy or the list growth fails, and then the artifact is as it
81 /// was.
82 pub fn appendClause(self: *ProofArtifact, literals: []const Literal) !void {
83 const owned = try self.allocator.dupe(Literal, literals);
84 errdefer self.allocator.free(owned);
85 try self.clauses.append(self.allocator, .{ .literals = owned });
86 }
87
88 /// Appends `literals` to the assumption list. A proof reader calls it for the assumption
89 /// record, and `Solver.lastProofArtifact` calls it once with the solve's assumptions. Calls
90 /// accumulate: each one appends after what earlier calls added. The call returns
91 /// `error.OutOfMemory` when the list growth fails.
92 pub fn appendAssumptions(self: *ProofArtifact, literals: []const Literal) !void {
93 try self.assumptions.appendSlice(self.allocator, literals);
94 }
95
96 /// Copies `literals` and adds the copy as the last proof step. A proof reader calls it once per
97 /// step, in file order, and `Solver.lastProofArtifact` calls it once per step of the trace. The
98 /// caller keeps `literals`. The call returns `error.OutOfMemory` when the copy or the list
99 /// growth fails, and then the artifact is as it was.
100 pub fn appendStep(self: *ProofArtifact, literals: []const Literal) !void {
101 const owned = try self.allocator.dupe(Literal, literals);
102 errdefer self.allocator.free(owned);
103 try self.steps.append(self.allocator, .{ .literals = owned });
104 }
105
106 /// Returns true when every step follows by unit propagation from the starting clauses, the
107 /// assumptions and the steps before it, and the last step is the empty clause. A caller runs it
108 /// to confirm an unsatisfiable answer independently of the solver that gave it. To check one
109 /// step, the call assumes the assumptions true and the step's literals false, then propagates
110 /// unit clauses over the starting clauses and the earlier steps until a clause becomes false
111 /// (Reverse Unit Propagation). The step passes when a clause becomes false, and also when the
112 /// assumptions clash with the negated step. The call returns false when the step list is empty,
113 /// or when any literal names a variable at or above `variable_count`. A step may use only the
114 /// steps before it, so a step that only a later step supports fails. Each step repeats the
115 /// propagation over every starting clause and earlier step until a pass leaves every value as
116 /// it was. The call allocates one truth value per variable with the artifact's allocator for
117 /// its own duration, and `error.OutOfMemory` is its only error.
118 pub fn valid(self: *const ProofArtifact) !bool {
119 if (self.steps.items.len == 0) return false;
120 if (!proofClausesUseKnownVariables(
121 ProofClause,
122 self.variable_count,
123 self.clauses.items,
124 )) return false;
125 if (!proofLiteralsUseKnownVariables(
126 self.variable_count,
127 self.assumptions.items,
128 )) return false;
129 for (self.steps.items) |step| {
130 if (!proofLiteralsUseKnownVariables(self.variable_count, step.literals)) return false;
131 }
132 const assignment = try self.allocator.alloc(BoolValue, self.variable_count);
133 defer self.allocator.free(assignment);
134 for (self.steps.items, 0..) |step, index| {
135 if (!rupCheckKnownVariablesWithClauses(
136 assignment,
137 ProofClause,
138 self.clauses.items,
139 self.assumptions.items,
140 self.steps.items,
141 step.literals,
142 index,
143 )) return false;
144 }
145 return self.steps.items[self.steps.items.len - 1].literals.len == 0;
146 }
147 };
148
149 pub fn rupCheckKnownVariablesWithClauses(
150 assignment: []BoolValue,
151 comptime ClauseType: type,
152 clauses: []const ClauseType,
153 assumptions: []const Literal,
154 steps: []const ProofStep,
155 literals: []const Literal,
156 proof_step_limit: usize,
157 ) bool {
158 std.debug.assert(proof_step_limit <= steps.len);
159 if (proofSeedConflict(assignment, assumptions, literals)) return true;
160 return proofPropagatesConflictWithClauses(
161 ClauseType,
162 clauses,
163 steps,
164 assignment,
165 proof_step_limit,
166 );
167 }
168
169 pub const ReasonTrace = struct {
170 trail: []const Literal,
171 reasons: []const ?usize,
172 conflict: usize,
173 };
174
175 /// Checks that a learned clause follows by unit propagation, replaying the clause that forced each
176 /// assigned literal, in the order the literals were assigned, and then the clause that became
177 /// false. The solver calls it on each clause it learns, before keeping the clause, and a false
178 /// result ends the solve with `error.InvalidProofTrace`. The call first assumes `assumptions` true
179 /// and the clause's `literals` false, and returns true at once when those clash. It returns true
180 /// when a replayed clause becomes false, and false otherwise. `trace.trail` lists the assigned
181 /// literals in assignment order, `trace.reasons` gives for each variable the index of the clause
182 /// that forced it, or `null` for a decision or an assumption, and `trace.conflict` is the index of
183 /// the clause that became false. Every clause the replay uses has to be one of `clauses`, which
184 /// holds the clauses the proof may rely on. The call asserts that each clause index it follows lies
185 /// inside `clauses`. `trace.reasons` and `assignment` hold one entry per variable, and the call
186 /// overwrites `assignment`.
187 pub fn rupCheckKnownVariablesWithReasons(
188 assignment: []BoolValue,
189 comptime ClauseType: type,
190 clauses: []const ClauseType,
191 assumptions: []const Literal,
192 literals: []const Literal,
193 trace: ReasonTrace,
194 ) bool {
195 std.debug.assert(trace.reasons.len == assignment.len);
196 std.debug.assert(trace.conflict < clauses.len);
197 if (proofSeedConflict(assignment, assumptions, literals)) return true;
198 for (trace.trail) |literal| {
199 const reason = trace.reasons[literal.variable()] orelse continue;
200 std.debug.assert(reason < clauses.len);
201 if (proofApplyClause(assignment, clauses[reason].literals) == .conflict) return true;
202 }
203 return proofApplyClause(assignment, clauses[trace.conflict].literals) == .conflict;
204 }
205
206 fn proofSeedConflict(
207 assignment: []BoolValue,
208 assumptions: []const Literal,
209 literals: []const Literal,
210 ) bool {
211 @memset(assignment, .unset);
212 for (assumptions) |assumption| {
213 if (!proofAssign(assignment, assumption)) return true;
214 }
215 for (literals) |literal| {
216 if (!proofAssign(assignment, literal.negated())) return true;
217 }
218 return false;
219 }
220
221 fn proofPropagatesConflictWithClauses(
222 comptime ClauseType: type,
223 clauses: []const ClauseType,
224 steps: []const ProofStep,
225 assignment: []BoolValue,
226 proof_step_limit: usize,
227 ) bool {
228 const limit = proof_step_limit;
229 while (true) {
230 var changed = false;
231 for (clauses) |clause| {
232 switch (proofApplyClause(assignment, clause.literals)) {
233 .consistent => {},
234 .assigned => changed = true,
235 .conflict => return true,
236 }
237 }
238 for (steps[0..limit]) |step| {
239 switch (proofApplyClause(assignment, step.literals)) {
240 .consistent => {},
241 .assigned => changed = true,
242 .conflict => return true,
243 }
244 }
245 if (!changed) return false;
246 }
247 }
248
249 const ProofClauseResult = enum {
250 consistent,
251 assigned,
252 conflict,
253 };
254
255 fn proofApplyClause(assignment: []BoolValue, literals: []const Literal) ProofClauseResult {
256 var unset_literal: ?Literal = null;
257 for (literals) |literal| {
258 switch (proofLiteralValue(assignment, literal)) {
259 .true => return .consistent,
260 .false => {},
261 .unset => {
262 if (unset_literal != null) return .consistent;
263 unset_literal = literal;
264 },
265 }
266 }
267 const unit = unset_literal orelse return .conflict;
268 return if (proofAssign(assignment, unit)) .assigned else .conflict;
269 }
270
271 fn proofAssign(assignment: []BoolValue, literal: Literal) bool {
272 const variable_index = literal.variable();
273 if (variable_index >= assignment.len) return false;
274 const current = proofLiteralValue(assignment, literal);
275 if (current == .true) return true;
276 if (current == .false) return false;
277 assignment[variable_index] = BoolValue.fromBool(literal.isPositive());
278 return true;
279 }
280
281 fn proofLiteralValue(assignment: []const BoolValue, literal: Literal) BoolValue {
282 if (literal.variable() >= assignment.len) return .unset;
283 const assigned = assignment[literal.variable()];
284 return if (literal.isPositive()) assigned else assigned.invert();
285 }
286
287 fn proofClausesUseKnownVariables(
288 comptime ClauseType: type,
289 variable_count: usize,
290 clauses: []const ClauseType,
291 ) bool {
292 for (clauses) |clause| {
293 if (!proofLiteralsUseKnownVariables(variable_count, clause.literals)) return false;
294 }
295 return true;
296 }
297
298 fn proofLiteralsUseKnownVariables(variable_count: usize, literals: []const Literal) bool {
299 for (literals) |literal| {
300 if (literal.variable() >= variable_count) return false;
301 }
302 return true;
303 }
304
305 test "proof reason replay checks inference and rejects an incomplete trail" {
306 var first = [_]Literal{ Literal.negative(0), Literal.positive(1) };
307 var second = [_]Literal{ Literal.negative(1), Literal.positive(2) };
308 var conflict = [_]Literal{Literal.negative(2)};
309 const clauses = [_]ProofClause{
310 .{ .literals = &first },
311 .{ .literals = &second },
312 .{ .literals = &conflict },
313 };
314 const trail = [_]Literal{
315 Literal.positive(0), Literal.positive(1), Literal.positive(2),
316 };
317 const reasons = [_]?usize{ null, 0, 1 };
318 var assignment: [3]BoolValue = undefined;
319 const learned = [_]Literal{Literal.negative(0)};
320 const trace: ReasonTrace = .{ .trail = &trail, .reasons = &reasons, .conflict = 2 };
321 try std.testing.expect(rupCheckKnownVariablesWithReasons(
322 &assignment,
323 ProofClause,
324 &clauses,
325 &.{},
326 &learned,
327 trace,
328 ));
329 try std.testing.expect(rupCheckKnownVariablesWithClauses(
330 &assignment,
331 ProofClause,
332 &clauses,
333 &.{},
334 &.{},
335 &learned,
336 0,
337 ));
338 try std.testing.expect(!rupCheckKnownVariablesWithReasons(
339 &assignment,
340 ProofClause,
341 &clauses,
342 &.{},
343 &.{Literal.positive(0)},
344 trace,
345 ));
346 try std.testing.expect(!rupCheckKnownVariablesWithReasons(
347 &assignment,
348 ProofClause,
349 &clauses,
350 &.{},
351 &learned,
352 .{ .trail = trail[2..], .reasons = &reasons, .conflict = 2 },
353 ));
354 try std.testing.expect(rupCheckKnownVariablesWithReasons(
355 &assignment,
356 ProofClause,
357 &clauses,
358 &.{Literal.positive(0)},
359 &.{Literal.positive(0)},
360 trace,
361 ));
362 }
363
364 test "proof propagation reaches a fixed point within the exact step prefix" {
365 var first = [_]Literal{ Literal.negative(0), Literal.positive(1) };
366 var second = [_]Literal{ Literal.negative(1), Literal.positive(2) };
367 var seed = [_]Literal{Literal.positive(0)};
368 var contradiction = [_]Literal{Literal.negative(2)};
369 const clauses = [_]ProofClause{
370 .{ .literals = &seed },
371 .{ .literals = &contradiction },
372 };
373 const steps = [_]ProofStep{
374 .{ .literals = &first },
375 .{ .literals = &second },
376 .{ .literals = &.{} },
377 };
378 var assignment: [3]BoolValue = undefined;
379 try std.testing.expect(rupCheckKnownVariablesWithClauses(
380 &assignment,
381 ProofClause,
382 &clauses,
383 &.{},
384 &steps,
385 &.{},
386 2,
387 ));
388 try std.testing.expect(!rupCheckKnownVariablesWithClauses(
389 &assignment,
390 ProofClause,
391 clauses[0..1],
392 &.{},
393 &steps,
394 &.{},
395 2,
396 ));
397 try std.testing.expect(rupCheckKnownVariablesWithClauses(
398 &assignment,
399 ProofClause,
400 clauses[0..1],
401 &.{},
402 &steps,
403 &.{},
404 3,
405 ));
406 }
407
408 test "proof artifact rejects a first step visible only to itself" {
409 var artifact = ProofArtifact.init(std.testing.allocator, 1);
410 defer artifact.deinit();
411 try artifact.appendStep(&.{Literal.positive(0)});
412 try artifact.appendStep(&.{Literal.negative(0)});
413 try artifact.appendStep(&.{});
414 try std.testing.expectEqual(false, try artifact.valid());
415 }
416
417 test "proof artifact rejects literals outside its variable scope" {
418 var artifact = ProofArtifact.init(std.testing.allocator, 1);
419 defer artifact.deinit();
420 try artifact.appendClause(&.{Literal.positive(1)});
421 try artifact.appendStep(&.{});
422 try std.testing.expectEqual(false, try artifact.valid());
423 }
424
425 test "proof artifact assumptions are part of its exact scope" {
426 var scoped = ProofArtifact.init(std.testing.allocator, 1);
427 defer scoped.deinit();
428 try scoped.appendClause(&.{Literal.positive(0)});
429 try scoped.appendAssumptions(&.{Literal.negative(0)});
430 try scoped.appendStep(&.{});
431 try std.testing.expect(try scoped.valid());
432
433 var erased = ProofArtifact.init(std.testing.allocator, 1);
434 defer erased.deinit();
435 try erased.appendClause(&.{Literal.positive(0)});
436 try erased.appendStep(&.{});
437 try std.testing.expectEqual(false, try erased.valid());
438 }