nx_pure_lit.nx source
↩ module page · 116 lines · 4282 B
1// nx_pure_lit.nx -- pure-literal elimination preprocessing.
2//
3// A predicate symbol is "pure" if it appears with only one polarity
4// across the entire clause set. Clauses containing a pure literal
5// can be vacuously satisfied -- there's no clause that could ever
6// contradict them, so removing them preserves UNSAT-equivalence.
7//
8// Standard SAT-solver preprocessing (Davis-Putnam 1960 lineage)
9// extended to first-order: the predicate symbol is the unit of
10// purity, not the literal. A clause containing ANY pure-positive
11// literal of pred p (or ANY pure-negative literal of pred p) is
12// dropped. Iterating to fixpoint can cascade: dropping clauses may
13// make other predicates become pure.
14//
15// API: nx_pure_lit_eliminate(input, n_input, out, *out_n) -- one
16// pass. Caller iterates to fixpoint if desired.
17//
18// Bits-up nx_int.
19
20// nx_safety_envelope:
21// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
22// sil_target: SIL1
23// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
24// verdict: NOT_YET_EVALUATED
25
26import "nx_syscalls.nx"
27import "nx_runtime.nx"
28import "nx_tier.nx"
29import "nx_result.nx"
30import "nx_unify.nx"
31import "nx_resolution.nx"
32
33const NX_PURE_MAX_PREDS: nx_int = 1024
34
35// Per-predicate bitfield: bit 0 set iff seen with POS polarity;
36// bit 1 set iff seen with NEG polarity.
37const NX_PURE_POS_BIT: nx_int = 1
38const NX_PURE_NEG_BIT: nx_int = 2
39
40// Walk clauses, for each predicate symbol record which polarities
41// it appears with. Variable atoms are skipped (they don't have a
42// predicate symbol -- defensive, not expected in well-formed CNF).
43func nx_pure_collect(clauses: *Clause, n: nx_int, polarities: *nx_int) {
44 var i: nx_int = 0
45 while i < n {
46 let c: *Clause = ((clauses as nx_int) + (i * NX_CLAUSE_BYTES)) as *Clause
47 var j: nx_int = 0
48 while j < c.n_lits {
49 let l: *Literal = nx_clause_lit_at(c, j)
50 if l.atom.kind != NX_TERM_VAR {
51 let s: nx_int = l.atom.sym
52 if s >= 0 {
53 if s < NX_PURE_MAX_PREDS {
54 if l.sign == NX_LIT_POS {
55 polarities[s] = polarities[s] | NX_PURE_POS_BIT
56 }
57 if l.sign == NX_LIT_NEG {
58 polarities[s] = polarities[s] | NX_PURE_NEG_BIT
59 }
60 }
61 }
62 }
63 j = j + 1
64 }
65 i = i + 1
66 }
67}
68
69// Returns 1 iff clause c contains any literal whose predicate symbol
70// is pure (only one polarity in the whole input).
71func nx_pure_clause_has_pure_lit(c: *Clause, polarities: *nx_int) -> nx_int {
72 var j: nx_int = 0
73 while j < c.n_lits {
74 let l: *Literal = nx_clause_lit_at(c, j)
75 if l.atom.kind != NX_TERM_VAR {
76 let s: nx_int = l.atom.sym
77 if s >= 0 {
78 if s < NX_PURE_MAX_PREDS {
79 let pol: nx_int = polarities[s]
80 // Pure POS: only POS_BIT set, no NEG_BIT, AND this
81 // literal is POS.
82 if l.sign == NX_LIT_POS {
83 if pol == NX_PURE_POS_BIT { return 1 }
84 }
85 if l.sign == NX_LIT_NEG {
86 if pol == NX_PURE_NEG_BIT { return 1 }
87 }
88 }
89 }
90 }
91 j = j + 1
92 }
93 return 0
94}
95
96// One-pass elimination. Returns number of clauses kept.
97func nx_pure_lit_eliminate(input: *Clause, n_input: nx_int,
98 out: *Clause, out_n: *nx_int) -> nx_int {
99 let polarities: *nx_int = (sys_mmap((NX_PURE_MAX_PREDS * 8) as i64)) as *nx_int
100 nx_pure_collect(input, n_input, polarities)
101
102 var n_kept: nx_int = 0
103 var i: nx_int = 0
104 while i < n_input {
105 let c: *Clause = ((input as nx_int) + (i * NX_CLAUSE_BYTES)) as *Clause
106 if nx_pure_clause_has_pure_lit(c, polarities) == 0 {
107 let dest: *Clause = ((out as nx_int) + (n_kept * NX_CLAUSE_BYTES)) as *Clause
108 dest.n_lits = c.n_lits
109 dest.lits = c.lits
110 n_kept = n_kept + 1
111 }
112 i = i + 1
113 }
114 out_n[0] = n_kept
115 return n_kept
116}