大きな有限領域上の最適化を伴う制約解法への一般的なアプローチ？

Question

は、私が「楽しい」プロパティのカップルを持っている私が取り組んできた制約問題、持っている：

• ドメインが巨大です。基本的な制約により、2^40〜2^30程度になりますが、それを下げるのは難しいです...
• 解決策の最適化。単一の制約付きソリューションはありません。私はいくつかの複雑な述語に基づいてドメイン内の最適な適合を探しています。

私はErlang、Haskell、およびPrologをブラッシュアップしましたが、これらの言語にはまだ私が探している高度な述語がありません。私はを知っています私の最適化のいくつかは、検索スペースを減らす可能性があり、人間は、ドメインをかなり早く精通し、最適な答えについての本当に良い推測をすることができます。ドメインは数十の変数でパラメータ化されており、ドメイン内で最良のものに近い候補を選択するのは本当に簡単です。

私がこの質問で探しているのは、魔法のアルゴリズムではありませんこの検索を扱いますが、PrologとHaskellはこれに適したツールではないので、どの言語やライブラリがより良い答えになるのでしょうか？ I にはが書かれていますが、600万アイテムの制限付き検索では1秒間に1万回の比較に達することさえできませんでした。おそらくこれはHaskellがこれらの問題を表現するのに適していないからです。

Answer 1

正しく覚えていれば、Coqは計算上の制約をうまくサポートしています。少なくとも、ドメインが正式なシステムとして記述されている場合、Coqはコードとして書き留めて基本的な計算を実行するのに役立ちます。