SMCHR：满足性模块化约束处理规则
摘要：基于限制处理规则（Constraint Handling Rules, CHRs）的规则集成是一种高级的基于规则的编程语言，用于约束求解器的规范和实现。CHR操作一个表示约束平面连结的全局存储。默认情况下，CHR不支持具有更复杂命题结构（包括析取、否定等）的目标，或者CHR依赖于宿主系统提供此类功能。本文介绍了基于可满足性模块的约束处理规则（Satisfiability Modulo Constraint Handling Rules, SMCHR）：一个将CHR与现代布尔可满足性（SAT）求解器紧密集成起来的系统，用于具有任意命题结构的量词自由公式。SMCHR本质上是一个实现在CHR中的模块化理论可满足性（Satisfiability Modulo Theories, SMT）求解器。SMCHR的执行算法基于惰性子句生成，即每当应用一条规则时，就会生成一个新的SAT求解器子句。我们还将探讨构建SMCHR系统的实际方面，包括扩展“内建”约束求解器以支持具有统一和合理化的等式。
作者：Gregory J. Duck
论文ID：1210.5307
分类：Programming Languages
分类简称：cs.PL
提交时间：2012-10-22