nx_cdcl_lib.nx source

1// nx_cdcl_lib.nx -- the REAL CDCL SAT solver as a SHARED LIBRARY (no main): var_of/lit_true/lit_false/solve, extracted 2// verbatim from the verified nx_cdcl_sat_gate so BOTH the gate AND the neurosymbolic dispatch loop call the SAME proven 3// code (DRY, rule 15). 1-UIP clause learning + non-chronological backjump + VSIDS. Integer, deterministic, NO LLM. 4// license_tier: ORIGINAL 5import "nx_syscalls.nx" 6const K_MAGIC_2048: i64 = 2048 7 8func var_of(lit: i64) -> i64 { if lit<0 { return 0-lit } return lit } 9func 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 } 10func 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 } 11 12// CDCL. lits/cstart/clen hold clauses (capacity for learned). returns 1=SAT (model in val), 0=UNSAT. lc_out[0]=#learned. 13func solve(NV: i64, nc0: i64, lits: *i64, cstart: *i64, clen: *i64, val: *i64, lc_out: *i64) -> i64 { 14 let lvl: *i64=sys_mmap(256) as *i64; let ante: *i64=sys_mmap(256) as *i64; let seen: *i64=sys_mmap(256) as *i64; let act: *i64=sys_mmap(256) as *i64 15 let trail: *i64=sys_mmap(K_MAGIC_2048) as *i64; let learnt: *i64=sys_mmap(256) as *i64 16 var v: i64=0; while v<=NV { val[v]=0; lvl[v]=0; ante[v]=0-1; seen[v]=0; act[v]=0; v=v+1 } 17 var nt: i64=0; var dl: i64=0; var nc: i64=nc0; var nlearned: i64=0; var lits_top: i64=cstart[nc0-1]+clen[nc0-1] 18 while 1==1 { 19 var conflict: i64=0-1; var changed: i64=1 20 while changed==1 { 21 changed=0; var c: i64=0 22 while c<nc { 23 var sat: i64=0; var nun: i64=0; var ulit: i64=0; var k: i64=cstart[c]; let ke: i64=cstart[c]+clen[c] 24 while k<ke { let L: i64=lits[k]; if lit_true(L,val)==1 { sat=1; k=ke } else { if lit_false(L,val)==0 { nun=nun+1; ulit=L } k=k+1 } } 25 if sat==0 { if nun==0 { conflict=c; c=nc } else { if nun==1 { let vv: i64=var_of(ulit); if ulit>0 { val[vv]=1 } else { val[vv]=0-1 } lvl[vv]=dl; ante[vv]=c; trail[nt]=ulit; nt=nt+1; changed=1 } c=c+1 } } else { c=c+1 } 26 } 27 if conflict>=0 { changed=0 } 28 } 29 if conflict>=0 { 30 if dl==0 { lc_out[0]=nlearned; return 0 } 31 v=0; while v<=NV { seen[v]=0; v=v+1 } 32 var nl: i64=0; var counter: i64=0; var btlevel: i64=0; var p: i64=0; var pivot: i64=0; var cc: i64=conflict; var idx: i64=nt-1; var done: i64=0 33 while done==0 { 34 var k: i64=cstart[cc]; let ke: i64=cstart[cc]+clen[cc] 35 while k<ke { 36 let q: i64=lits[k]; let qv: i64=var_of(q) 37 if qv!=pivot { if seen[qv]==0 { if lvl[qv]>0 { seen[qv]=1; act[qv]=act[qv]+1 38 if lvl[qv]==dl { counter=counter+1 } else { learnt[nl]=q; nl=nl+1; if lvl[qv]>btlevel { btlevel=lvl[qv] } } } } } 39 k=k+1 40 } 41 while seen[var_of(trail[idx])]==0 { idx=idx-1 } 42 p=trail[idx]; idx=idx-1; pivot=var_of(p); seen[pivot]=0; counter=counter-1 43 if counter==0 { learnt[nl]=0-p; nl=nl+1; done=1 } else { cc=ante[pivot] } 44 } 45 cstart[nc]=lits_top; clen[nc]=nl; var j: i64=0; while j<nl { lits[lits_top+j]=learnt[j]; j=j+1 } lits_top=lits_top+nl 46 let lc: i64=nc; nc=nc+1; nlearned=nlearned+1 47 var bjdone: i64=0 48 while bjdone==0 { if nt==0 { bjdone=1 } else { let topv: i64=var_of(trail[nt-1]); if lvl[topv]>btlevel { val[topv]=0; lvl[topv]=0; ante[topv]=0-1; nt=nt-1 } else { bjdone=1 } } } 49 dl=btlevel 50 let uip: i64=learnt[nl-1]; let uv: i64=var_of(uip); if uip>0 { val[uv]=1 } else { val[uv]=0-1 } lvl[uv]=dl; ante[uv]=lc; trail[nt]=uip; nt=nt+1 51 } else { 52 var dvar: i64=0; var ba: i64=0-1; v=1; while v<=NV { if val[v]==0 { if act[v]>ba { ba=act[v]; dvar=v } } v=v+1 } 53 if dvar==0 { lc_out[0]=nlearned; return 1 } 54 dl=dl+1; val[dvar]=1; lvl[dvar]=dl; ante[dvar]=0-1; trail[nt]=dvar; nt=nt+1 55 } 56 } 57 lc_out[0]=nlearned; return 0 58}