code wiki / _hdl_build / nx_cdcl_lib.nx
nx_cdcl_lib.nx
buildroot/runtime/_hdl_build/nx_cdcl_lib.nx
about
nx_cdcl_lib.nx -- the REAL CDCL SAT solver as a SHARED LIBRARY (no main): var_of/lit_true/lit_false/solve, extracted
verbatim from the verified nx_cdcl_sat_gate so BOTH the gate AND the neurosymbolic dispatch loop call the SAME proven
code (DRY, rule 15). 1-UIP clause learning + non-chronological backjump + VSIDS. Integer, deterministic, NO LLM.
license_tier: ORIGINAL
dependencies 1 imports · 4 importers
imports: nx_syscalls.nx
imported by: nx_neurosym_complete_gate.nxnx_neurosym_full_gate.nxnx_neurosym_loop_gate.nxnx_satplan_gate.nx
structs
| none |
consts
| 6 | const K_MAGIC_2048: i64 = 2048 |
functions
| 8 | func var_of(lit: i64) -> i64 { if lit<0 { return 0-lit } return lit } |
| 9 | func lit_true(lit: i64, val: *i64) -> i64 { let v: i64=var_of(lit); if val[v]==0 { return 0 } if lit>0 { if val[v]==1 { return 1 } return 0 } if val[v]==(0-1) { return 1 } return 0 } |
| 10 | func lit_false(lit: i64, val: *i64) -> i64 { let v: i64=var_of(lit); if val[v]==0 { return 0 } if lit>0 { if val[v]==(0-1) { return 1 } return 0 } if val[v]==1 { return 1 } return 0 } |
| 13 | func solve(NV: i64, nc0: i64, lits: *i64, cstart: *i64, clen: *i64, val: *i64, lc_out: *i64) -> i64 |