私は、未知の値がたくさんある問題を解決する実用的な方法 (たとえば、エンジニアリングの努力の観点から) を探しています。
val a: Int32 = ???
val c: Int32 = ???
val d: Bool = ???
最終的にブール値を返す (メモリ内の) バイナリ ツリー式。
((a > 4) || (b == (c+2))) && (a < b) && ((2*d)) || e
私が持っているブール演算子とand or xor not32 ビット整数には、比較、加算、乗算、除算 (注: これらは 32 ビット オーバーフローを尊重する必要があります!) のようなものと、いくつかのビット単位のもの (シフト、ビット単位の &、|) があります。 ^ )。しかし、必ずしもすべての操作をサポートする必要はありません [参照: LOL_NO_IDEA ]
そして、次の 3 つの答えのいずれかを取得したいと考えています。
- ES_POSSIBLE [方法を知る必要はありません。その方法が存在することを伝えてください]
- 不可能[私の変数がどんな値を保持していても、この等式は決して真ではありません]
- LOL_NO_IDEA [問題が複雑すぎるか時間がかかる場合、これは許容されます]
私が解決している問題はどれも、過度に大規模または複雑で、用語が多すぎるものではありません (ほとんどの場合、数百のオーダーです)。そして大量の LOL_NO_IDEA を持っていても問題ありません。ただし、私はこれらの問題を何百万も解決しているため、一定のコストがかかります (たとえば、テキスト形式に変換し、外部ソルバーを呼び出します)。
私はこれを scala から実行しているので、SAT4J を使用することは非常に魅力的です。ただし、ドキュメントはひどいものです（特に、このSATの世界を数日間しか調べていない私のような人は）
しかし、私の現在の考えは、最初にすべての Int32 を 32 のブール値に変換することです。そうすれば、入れ子になったブール式として (a < b) のような関係を表現できます (msb を比較し、それらが eq の場合は、次に、など)。
そして、ブール変数とブール式の大きな式ツリーがある場合、それをトラバースして、次のように段階的に構築します: http://en.wikipedia.org/wiki/Conjunctive_normal_form
それをSAT4Jに供給します。
ただし、これはすべて非常に困難に見えます。CNF を構築することでさえ、非常に非効率的であり (私が実装したような単純な方法で行う)、エラーが発生しやすいようです。すべての整数演算をブール式としてエンコードしようとすることは言うまでもありません。また、SAT 解法を主にブラック ボックスとして使用したいという問題を抱えたエンジニアである、私のような人向けに設計された優れたリソースを見つけることができませんでした。
「笑、あなたのばか - X を見てください」または「ええ、あなたの考えは正しいです。楽しんでください!」のようなものであっても、フィードバックをいただければ幸いです。