nx_fmb.nx source
↩ module page · 309 lines · 11413 B
1// nx_fmb.nx -- Finite Model Building.
2//
3// Per Vampire Trophy Cabinet (https://github.com/vprover/vampire/wiki/Trophy-Cabinet):
4// "Our success [in the FNT division] is supported heavily by our
5// implementation of finite model building."
6//
7// FMB is the explicitly-named technique Vampire credits with its
8// Find-Non-Theorems wins. Shipping it closes the BLOCKED_ON_FMB axis
9// from the substrate's honest CASC verdict.
10//
11// Algorithm (MACE-style, simplified):
12// For each domain size N = 1, 2, 3, ...:
13// 1. Ground every clause over a domain of N constants
14// {d_1, d_2, ..., d_N}. Every variable in every clause is
15// instantiated as each domain element in turn (one variable ->
16// N copies of the clause; two variables -> N^2 copies; etc.).
17// 2. Convert the ground clause set into a propositional SAT problem.
18// 3. Run the SAT solver. If SAT, the original problem has a
19// finite model of size N -- emit MODEL_FOUND verdict.
20// If UNSAT, try N+1.
21// 4. If no model found within max_size, return UNKNOWN.
22//
23// Verdicts:
24// NX_FMB_MODEL_FOUND -- problem has a finite model (so the negated
25// conjecture is satisfiable; original was NOT
26// a theorem) -- CounterModel found
27// NX_FMB_NO_MODEL -- search ran up to max_size without finding
28// NX_FMB_ERROR -- bad input / capacity exceeded
29//
30// This is the basic CounterSatisfiable detector. Real Vampire FMB
31// uses CSP-style constraints + sort inference + sym break; this MVP
32// uses naive grounding + DPLL on the SAT side. Sufficient for
33// FNT-easy problems.
34//
35// Bits-up nx_int; uses existing nx_sat_solver DPLL backend.
36
37// nx_safety_envelope:
38// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
39// sil_target: SIL1
40// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
41// verdict: NOT_YET_EVALUATED
42
43import "nx_syscalls.nx"
44import "nx_runtime.nx"
45import "nx_tier.nx"
46import "nx_result.nx"
47import "nx_unify.nx"
48import "nx_resolution.nx"
49import "nx_sat_solver.nx"
50const NX_MAGIC_4096: i64 = 4096
51
52const NX_FMB_MODEL_FOUND: nx_int = 1
53const NX_FMB_NO_MODEL: nx_int = 2
54const NX_FMB_ERROR: nx_int = 3
55
56// Domain constants get sym_ids in this range -- distinct from user
57// (1000+), Tseitin (800k+), Skolem (900k+), Answer (700k+),
58// AVATAR-sp (600k+).
59const NX_FMB_DOMAIN_BASE_SYM: nx_int = 500000
60
61// Max literals per ground atom (for SAT propositional mapping).
62const NX_FMB_MAX_VARS_PER_CLAUSE: nx_int = 8
63
64// Recursive var-collector for a term (defined first for forward-ref
65// avoidance). Appends new var ids to out_vars if not already
66// present; returns updated count.
67func nx_fmb_term_vars(t: *Term, out: *nx_int, n_out: nx_int) -> nx_int {
68 if t.kind == NX_TERM_VAR {
69 var i: nx_int = 0
70 while i < n_out {
71 if out[i] == t.sym { return n_out }
72 i = i + 1
73 }
74 if n_out < NX_FMB_MAX_VARS_PER_CLAUSE {
75 out[n_out] = t.sym
76 return n_out + 1
77 }
78 return n_out
79 }
80 if t.kind == NX_TERM_CONST { return n_out }
81 var k: nx_int = 0
82 var n: nx_int = n_out
83 while k < t.n_args {
84 n = nx_fmb_term_vars(nx_term_arg(t, k), out, n)
85 k = k + 1
86 }
87 return n
88}
89
90// Collect distinct variable ids in a clause (across all literals).
91// Returns count.
92func nx_fmb_collect_vars(c: *Clause, out_vars: *nx_int) -> nx_int {
93 var n: nx_int = 0
94 var i: nx_int = 0
95 while i < c.n_lits {
96 let lit: *Literal = nx_clause_lit_at(c, i)
97 n = nx_fmb_term_vars(lit.atom, out_vars, n)
98 i = i + 1
99 }
100 return n
101}
102
103// Substitute every occurrence of `var_id` in t with the domain element
104// at index `dom_elem` (which corresponds to sym_id NX_FMB_DOMAIN_BASE_SYM+dom_elem).
105func nx_fmb_subst_term(t: *Term, var_id: nx_int, dom_elem: nx_int) -> *Term {
106 if t.kind == NX_TERM_VAR {
107 if t.sym == var_id { return nx_term_const(NX_FMB_DOMAIN_BASE_SYM + dom_elem) }
108 return t
109 }
110 if t.kind == NX_TERM_CONST { return t }
111 if t.n_args == 0 { return t }
112 let new_args: *Term = (sys_mmap((t.n_args * NX_TERM_BYTES) as i64)) as *Term
113 var changed: nx_int = 0
114 var i: nx_int = 0
115 while i < t.n_args {
116 let child: *Term = nx_term_arg(t, i)
117 let new_child: *Term = nx_fmb_subst_term(child, var_id, dom_elem)
118 let dest: *Term = ((new_args as nx_int) + (i * NX_TERM_BYTES)) as *Term
119 dest.kind = new_child.kind
120 dest.sym = new_child.sym
121 dest.n_args = new_child.n_args
122 dest.args = new_child.args
123 if (new_child as nx_int) != (child as nx_int) { changed = 1 }
124 i = i + 1
125 }
126 if changed == 1 { return nx_term_app(t.sym, t.n_args, new_args) }
127 return t
128}
129
130// Substitute in a clause (in-place rebuild).
131func nx_fmb_subst_clause(c: *Clause, var_id: nx_int, dom_elem: nx_int) -> *Clause {
132 let out: *Clause = nx_clause_new()
133 var i: nx_int = 0
134 while i < c.n_lits {
135 let li: *Literal = nx_clause_lit_at(c, i)
136 let new_atom: *Term = nx_fmb_subst_term(li.atom, var_id, dom_elem)
137 let new_lit: *Literal = nx_lit_make(li.sign, new_atom)
138 let _r: *NxResult = nx_clause_add(out, new_lit)
139 i = i + 1
140 }
141 return out
142}
143
144// Ground a clause over the entire domain of size N. Returns the count
145// of ground instances emitted (= N^k where k is the # of distinct vars).
146// out_clauses is caller-allocated.
147func nx_fmb_ground_clause(c: *Clause, domain_size: nx_int,
148 out_clauses: *Clause, out_n: *nx_int, cap: nx_int) -> nx_int {
149 let vars: *nx_int = (sys_mmap((NX_FMB_MAX_VARS_PER_CLAUSE * 8) as i64)) as *nx_int
150 let n_vars: nx_int = nx_fmb_collect_vars(c, vars)
151
152 if n_vars == 0 {
153 // Ground clause -- copy as-is.
154 if out_n[0] >= cap { return 0 - 1 }
155 let dest: *Clause = ((out_clauses as nx_int) + (out_n[0] * NX_CLAUSE_BYTES)) as *Clause
156 dest.n_lits = c.n_lits
157 dest.lits = c.lits
158 out_n[0] = out_n[0] + 1
159 return 1
160 }
161
162 // n_vars variables, domain_size choices each. Iterate odometer-style.
163 let assign: *nx_int = (sys_mmap((NX_FMB_MAX_VARS_PER_CLAUSE * 8) as i64)) as *nx_int
164 var i: nx_int = 0
165 while i < n_vars { assign[i] = 0; i = i + 1 }
166
167 var emitted: nx_int = 0
168 var done: nx_int = 0
169 while done == 0 {
170 // Apply current assignment to clause.
171 var cur: *Clause = c
172 var v: nx_int = 0
173 while v < n_vars {
174 cur = nx_fmb_subst_clause(cur, vars[v], assign[v])
175 v = v + 1
176 }
177 if out_n[0] >= cap { return 0 - 1 }
178 let dest: *Clause = ((out_clauses as nx_int) + (out_n[0] * NX_CLAUSE_BYTES)) as *Clause
179 dest.n_lits = cur.n_lits
180 dest.lits = cur.lits
181 out_n[0] = out_n[0] + 1
182 emitted = emitted + 1
183
184 // Advance the odometer.
185 var k: nx_int = 0
186 var carry: nx_int = 1
187 while k < n_vars {
188 if carry == 1 {
189 assign[k] = assign[k] + 1
190 if assign[k] >= domain_size {
191 assign[k] = 0
192 carry = 1
193 } else {
194 carry = 0
195 }
196 }
197 k = k + 1
198 }
199 if carry == 1 { done = 1 }
200 }
201 return emitted
202}
203
204// Map a ground atom (no variables, but with domain constants + possibly
205// nested function applications) to a fresh propositional SAT variable
206// id. Two structurally equal atoms get the same id. Uses a flat
207// table for the mapping; bounded by NX_FMB_MAX_PROP_ATOMS.
208const NX_FMB_MAX_PROP_ATOMS: nx_int = 4096
209
210struct FmbPropMap {
211 atoms: *Term, // [NX_FMB_MAX_PROP_ATOMS] -- known ground atoms
212 n: nx_int,
213}
214const NX_FMB_PROP_MAP_BYTES: nx_int = 16
215
216func nx_fmb_prop_map_new() -> *FmbPropMap {
217 let m: *FmbPropMap = (sys_mmap(NX_FMB_PROP_MAP_BYTES as i64)) as *FmbPropMap
218 m.atoms = (sys_mmap((NX_FMB_MAX_PROP_ATOMS * NX_TERM_BYTES) as i64)) as *Term
219 m.n = 0
220 return m
221}
222
223// Returns the SAT-side variable id (1-indexed) for `atom`. Allocates a
224// new id if the atom hasn't been seen. Returns -1 on capacity overflow.
225func nx_fmb_prop_id(m: *FmbPropMap, atom: *Term) -> nx_int {
226 var i: nx_int = 0
227 while i < m.n {
228 let existing: *Term = ((m.atoms as nx_int) + (i * NX_TERM_BYTES)) as *Term
229 if nx_term_eq(existing, atom) == 1 { return i + 1 }
230 i = i + 1
231 }
232 if m.n >= NX_FMB_MAX_PROP_ATOMS { return 0 - 1 }
233 let dest: *Term = ((m.atoms as nx_int) + (m.n * NX_TERM_BYTES)) as *Term
234 dest.kind = atom.kind
235 dest.sym = atom.sym
236 dest.n_args = atom.n_args
237 dest.args = atom.args
238 m.n = m.n + 1
239 return m.n
240}
241
242// Try to find a finite model of the given clause set at the specified
243// domain size. Returns NX_FMB_MODEL_FOUND or NX_FMB_NO_MODEL.
244func nx_fmb_try_size(clauses: *Clause, n_clauses: nx_int, size: nx_int) -> nx_int {
245 let cap: nx_int = NX_MAGIC_4096
246 let ground: *Clause = (sys_mmap((cap * NX_CLAUSE_BYTES) as i64)) as *Clause
247 let n_ground: *nx_int = sys_mmap(8) as *nx_int
248 n_ground[0] = 0
249
250 var i: nx_int = 0
251 while i < n_clauses {
252 let c: *Clause = ((clauses as nx_int) + (i * NX_CLAUSE_BYTES)) as *Clause
253 let rc: nx_int = nx_fmb_ground_clause(c, size, ground, n_ground, cap)
254 if rc < 0 { return NX_FMB_ERROR }
255 i = i + 1
256 }
257
258 // Convert ground clauses to a SAT problem via prop map.
259 let m: *FmbPropMap = nx_fmb_prop_map_new()
260 let sat_f: *SatFormula = nx_sat_alloc(NX_FMB_MAX_PROP_ATOMS)
261 let sat_lits: *nx_int = (sys_mmap((NX_CLAUSE_MAX_LITS * 8) as i64)) as *nx_int
262
263 var g: nx_int = 0
264 while g < n_ground[0] {
265 let gc: *Clause = ((ground as nx_int) + (g * NX_CLAUSE_BYTES)) as *Clause
266 var nl: nx_int = 0
267 var k: nx_int = 0
268 while k < gc.n_lits {
269 let lk: *Literal = nx_clause_lit_at(gc, k)
270 let pid: nx_int = nx_fmb_prop_id(m, lk.atom)
271 if pid < 0 { return NX_FMB_ERROR }
272 if lk.sign == NX_LIT_POS { sat_lits[nl] = pid }
273 if lk.sign != NX_LIT_POS { sat_lits[nl] = 0 - pid }
274 nl = nl + 1
275 k = k + 1
276 }
277 let _add: nx_int = nx_sat_add_clause(sat_f, sat_lits, nl)
278 g = g + 1
279 }
280
281 let v: nx_int = nx_sat_solve(sat_f)
282 if v == NX_SAT_SAT { return NX_FMB_MODEL_FOUND }
283 return NX_FMB_NO_MODEL
284}
285
286// Search domains 1..max_size; return verdict + the size that worked.
287// Writes the model size to *found_size_out (or 0 if no model found).
288func nx_fmb_search(clauses: *Clause, n_clauses: nx_int,
289 max_size: nx_int, found_size_out: *nx_int) -> nx_int {
290 found_size_out[0] = 0
291 var size: nx_int = 1
292 while size <= max_size {
293 let v: nx_int = nx_fmb_try_size(clauses, n_clauses, size)
294 if v == NX_FMB_MODEL_FOUND {
295 found_size_out[0] = size
296 return NX_FMB_MODEL_FOUND
297 }
298 if v == NX_FMB_ERROR { return NX_FMB_ERROR }
299 size = size + 1
300 }
301 return NX_FMB_NO_MODEL
302}
303
304func nx_fmb_verdict_name(v: nx_int) -> *u8 {
305 if v == NX_FMB_MODEL_FOUND { return "MODEL_FOUND" as *u8 }
306 if v == NX_FMB_NO_MODEL { return "NO_MODEL" as *u8 }
307 if v == NX_FMB_ERROR { return "ERROR" as *u8 }
308 return "?" as *u8
309}