ブール式の膨大なセット（20000）があります。それらは、、ANDおよびOR演算NOT子と多数のブール変数、、A1... （約1000）A2で構成されます。A3ほとんどの式には、これらの変数のうち5つ、おそらく20つしか含まれていません。
変数（A1 = true, A2 = false, A3 = false ...）の割り当てが与えられた場合、に評価される式を見つける必要がありますfalse。
同じ式のセットが、複数（10〜100）の割り当てに対して評価されます
この目的のために：
式をディスクに保存して高速にロードおよび解析できるようにするにはどうすればよいですか（現在、式は特殊なDSLとして、または多かれ少なかれ正規化された（そして非常に遅い）リレーショナルデータ構造として持っていますが、変更できます）
私が使用できるそのような式を評価するための高速なアルゴリズム/データ構造はありますか？
JVM上の実装は存在しますか？
式を連言標準形に変換し、同様の用語を組み合わせることを検討することをお勧めします。次に、式を一連の用語に双方向にマッピングできます。いずれもfalseと評価されると、式全体がfalseと評価されることを意味します。変数の割り当てごとに、一連の式から始めて、falseと評価されるまでCNF用語を評価します。その用語が偽の場合、その用語を含むすべての式も偽になるため、それらの式もセットから削除できます。
そのようなアプローチがあなたのケースに合うかどうかは、式を見ずに言うことはできません-1000個の変数と20000個の式があるので、それらに多くのCNF用語が共通しているわけではないかもしれません。
Javaの外部では、式の数がはるかに多い場合、GPUでの実装が明らかであるため、DNFの方がおそらくより便利です。
これに対するSOPの答えは、式を文字列としてRPN（逆ポーランド記法）に格納し、それらを評価するための単純なStackMachineパーサーを作成することです。
一般に、RPN文字列は、すでにメモリ内にあるAST（抽象シンボルツリー）とほぼ同じ速度で評価できます。そして、スタックマシンパーサーは非常に簡単に記述できます。
あなたはJavaに執着しているように見えますが、eval（）関数を持つ言語にこれらのものを供給することを検討しましたか？おそらく、ファイルに式を保存して評価することで問題が軽減されるでしょう。式（のソース）を信頼しない場合、これにはセキュリティ上の影響があることに注意してください。
Jythonが思い浮かびますが、これを非常に短時間で実行できるものはおそらくいくつかあります。
Javaと結婚している場合は、ブール代数の再帰下降パーサーを実装できます。しかし、それはかなり複雑です。
更新：次のサイトには、役立つ可能性のあるコードがあります。
式のリストを関数のソースコードに変換します。この関数を変数の値で呼び出すと、すべての関数が評価され、どの式がfalseと評価されるかが示されます。関数をコンパイルしてから、さまざまな変数値に対して呼び出します。
私は同様のことを行い、Pythonを使用しました。私が書かなければならなかった唯一の構文解析と解釈は、入力ブール演算子'＆'、'|'、'〜'を対応するPythonに変換することでした。
あなたの問題のサイズはPythonソリューションにとってはかなり問題ないようです。
変数ごとに、変数が正に発生する式と負に発生する式の2つのセットを記録するインデックスを作成できます。変数の値に応じて、この変数が原因でfalseになる可能性のある式を収集します（変数がfalseに設定されている場合、またはその逆の場合は正の値になります）。編集：これらは単なる候補ですが、実際に偽になるかどうかを確認するために評価する必要があります。
これがすべての式を評価するだけの場合と比較して役立つかどうかは、式の構造と、falseと評価される式の数によって異なります。
それらをCNFに変換し、MiniSatを使用して、式がtrueまたはfalseに評価されるかどうかを確認してください