Systems & Production Software
SAT Solver
Boolean satisfiability framework reducing NP-complete problems to SAT via a generic Expression<T> free algebra
Overview
A Boolean satisfiability (SAT) solver framework in Swift that reduces combinatorial problems -- N-Queens and Minimum Dominating Set -- into SAT via a generic Expression<T> intermediate representation, then compiles to DIMACS CNF format for CryptoMiniSat. The core insight is treating Boolean expressions as a free Boolean algebra: an indirect enum with a functor instance (map) that enables type-safe variable substitution while keeping the tree structure inspectable and transformable.
Key concepts
Free Boolean Algebra
Expression<T> is algebraically a free Boolean algebra -- it generates all Boolean expressions from generators (variables of type T) without imposing equations beyond structural laws. The 'free' part means you can interpret it however you want: into DIMACS strings, or evaluated, simplified, or pretty-printed. Same pattern as free monads being ASTs.
Code highlights
public indirect enum Expression<T> {
case variable(T)
case and([Expression])
case or([Expression])
case negate(Expression)
}Highlights
- — Designed Expression<T> as a generic, functor-equipped recursive data type -- the free Boolean algebra pattern later reused in renderbox-engine's FilterNode AST
- — Implemented two NP-complete problem reductions to SAT (N-Queens and Minimum Dominating Set) with mathematical rigor
- — Functor-based coordinate system decoupling -- generate constraints in natural spaces, then map to linear DIMACS indices
- — End-to-end solver pipeline from graph parsing through constraint generation, CNF compilation, external solver integration, and solution verification
Related projects
PromiseKit
Production Promise library built from algebraic first principles, shipped to ~50K DAU across multiple iOS apps
View →fluent-html
Zero-dependency, type-safe HTML builder for TypeScript with compile-time Tailwind CSS and HTMX safety
View →Everyframe
Composable type-safe TypeScript DSL that compiles to FFmpeg, ONNX Runtime, and OpenCV
View →