lib/smt/src/sat/types.zig
daab053ee43316e1809a84551d573ddd1e5bf3d2
1 //! The values a caller hands to the solver and reads back from it: literals, answers, truth values
2 //! that may be unset, counts of a solve's work, and the restart schedule.
3 //!
4 //! A caller writes clauses as literals over variables numbered from 0, reads one of three answers
5 //! after each solve, and reads the value of each variable after a satisfiable answer. Clause files
6 //! in the common text format number variables from 1 and write a negated variable as a negative
7 //! number (DIMACS), so a caller reading or writing them converts each literal.
8 //!
9 //! The solver keeps one list per literal, so a literal has to map to a small number that can index
10 //! an array. A literal packs its variable and its sign into one 32-bit number (`Literal.raw`):
11 //! twice the variable index, plus one for a negated literal. That number indexes the solver's
12 //! per-literal lists directly, and negating a literal flips its lowest bit. `Literal.fromDimacs`
13 //! and `Literal.toDimacs` convert between that number and the signed numbers of the text format. A
14 //! truth value has a third state, unset (`BoolValue.unset`), for an unassigned variable.
15 /// The answer of one solve. A caller switches on it to decide whether to read a satisfying
16 /// assignment, an unsat core and a proof, or neither.
17 pub const Status = enum {
18 /// Some assignment makes every clause and every assumption of the solve true. `Solver.value`
19 /// and `Solver.literalValue` read that assignment until the next solve.
20 sat,
21 /// No assignment makes every clause and every assumption of the solve true. The solver then
22 /// holds a proof trace that ends in the empty clause, and after a solve under assumptions an
23 /// unsat core.
24 unsat,
25 /// The solve ran out of its conflict limit (`Solver.conflict_budget`) before it reached an
26 /// answer, or while core minimization certified a smaller core. After the second case the core
27 /// is empty, but the proof trace still holds a refutation under every assumption of the solve.
28 unknown,
29 };
30
31 /// A truth value that may also be unset. A caller switches on the value `Solver.literalValue`
32 /// returns to read a literal in a satisfying assignment.
33 pub const BoolValue = enum {
34 /// The variable is unassigned, or the literal names a variable at or above the solver's
35 /// variable count.
36 unset,
37 /// The literal or variable is false.
38 false,
39 /// The literal or variable is true.
40 true,
41
42 /// Returns `.true` for true and `.false` for false. The solver and the proof checker record an
43 /// assigned value through it.
44 pub fn fromBool(value: bool) BoolValue {
45 return if (value) .true else .false;
46 }
47
48 /// Returns the opposite value, and `.unset` for `.unset`. The solver and the proof checker read
49 /// a negated literal's value from its variable's value through it.
50 pub fn invert(self: BoolValue) BoolValue {
51 return switch (self) {
52 .unset => .unset,
53 .false => .true,
54 .true => .false,
55 };
56 }
57 };
58
59 /// Counts of the work one solve did. A caller reads them from `Solver.lastSolveStats` to report how
60 /// much work a solve took. The solver sets every count to zero when a solve starts. The counts
61 /// cover the main search: the extra solves of core minimization change only `proof_steps`, which
62 /// takes the certified trace's length.
63 pub const SolveStats = struct {
64 /// Decisions the search made, each giving an unassigned variable a value.
65 decisions: usize = 0,
66 /// Decisions that gave the variable the value it last held, in this solve or an earlier one,
67 /// counted within `decisions`.
68 phase_saved_decisions: usize = 0,
69 /// Literals the search assigned because every other literal of a clause was false. Unit clauses
70 /// of the formula and assumptions sit outside the count.
71 propagations: usize = 0,
72 /// Times the main search found a clause with every literal false. `Solver.conflict_budget`
73 /// limits this count.
74 conflicts: usize = 0,
75 /// Clauses the search learned from conflicts in this solve.
76 learned_clauses: usize = 0,
77 /// Learned clauses the solver removed to stay within `Solver.max_learned_clauses`, removals at
78 /// the start of the solve included.
79 evicted_clauses: usize = 0,
80 /// Steps in the proof trace at the end of the solve: one per learned clause, plus the final
81 /// empty clause after an unsatisfiable answer. After core minimization certified a smaller
82 /// core, the count is the certifying solve's step count.
83 proof_steps: usize = 0,
84 /// Times the search went back to the first decision, on the restart schedule or to remove
85 /// learned clauses.
86 restarts: usize = 0,
87 /// The largest number of decisions in force at once during the solve.
88 max_decision_level: u32 = 0,
89 /// Conflicts found at decision level zero, counted within `conflicts`. Assumptions sit below
90 /// every decision, so a conflict among the assumptions counts here.
91 root_conflicts: usize = 0,
92 };
93
94 /// The restart schedule: the search goes back to the first decision after a conflict count that
95 /// starts at `first_conflict_interval` and multiplies by `growth` after each restart. A caller
96 /// passes one to `Solver.setRestartPolicy` to change the schedule, for example to restart after
97 /// every conflict. The default restarts after 128 conflicts, then after 256 more, then 512,
98 /// doubling each time. The solver keeps its learned clauses across a restart. The count starts over
99 /// at each solve, and a restart happens only while a decision is in force.
100 pub const RestartPolicy = struct {
101 /// Conflicts before the first restart of each solve, 128 by default. Zero turns restarts off.
102 first_conflict_interval: usize = 128,
103 /// The factor the interval grows by after each restart, 2 by default. A factor of 0 or 1 keeps
104 /// the interval fixed, and the interval stops growing at the largest `usize`.
105 growth: usize = 2,
106
107 /// Returns a policy that turns restarts off: an interval of 0 and a growth of 1. A caller that
108 /// turns restarts off passes it to `Solver.setRestartPolicy`.
109 pub fn disabled() RestartPolicy {
110 return .{ .first_conflict_interval = 0, .growth = 1 };
111 }
112 };
113
114 /// A variable or its negation, packed into one 32-bit number. A caller builds every clause and
115 /// every assumption from literals. Variables are numbered from 0 in the order `Solver.addVariable`
116 /// returns them.
117 pub const Literal = struct {
118 /// The packed number: twice the variable index, plus one for a negated literal. Two literals
119 /// are equal when their `raw` values are equal, and callers compare literals that way.
120 raw: u32,
121
122 /// Returns the literal of variable `variable_index`, unnegated when `polarity` is true and
123 /// negated when it is false. Code that picks the sign at run time calls it. An index of
124 /// 2147483648 or more overflows the packed number, which panics in safe builds.
125 pub fn init(variable_index: u32, polarity: bool) Literal {
126 return .{ .raw = variable_index * 2 + if (polarity) @as(u32, 0) else @as(u32, 1) };
127 }
128
129 /// Returns the unnegated literal of variable `variable_index`. A caller writes a clause whose
130 /// signs it knows in its source.
131 pub fn positive(variable_index: u32) Literal {
132 return init(variable_index, true);
133 }
134
135 /// Returns the negated literal of variable `variable_index`. A caller writes a clause whose
136 /// signs it knows in its source.
137 pub fn negative(variable_index: u32) Literal {
138 return init(variable_index, false);
139 }
140
141 /// Returns the variable index of the literal. A caller finds which variable a literal names,
142 /// for example to check it against a variable count.
143 pub fn variable(self: Literal) u32 {
144 return self.raw >> 1;
145 }
146
147 /// Returns true for an unnegated literal. A caller reads a literal's sign to evaluate it under
148 /// an assignment.
149 pub fn isPositive(self: Literal) bool {
150 return self.raw & 1 == 0;
151 }
152
153 /// Returns the literal of the same variable with the opposite sign. An encoder calls it to
154 /// state the negation of a condition.
155 pub fn negated(self: Literal) Literal {
156 return .{ .raw = self.raw ^ 1 };
157 }
158
159 /// Returns the packed number as a `usize`. The solver indexes its per-literal lists of watching
160 /// clauses by it, two entries per variable.
161 pub fn index(self: Literal) usize {
162 return @intCast(self.raw);
163 }
164
165 /// Returns the literal a DIMACS number stands for: variable `|value| - 1`, negated when `value`
166 /// is negative. The DIMACS and proof readers call it on each number of a clause. The call
167 /// returns `error.InvalidDimacsLiteral` for 0, the number that ends a clause in that format.
168 /// The value -2147483648 makes it panic, because its negation does not fit in 32 bits.
169 pub fn fromDimacs(value: i32) !Literal {
170 if (value == 0) return error.InvalidDimacsLiteral;
171 const magnitude: u32 = @intCast(if (value < 0) -value else value);
172 return init(magnitude - 1, value > 0);
173 }
174
175 /// Returns the DIMACS number of the literal: the variable index plus one, negative for a
176 /// negated literal. The DIMACS and proof writers call it on each literal they print. Variable
177 /// index 2147483647 makes it panic, because its number does not fit in `i32`.
178 pub fn toDimacs(self: Literal) i32 {
179 const one_based: i32 = @intCast(self.variable() + 1);
180 return if (self.isPositive()) one_based else -one_based;
181 }
182 };