论文标题
正式验证的非二元约束转换为二进制约束
Formally Verified Transformation of Non-binary Constraints into Binary Constraints
论文作者
论文摘要
在约束编程社区中众所周知，任何非二进制约束满意度问题（带有有限域）都可以转变为同等的二进制二进制文件。最著名的翻译之一是隐藏的变量编码。在本文中，我们在证明助手的COQ中形式化了此编码，并证明二进制约束满意度问题的任何解决方案都可以构建原始问题的解决方案，反之亦然。这种正式开发用于完成Carlier，Dubois和Gotlieb在2012年在COQ中开发的正式验证的约束求解器，使其成为能够解决任何N- ARY约束满意度问题的工具，这是转换器与COQ二元求解器之间连接成功的关键，这是后者的一般性。
It is well known in the Constraint Programming community that any non-binary constraint satisfaction problem (with finite domains) can be transformed into an equivalent binary one. One of the most well-known translations is the Hidden Variable Encoding. In this paper we formalize this encoding in the proof assistant Coq and prove that any solution of the binary constraint satisfaction problem makes it possible to build a solution of the original problem and vice-versa. This formal development is used to complete the formally verified constraint solver developed in Coq by Carlier, Dubois and Gotlieb in 2012, making it a tool able to solve any n-ary constraint satisfaction problem, The key of success of the connection between the translator and the Coq binary solver is the genericity of the latter.
