Documentation
¶
Overview ¶
Package sat ships a CDCL SAT solver as a Wile extension.
The solver implements watched-literal unit propagation, 1-UIP conflict analysis with clause learning, VSIDS-style activity branching, Luby restarts, and activity-based clause-database cleanup. It targets MiniSat-class competence on instances up to roughly 10k variables and 100k clauses.
The Scheme front-end at (wile algebra sat) wraps these primitives with a Tseitin transform and exposes sat?, sat-cnf?, boolean-decide-sat?, and boolean-decide-equivalent?. See memory/2026-05-30-sat-solver-design.local.md.
Index ¶
Constants ¶
This section is empty.
Variables ¶
var AddToRegistry = Builder.AddToRegistry
AddToRegistry registers all sat primitives.
var Builder = registry.NewRegistryBuilder(addPrimitives)
Builder aggregates all sat registration functions.
var Extension = registry.NewDescribedExtension("sat", "CDCL SAT solver kernel backing (wile algebra sat). Accepts CNF as a flat vector of int literals with 0-terminated clauses; returns SAT/UNSAT plus a model on SAT, or 'unknown on conflict-budget exhaustion or ctx cancellation.", AddToRegistry)
Extension is the SAT solver FFI extension.
Functions ¶
func PrimSatCNFFlat ¶
func PrimSatCNFFlat(mc machine.CallContext) error
PrimSatCNFFlat implements (sat-cnf-flat? vec budget).
vec is a flat vector of exact integers in DIMACS CNF format (non-zero literals separated by 0 terminators). budget is either #f (unlimited) or an exact integer giving the maximum number of conflicts.
Returns #t on SAT, #f on UNSAT, or the symbol 'unknown on budget/context exhaustion.
func PrimSatCNFFlatModel ¶
func PrimSatCNFFlatModel(mc machine.CallContext) error
PrimSatCNFFlatModel implements (sat-cnf-flat-model).
Returns the model vector from the most recent sat-cnf-flat? call that returned #t, or #f if no model is available. The vector is indexed 1..N where N is the largest variable index seen; index 0 is unused (#f).
Source Files