在大型有限域上約束求解的一般方法？

Question

我有一個約束問題我一直在工作，其中有一對夫婦的「好玩」的屬性：

• 域名是巨大的;基本約束將其降至2^40至2^30左右，但如果沒有進一步降低成本，則很難進一步降低...
• 解決方案的優化。沒有單一的約束解決方案;基於一些複雜的謂詞，我正在尋找最適合的領域。

在尋找一種方式來處理這個問題，我已經刷了我的二郎，哈斯克爾和前導，但是這些語言已經沒有我要找的先進謂詞。我知道，我的一些優化可能會降低搜索空間，人類可以相當快地仔細閱讀域名，並對最佳答案做出真正的猜測。 （該域在十幾個變量上進行了參數化;挑選異常值作爲接近域中最好域的可能候選非常容易。）

我在這個問題中尋找的不是一個神奇的算法處理這個搜索，但是這個問題的答案是：由於Prolog和Haskell不是這個的正確工具，哪種語言或庫可能是更好的答案？我在有寫在Haskell，但在一個有限的600萬項目的搜索，它甚至不能達到每秒一萬次比較，也許這是因爲Haskell不適合表達這些類型的問題。

Answer 1

如果我沒記錯的話，Coq對計算約束有很好的支持。至少，如果您的域可能被描述爲正式系統，Coq將幫助將其寫成代碼並執行基本計算。