Committing to the bit: Relational programming with semiring arrays and SAT solving
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866909809671929856 |
|---|---|
| author | Volkov, Dmitri Yang, Yafei Shan, Chung-chieh |
| author_facet | Volkov, Dmitri Yang, Yafei Shan, Chung-chieh |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_22614 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Committing to the bit: Relational programming with semiring arrays and SAT solving Volkov, Dmitri Yang, Yafei Shan, Chung-chieh Programming Languages D.3.1; F.3.2; D.3.2; D.3.3 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. |
| title | Committing to the bit: Relational programming with semiring arrays and SAT solving |
| topic | Programming Languages D.3.1; F.3.2; D.3.2; D.3.3 |
| url | https://arxiv.org/abs/2509.22614 |