関連：CNFの単純化（実際、その質問の送信者は、私がここで欲しいものを求めていたのではないかと思います）
DIMACS 形式の CNF 式を単純化 (または解決する前に「前処理」) するためのツールが多数あり、ほとんどの SAT ソルバーにはいくつかのツールが組み込まれています。しかし、私が知っていることはすべて、自明に充足可能な式をゼロまたは 1 つの変数を持つ自明に充足可能な CNF に単純化することです。つまり、式の充足可能性を維持しようとするだけです。少なくとも、SatELite と cryptominisat の前処理モードを試しました。
ただし、大規模な問題の CNF を構築する場合、問題の明確に定義されたサブセットを一度に単純化することは非常に有用であるように思われます。これらの部分式のいくつかの変数間の制約。
それで、ツールは存在しますか、それとも通常のSATソルバー（または最小化したいCNFを生成するために使用しているZ3のような他のソルバー）を何らかの方法で巧妙に使用して、すべてのソリューションを維持しながらCNF式を単純化できますか与えられた変数のセットについて？