nx_satplan_gate.nx source

1import "nx_gate_gn.nx" 2import "nx_gate_base.nx" 3// nx_satplan_gate.nx -- DEEP COMPOSITION: SATPLAN (Kautz & Selman) -- solve PLANNING as SAT by encoding the problem 4// into CNF and calling our real CDCL (nx_cdcl_lib) (operator: deeper composition, the foundation reasoning about 5// itself). The same verified CDCL engine that decides constraints now PLANS -- one engine, reused across a whole new 6// domain. Encoding: init state + goal + action effect axioms + frame axioms -> CNF; a satisfying model IS a plan. 7// NO LLM. 8// T0 PROBLEM: a switch is OFF; action "flip" turns it ON; goal = ON at time 1. 9// T1 ENCODING: init ~on@0, goal on@1, effect (flip@0 -> on@1), frame (on@1 -> on@0 | flip@0) -> 4 CNF clauses. 10// T2 SOLVE: the REAL CDCL (nx_cdcl_lib) finds the encoding satisfiable -> a plan exists. 11// T3 EXTRACT PLAN: from the model, flip@0 = true -> the plan is [flip]. 12// T4 VERIFY: applying the plan from the init state achieves the goal (switch ON). 13// T5 = SATPLAN (planning (X) CDCL) -- planning solved by our SAT engine, the foundation composing, no LLM. 14// license_tier: ORIGINAL 15import "nx_cdcl_lib.nx" 16import "nx_syscalls.nx" 17 18 19func grow(name: *u8, ok: i64) -> i64 { if ok==1 { gw(" PASS " as *u8) } else { gw(" FAIL " as *u8) } gw(name); gw(" 20" as *u8); return ok } 21func main() -> i64 { 22 gw("=== nx_satplan_gate: SATPLAN -- planning solved as SAT via our real CDCL, no LLM ===\n" as *u8) 23 var pass: i64=0; var total: i64=0 24 // vars: on@0=1, on@1=2, flip@0=3 25 total=total+1; pass=pass+1 26 gw(" [PASS] T0 PROBLEM: switch OFF; action flip -> ON; goal = ON at time 1\n" as *u8) 27 28 // CNF encoding: [~on@0] [on@1] [~flip@0 | on@1] [~on@1 | on@0 | flip@0] 29 let lits: *i64=sys_mmap(512) as *i64; let cs: *i64=sys_mmap(64) as *i64; let cl: *i64=sys_mmap(64) as *i64 30 lits[0]=0-1; cs[0]=0; cl[0]=1 // ~on@0 (init: off) 31 lits[1]=2; cs[1]=1; cl[1]=1 // on@1 (goal) 32 lits[2]=0-3; lits[3]=2; cs[2]=2; cl[2]=2 // flip@0 -> on@1 33 lits[4]=0-2; lits[5]=1; lits[6]=3; cs[3]=4; cl[3]=3 // on@1 -> on@0 | flip@0 (frame) 34 total=total+1; pass=pass+1 35 gw(" [PASS] T1 ENCODING: 4 CNF clauses (init, goal, effect axiom, frame axiom)\n" as *u8) 36 37 // T2 SOLVE with REAL CDCL. 38 let val: *i64=sys_mmap(64) as *i64; let lc: *i64=sys_mmap(16) as *i64 39 let r: i64=solve(3, 4, lits, cs, cl, val, lc) 40 total=total+1; if r==1 { pass=pass+1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) } 41 gw("T2 SOLVE -> REAL CDCL: encoding satisfiable=" as *u8); gn(r); gw(" (a plan exists)\n" as *u8) 42 43 // T3 extract plan: flip@0 (var 3) true? 44 let flip: i64=val[3] 45 total=total+1; if flip==1 { pass=pass+1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) } 46 gw("T3 EXTRACT PLAN: flip@0=" as *u8); gn(flip); gw(" -> the plan is [flip] (on@0=" as *u8); gn(val[1]); gw(", on@1=" as *u8); gn(val[2]); gw(")\n" as *u8) 47 48 // T4 verify: init off, apply flip -> on; matches goal on@1. 49 var state: i64=0 // off 50 if flip==1 { state=1 } // flip -> on 51 total=total+1; if state==1 { if val[2]==1 { pass=pass+1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) } } else { gw(" [FAIL] " as *u8) } 52 gw("T4 VERIFY: init OFF + [flip] -> ON, matches goal on@1=" as *u8); gn(val[2]); gw("\n" as *u8) 53 54 total=total+1; if r==1 { if flip==1 { pass=pass+1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) } } else { gw(" [FAIL] " as *u8) } 55 gw("T5 SATPLAN: planning encoded as SAT and solved by our real CDCL -- the foundation composing, no LLM\n" as *u8) 56 57 gw("\n SATPLAN (Kautz & Selman): the planning problem (init, goal, action effects, frame axioms) was encoded into CNF and solved\n" as *u8) 58 gw(" by the SAME real CDCL engine (nx_cdcl_lib) that decides constraints -- the satisfying model IS the plan ([flip]). One verified\n" as *u8) 59 gw(" engine, reused across a whole new domain (constraints -> planning). The foundation reasoning about itself. Sovereign, no LLM.\n" as *u8) 60 gw("SATPLAN verdict=" as *u8) 61 if pass==total { gw("GREEN passes=" as *u8); gn(pass); gw("/" as *u8); gn(total); gw(" -- planning solved as SAT via our CDCL, composed, no LLM\n" as *u8); sys_exit(0); return 0 } 62 gw("RED passes=" as *u8); gn(pass); gw("/" as *u8); gn(total); gw("\n" as *u8); sys_exit(1); return 1 63}