REVIEW 2 cited by
Formally Verified Transformation of Non-binary Constraints into Binary Constraints
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
read the original abstract
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.
Forward citations
Cited by 2 Pith papers
-
LeanCSP: A Framework for Certifying Constraint Reformulation and Solving in Lean
LeanCSP certifies both parametric CSP reformulations and external solver certificates in Lean, yielding end-to-end (un)satisfiability without trusting solvers.
-
When Influence Misleads: Informational and Strategic Limits of Social Learning in Trading Networks
On eToro, traders mirror popular investors rather than profitable ones, and the simulation used to argue for performance-based signals depends on an autocorrelation in returns that the data do not show.
Discussion (0). Sign in to comment.