nx_sat_solver_test.nx source

1// nx_sat_solver_test.nx -- smoke for the SAT solver foundation. 2// Verifies a few well-known SAT / UNSAT instances. 3 4import "nx_syscalls.nx" 5import "nx_runtime.nx" 6import "nx_tier.nx" 7import "nx_sat_solver.nx" 8 9func main() -> nx_exit { 10 println("=== SAT solver foundation smoke ===" as *u8) 11 12 // Test 1: trivial SAT (a OR b) AND (a OR -b) -> SAT with a=TRUE 13 let f1: *SatFormula = nx_sat_alloc(2) 14 let c1a: *nx_int = (sys_mmap(16)) as *nx_int 15 c1a[0] = 1; c1a[1] = 2 // a OR b 16 let _: nx_int = nx_sat_add_clause(f1, c1a, 2) 17 let c1b: *nx_int = (sys_mmap(16)) as *nx_int 18 c1b[0] = 1; c1b[1] = -2 // a OR -b 19 let _a: nx_int = nx_sat_add_clause(f1, c1b, 2) 20 let r1: nx_int = nx_sat_solve(f1) 21 print("Test 1 (a OR b) AND (a OR -b): " as *u8) 22 if r1 == NX_SAT_SAT { println("SAT" as *u8) } 23 if r1 != NX_SAT_SAT { println("FAIL" as *u8); return 1 } 24 25 // Test 2: trivial UNSAT a AND -a 26 let f2: *SatFormula = nx_sat_alloc(1) 27 let c2a: *nx_int = (sys_mmap(8)) as *nx_int 28 c2a[0] = 1 29 let _b: nx_int = nx_sat_add_clause(f2, c2a, 1) 30 let c2b: *nx_int = (sys_mmap(8)) as *nx_int 31 c2b[0] = -1 32 let _c: nx_int = nx_sat_add_clause(f2, c2b, 1) 33 let r2: nx_int = nx_sat_solve(f2) 34 print("Test 2 (a) AND (-a): " as *u8) 35 if r2 == NX_SAT_UNSAT { println("UNSAT" as *u8) } 36 if r2 != NX_SAT_UNSAT { println("FAIL" as *u8); return 2 } 37 38 // Test 3: 3-SAT instance (a OR b OR c) AND (-a OR -b) AND (-a OR -c) AND (-b OR -c) 39 // = "exactly one of a,b,c true" -- SAT with several valid assignments 40 let f3: *SatFormula = nx_sat_alloc(3) 41 let c3a: *nx_int = (sys_mmap(24)) as *nx_int 42 c3a[0] = 1; c3a[1] = 2; c3a[2] = 3 43 let _d: nx_int = nx_sat_add_clause(f3, c3a, 3) 44 let c3b: *nx_int = (sys_mmap(16)) as *nx_int 45 c3b[0] = -1; c3b[1] = -2 46 let _e: nx_int = nx_sat_add_clause(f3, c3b, 2) 47 let c3c: *nx_int = (sys_mmap(16)) as *nx_int 48 c3c[0] = -1; c3c[1] = -3 49 let _f: nx_int = nx_sat_add_clause(f3, c3c, 2) 50 let c3d: *nx_int = (sys_mmap(16)) as *nx_int 51 c3d[0] = -2; c3d[1] = -3 52 let _g: nx_int = nx_sat_add_clause(f3, c3d, 2) 53 let r3: nx_int = nx_sat_solve(f3) 54 print("Test 3 exactly-one-of-3: " as *u8) 55 if r3 == NX_SAT_SAT { println("SAT" as *u8) } 56 if r3 != NX_SAT_SAT { println("FAIL" as *u8); return 3 } 57 58 println("=== All SAT smoke tests PASS ===" as *u8) 59 return 0 60}