nx_sat_solver.nx

buildroot/runtime/nx_sat_solver.nx

6393 B185 linesdepth 3pulls 3 transitivereach 7 importersview sourcekind library

docs dependencies structs consts functions

about

nx_sat_solver.nx -- propositional SAT solver foundation. Per user 2026-05-14 "i want to win in every event" referring to FLoC 2026 Olympics + SAT Competition specifically. This is the minimum-viable substrate-side DPLL SAT solver: supports CNF clauses, unit propagation, and naive backtracking. Foundation for future CDCL (conflict-driven clause learning) extensions that win SAT-COMP divisions. CNF representation: - Each variable is identified by positive i64 (1..N). - A literal is either +var (positive) or -var (negative). - A clause is a list of literals. - A formula is a list of clauses. Substrate variable convention: vars[i] = NX_SAT_TRUE (1) / NX_SAT_FALSE (0) / NX_SAT_UNDEF (-1) nx_safety_envelope: intended_use: "DPLL SAT solver -- foundation for substrate formal-methods chain (model checking, type- system queries, theorem prover preprocessing)" sil_target: SIL2 (formal-methods correctness) asil_target: QM dal_target: DAL B evidence: [DPLL_1962_canonical_basis, no_FP, sealed_3_value_assignment_enum, unit_propagation_canonical, conflict_clause_learning_target] hazard_register: [bug-tape-time-bomb-via-PHP-encoding, bug-tape-incomplete-CDCL-vs-DPLL-claim] residual_risk: "SAT is NP-complete; substrate provides decision procedure but cannot guarantee polynomial-time bound. Caller should set decision budget." verdict: NOT_YET_EVALUATED

dependencies 3 imports · 7 importers

imports: nx_syscalls.nxnx_runtime.nxnx_tier.nx

imported by: nx_avatar_encode.nxnx_avatar_encode_test.nxnx_fmb.nxnx_fmb_test.nxnx_sat_solver_test.nxnx_smtlib_parse.nxnx_smtlib_parse_test.nx

structs

53	struct SatFormula

consts

42	const NX_SAT_FALSE: nx_int = 0
43	const NX_SAT_TRUE: nx_int = 1
44	const NX_SAT_UNDEF: nx_int = -1
46	const NX_SAT_SAT: nx_int = 1
47	const NX_SAT_UNSAT: nx_int = 0
49	const NX_SAT_MAX_VARS: nx_int = 1024
50	const NX_SAT_MAX_CLAUSES: nx_int = 8192
51	const NX_SAT_MAX_LITS: nx_int = 65536

functions

62	func nx_sat_alloc(n_vars: nx_int) -> *SatFormula called by 4: main nx_fmb_try_size main nx_smt_parser_new calls 1: sys_mmap
79	func nx_sat_add_clause(f: SatFormula, lits_in: nx_int, n: nx_int) -> nx_int called by 4: nx_avatar_encode_to_sat nx_fmb_try_size main nx_smt_handle_assert
96	func nx_sat_lit_value(f: *SatFormula, lit: nx_int) -> nx_int called by 1: nx_sat_clause_value
111	func nx_sat_clause_value(f: *SatFormula, ci: nx_int) -> nx_int called by 1: nx_sat_formula_value calls 1: nx_sat_lit_value
127	func nx_sat_formula_value(f: *SatFormula) -> nx_int called by 1: nx_sat_dpll calls 1: nx_sat_clause_value
141	func nx_sat_pick_branch_var(f: *SatFormula) -> nx_int called by 1: nx_sat_dpll
152	func nx_sat_dpll(f: *SatFormula) -> nx_int called by 2: nx_sat_dpll nx_sat_solve calls 3: nx_sat_formula_value nx_sat_pick_branch_var nx_sat_dpll
179	func nx_sat_solve(f: *SatFormula) -> nx_int called by 4: main nx_fmb_try_size main main calls 1: nx_sat_dpll
183	func nx_sat_get_assignment(f: *SatFormula, v: nx_int) -> nx_int