arXivDaily arXiv每日学术速递 周一至周五更新
arXiv 2510.04049cs.PL
收藏

在stableKanren中利用完整性约束编码数值计算并注入启发式知识

Encoding Numeric Computations and Infusing Heuristic Knowledge Using Integrity Constraints in stableKanren

Xiangyu Guo, Ajay Bansal

AI总结:

本文介绍stableKanren(miniKanren的稳定模型语义扩展)通过完整性约束存储实现数值计算的方法,验证其在表示、符号-数值平衡、语法上的优势,并以SEND+MORE=MONEY谜题为例证明注入启发式知识可提升求解性能,还给出外部函数混合方案。

摘要:

本文展示了在stableKanren中利用完整性约束编码数值计算以求解问题的多个示例。随后,我们借助其中一个示例介绍了多种注入启发式知识、缩短求解时间的方法。stableKanren是miniKanren的扩展,支持稳定模型语义下的常规逻辑程序,它通过为完整性约束构建约束存储,进一步支持数值计算。\n为关系编程语言扩展数值计算能力有三种方式:关系数表示、将数实例化为符号,以及约束存储构建。我们证明,与关系数表示相比,stableKanren中的数值计算具备更直观的数值表示形式。更重要的是,stableKanren避免了将所有数都实例化为符号,从而在关系编程中实现了符号计算与数值计算的平衡。最后,与其他约束存储构建方法相比,它的语法也更简洁。\nstableKanren支持在声明式“生成-测试”范式下求解组合搜索问题,该范式会生成问题所有可能的解组合,再应用一组约束剪去不需要的解。我们在SEND+MORE=MONEY谜题中验证,编写程序或查询的不同方式会影响求解器性能,随着通过程序或查询注入的启发式知识增多,性能会逐步提升。此外,我们还展示了如何利用外部函数实现混合求解方案。

英文摘要:

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.

机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。

↑