Committing to the bit: Relational programming with semiring arrays and SAT solving
Programming Languages
2025-09-29 v1
Abstract
We propose semiringKanren, a relational programming language where each relation expression denotes a semiring array. We formalize a type system that restricts the arrays to finite size. We then define a semantics that is parameterized by the semiring that the arrays draw their elements from. We compile semiringKanren types to bitstring representations. For the Boolean semiring, this compilation enables us to use an SAT solver to run semiringKanren programs efficiently. We compare the performance of semiringKanren and faster miniKanren for solving Sudoku puzzles. Our experiment shows that semiringKanren can be a more efficient variant of miniKanren.
Keywords
Cite
@article{arxiv.2509.22614,
title = {Committing to the bit: Relational programming with semiring arrays and SAT solving},
author = {Dmitri Volkov and Yafei Yang and Chung-chieh Shan},
journal= {arXiv preprint arXiv:2509.22614},
year = {2025}
}
Comments
12 pages, for associated repo see https://github.com/sporkl/semiringkanren