基于Prolog CLPFD求解Cryptogram游戏第9关谜题的技术问询

最近在Google Play上淘到一款叫Cryptogram的小游戏，同类应用一搜居然有几十款，挑了这款玩了起来。游戏规则挺明确的：需要把数字和对应颜色匹配起来，让所有给出的等式都成立才行。

我手动刷关的速度还不错，第1到8关加上第10关没怎么费劲就快速通关了，但第9关属实是个难题——试了好多次，猜来猜去都不对，完全卡壳了。折腾了半天没结果后，我突然想起本科阶段用Prolog/Datalog做过一些小型任务，不如写个程序来自动求解这关？

内容的提问来源于stack exchange，提问作者bananafacts