Committing to the bit: Relational programming with semiring arrays and SAT solving
summary
SemiringKanren implements relations as multi-dimensional semiring arrays evaluated with a bottom-up fixpoint strategy, compiles algebraic types to bitstring compilation and runs the Boolean-semiring case by reducing to SAT solving. The system is statically typed, compiles sums to boolean-tagged vectors, inlines recursive calls to a finite depth (allowing false negatives but not false positives), and shows Sudoku benchmarks where SAT-backed runs beat faster miniKanren on larger instances while naive dense arrays blow memory. Future work: polymorphism, recursive types, SMT integration.
AI-written summary · about
chapters (15)
- 0:00Semiring arrays and SAT intro
- 1:27Coin flip relation
- 2:51Adding weights with semirings
- 3:54Graph connectivity via transitive closure
- 5:24Relations compute multi-dimensional arrays
- 7:57Variables for multi-dimensional relations
- 9:01Low-level relations and combinators
- 11:11Recursion with fixpoint evaluation
- 13:17ADTs to bit strings
- 16:45Type-safe coercion code
- 18:10SAT from bit strings
- 19:14Sudoku benchmarking
- 19:57Future work on types
- 20:38Quantum computing analogies
- 21:27Q&A
related talks
24mAll for one and none forall: Compiling polymorphic relations without(…)
20mKanren Light
26mtypedKanren: Statically Typed Relational Programming with Exhaustive Matching in(…)
16mMulti-stage Relational Programming
14mOn Fair Relational Conjunction
47mLogic Programming à la Carte
14mRelational Synthesis for Pattern Matching
14mMicroKanren in J