Encoding Numeric Computations and Infusing Heuristic Knowledge Using Integrity Constraints in stableKanren
Xiangyu Guo, Ajay Bansal
TL;DR
This work shows how stableKanren can encode numeric computations via integrity constraints (CaVE) to support combinatorial search tasks within a relational programming framework. It argues for a balanced approach between symbolic and numeric representations by using a constraint store, and demonstrates arithmetic relations and a SEND+MORE=MONEY case study to illustrate heuristic-guided search. The main contributions include multiple heuristic techniques—variables reordering, smaller per-digit constraints, critical emitters, and an external oracle verifier—that substantially accelerate solving, sometimes by orders of magnitude. The findings underscore the practical impact of declarative problem solving with built-in constraints and point to future work on integrated heuristics, CDNL-like strategies, and CLP-style optimizations for NP-hard problems.
Abstract
This paper presents examples of using integrity constraints in stableKanren to encode numeric computations for problem solving. Then, we use one of the examples to introduce multiple ways to infuse heuristic knowledge and reduce solving time. stableKanren is an extension of miniKanren that supports normal logic programs under stable model semantics. stableKanren further supports numeric computation by constructing a constraint store for integrity constraints. There are three ways to extend a relational programming language with numeric computations: relational number representation, grounding numbers to symbols, and constraint store construction. We demonstrate that the numeric computations in stableKanren have a straightforward numerical representation compared to relational number representations. More importantly, stableKanren balances symbolic and numeric computation in relational programming by avoiding the grounding of all numbers to symbols. Lastly, it also has simpler syntax compared to other constraint store construction approaches. stableKanren supports combinatorial search problem solving under a declarative generate and test paradigm. Such a paradigm generates all possible combinations of solutions to the problem, then applies a set of constraints to prune out the unwanted solutions. We demonstrate that different approaches to writing programs or queries affect the solver's performance in the SEND+MORE=MONEY puzzle. The performance gradually improves as more heuristic knowledge is infused through the programs or queries. Additionally, we show how to use an external function to achieve a hybrid solution.