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
Designed and built a production Promise library from algebraic first principles -- map derives from flatMap, reduce from fold, operators match Haskell's typeclass precedence hierarchy
fluent-html
Zero-dependency, type-safe HTML builder for TypeScript with compile-time Tailwind CSS and HTMX safety
Designed a mixin architecture using TypeScript declaration merging + prototype assignment that splits a 1,100-line Tag class into focused modules with zero API changes
Redis Server (Zig)
From-scratch Redis-compatible server in Zig with RESP parsing, RDB persistence, and master-replica replication
Implemented a complete Redis-compatible server from scratch in 915 lines of zero-dependency Zig with RESP protocol parser, key-value store with TTL, and RDB binary format codec