相关：CNF 简化（事实上，我认为该问题的提交者可能一直在追求我想要的东西）
存在许多用于简化（或求解前“预处理”）DIMACS 格式 CNF 公式的工具，并且大多数 SAT 求解器都包含一些工具。然而，我所知道的一切都将一个平凡可满足的公式简化为一个具有零个或一个变量的平凡可满足的 CNF，即它们只试图保持公式的可满足性。我至少尝试过 SatELite 和 cryptominisat 的预处理模式。
然而，对于构建一个大问题的 CNF，在我看来，一次简化一个明确定义的问题子集会非常有用，然后可能会在最终的 CNF 中重复很多次，并添加额外的这些子公式中的一些变量之间的约束。
那么，是否存在任何工具，或者普通 SAT 求解器（或其他求解器，如 Z3，我用来生成我想最小化的 CNF）以某种方式巧妙地使用，以简化 CNF 公式，同时保留所有解决方案wrt一组给定的变量？
Coprocessor SAT 预处理器可以做你想做的事。它可以被赋予一个可选的变量范围，并且只会在该范围内应用保持等价的简化。在该范围之外，它将应用更强的、保持可满足性的简化。至少在版本 2 中是这样。
也许不是您正在寻找的东西，但是 espresso 系统 ( http://embedded.eecs.berkeley.edu/pubs/downloads/espresso/ ) 可以进行布尔简化。到目前为止，它已经有 20 多年的历史了，但仍然在该行业中用于其功能。
另一种方法是将 转换CNF为And-Inverter-Graph ( AIG) 并应用逻辑综合中的方法来重构和简化AIG.
这是在伯克利大学开发的ABC程序套件中完成的。一种方法是结构散列：在 中找到公共（等效）子表达式AIG并将它们联系在一起以修剪图形。
奥地利林茨大学提供了专门用于与逆变器图的AIGER工具集。