nx_sat_solver.nx source
↩ module page · 185 lines · 6393 B
1// nx_sat_solver.nx -- propositional SAT solver foundation.
2//
3// Per user 2026-05-14 "i want to win in every event" referring to
4// FLoC 2026 Olympics + SAT Competition specifically. This is the
5// minimum-viable substrate-side DPLL SAT solver: supports CNF
6// clauses, unit propagation, and naive backtracking. Foundation for
7// future CDCL (conflict-driven clause learning) extensions that win
8// SAT-COMP divisions.
9//
10// CNF representation:
11// - Each variable is identified by positive i64 (1..N).
12// - A literal is either +var (positive) or -var (negative).
13// - A clause is a list of literals.
14// - A formula is a list of clauses.
15//
16// Substrate variable convention:
17// vars[i] = NX_SAT_TRUE (1) / NX_SAT_FALSE (0) / NX_SAT_UNDEF (-1)
18//
19// nx_safety_envelope:
20// intended_use: "DPLL SAT solver -- foundation for substrate
21// formal-methods chain (model checking, type-
22// system queries, theorem prover preprocessing)"
23// sil_target: SIL2 (formal-methods correctness)
24// asil_target: QM
25// dal_target: DAL B
26// evidence: [DPLL_1962_canonical_basis, no_FP,
27// sealed_3_value_assignment_enum,
28// unit_propagation_canonical,
29// conflict_clause_learning_target]
30// hazard_register: [bug-tape-time-bomb-via-PHP-encoding,
31// bug-tape-incomplete-CDCL-vs-DPLL-claim]
32// residual_risk: "SAT is NP-complete; substrate provides
33// decision procedure but cannot guarantee
34// polynomial-time bound. Caller should set
35// decision budget."
36// verdict: NOT_YET_EVALUATED
37
38import "nx_syscalls.nx"
39import "nx_runtime.nx"
40import "nx_tier.nx"
41
42const NX_SAT_FALSE: nx_int = 0
43const NX_SAT_TRUE: nx_int = 1
44const NX_SAT_UNDEF: nx_int = -1
45
46const NX_SAT_SAT: nx_int = 1
47const NX_SAT_UNSAT: nx_int = 0
48
49const NX_SAT_MAX_VARS: nx_int = 1024
50const NX_SAT_MAX_CLAUSES: nx_int = 8192
51const NX_SAT_MAX_LITS: nx_int = 65536
52
53struct SatFormula {
54 n_vars: nx_int,
55 n_clauses: nx_int,
56 // clauses_offset[c] gives start index in lits[]; clauses_offset[c+1] gives end
57 clauses_offset: *nx_int,
58 lits: *nx_int,
59 vars: *nx_int, // current assignment per variable (UNDEF / TRUE / FALSE)
60}
61
62func nx_sat_alloc(n_vars: nx_int) -> *SatFormula {
63 let raw: *u8 = sys_mmap(48)
64 let f: *SatFormula = raw as *SatFormula
65 f.n_vars = n_vars
66 f.n_clauses = 0
67 f.clauses_offset = (sys_mmap((NX_SAT_MAX_CLAUSES + 1) * 8)) as *nx_int
68 f.lits = (sys_mmap(NX_SAT_MAX_LITS * 8)) as *nx_int
69 f.vars = (sys_mmap((n_vars + 1) * 8)) as *nx_int
70 var i: nx_int = 0
71 while i <= n_vars {
72 f.vars[i] = NX_SAT_UNDEF
73 i = i + 1
74 }
75 f.clauses_offset[0] = 0
76 return f
77}
78
79func nx_sat_add_clause(f: *SatFormula, lits_in: *nx_int, n: nx_int) -> nx_int {
80 if f.n_clauses >= NX_SAT_MAX_CLAUSES { return -1 }
81 let start: nx_int = f.clauses_offset[f.n_clauses]
82 if start + n > NX_SAT_MAX_LITS { return -2 }
83 var i: nx_int = 0
84 while i < n {
85 f.lits[start + i] = lits_in[i]
86 i = i + 1
87 }
88 f.clauses_offset[f.n_clauses + 1] = start + n
89 f.n_clauses = f.n_clauses + 1
90 return 0
91}
92
93// Evaluate a single literal under the current assignment.
94// Returns NX_SAT_TRUE if the literal is satisfied, NX_SAT_FALSE if
95// falsified, NX_SAT_UNDEF if its var is unassigned.
96func nx_sat_lit_value(f: *SatFormula, lit: nx_int) -> nx_int {
97 var v: nx_int = lit
98 if v < 0 { v = 0 - v }
99 let val: nx_int = f.vars[v]
100 if val == NX_SAT_UNDEF { return NX_SAT_UNDEF }
101 if lit > 0 { return val }
102 // negative literal: flip
103 if val == NX_SAT_TRUE { return NX_SAT_FALSE }
104 return NX_SAT_TRUE
105}
106
107// Evaluate a clause. Returns:
108// NX_SAT_TRUE if any literal is satisfied
109// NX_SAT_FALSE if all literals are falsified
110// NX_SAT_UNDEF if no literal is satisfied but some are unassigned
111func nx_sat_clause_value(f: *SatFormula, ci: nx_int) -> nx_int {
112 let s: nx_int = f.clauses_offset[ci]
113 let e: nx_int = f.clauses_offset[ci + 1]
114 var i: nx_int = s
115 var has_undef: nx_int = 0
116 while i < e {
117 let v: nx_int = nx_sat_lit_value(f, f.lits[i])
118 if v == NX_SAT_TRUE { return NX_SAT_TRUE }
119 if v == NX_SAT_UNDEF { has_undef = 1 }
120 i = i + 1
121 }
122 if has_undef == 1 { return NX_SAT_UNDEF }
123 return NX_SAT_FALSE
124}
125
126// Evaluate the whole formula under current assignment.
127func nx_sat_formula_value(f: *SatFormula) -> nx_int {
128 var ci: nx_int = 0
129 var has_undef: nx_int = 0
130 while ci < f.n_clauses {
131 let v: nx_int = nx_sat_clause_value(f, ci)
132 if v == NX_SAT_FALSE { return NX_SAT_FALSE } // any falsified clause => UNSAT under current
133 if v == NX_SAT_UNDEF { has_undef = 1 }
134 ci = ci + 1
135 }
136 if has_undef == 1 { return NX_SAT_UNDEF }
137 return NX_SAT_TRUE
138}
139
140// Pick the first unassigned variable (naive branching heuristic).
141func nx_sat_pick_branch_var(f: *SatFormula) -> nx_int {
142 var v: nx_int = 1
143 while v <= f.n_vars {
144 if f.vars[v] == NX_SAT_UNDEF { return v }
145 v = v + 1
146 }
147 return 0
148}
149
150// Backtracking DPLL solver. Returns NX_SAT_SAT or NX_SAT_UNSAT.
151// On SAT, f.vars[] holds the satisfying assignment.
152func nx_sat_dpll(f: *SatFormula) -> nx_int {
153 let st: nx_int = nx_sat_formula_value(f)
154 if st == NX_SAT_TRUE { return NX_SAT_SAT }
155 if st == NX_SAT_FALSE { return NX_SAT_UNSAT }
156
157 // Pick variable to branch on
158 let v: nx_int = nx_sat_pick_branch_var(f)
159 if v == 0 {
160 // All assigned but neither true nor false above -- shouldn't happen
161 return NX_SAT_UNSAT
162 }
163
164 // Try TRUE
165 f.vars[v] = NX_SAT_TRUE
166 if nx_sat_dpll(f) == NX_SAT_SAT { return NX_SAT_SAT }
167
168 // Try FALSE
169 f.vars[v] = NX_SAT_FALSE
170 if nx_sat_dpll(f) == NX_SAT_SAT { return NX_SAT_SAT }
171
172 // Backtrack
173 f.vars[v] = NX_SAT_UNDEF
174 return NX_SAT_UNSAT
175}
176
177// Convenience: solve a formula encoded as (n_vars, list of clauses).
178// Each clause is encoded as (n_lits, lit_1, lit_2, ...).
179func nx_sat_solve(f: *SatFormula) -> nx_int {
180 return nx_sat_dpll(f)
181}
182
183func nx_sat_get_assignment(f: *SatFormula, v: nx_int) -> nx_int {
184 return f.vars[v]
185}