有关的：CNF 简化 https://stackoverflow.com/questions/23461191/cnf-simplification（事实上，我认为这个问题的提交者可能是在追求我想要的东西）
有许多工具可用于简化（或求解前“预处理”）DIMACS 格式的 CNF 公式，并且大多数 SAT 求解器都包含一些工具。然而，我所知道的一切都将一个平凡可满足的公式简化为具有零个或一个变量的平凡可满足的 CNF，即它们只是试图保留公式的可满足性。我至少尝试过 SatELite 和 cryptominisat 的预处理模式。
然而，对于构建一个大问题的 CNF，在我看来，一次简化问题的一个明确定义的子集是非常有用的，然后可以在最终的 CNF 中重复大量次，并添加额外的内容。这些子公式中某些变量之间的约束。
那么，是否存在任何工具，或者普通 SAT 求解器（或其他求解器，如 Z3，我用来生成我想要最小化的 CNF）可以以某种方式巧妙地使用，以简化 CNF 公式，同时保留所有解决方案wrt 一组给定的变量？
The 协处理器 http://tools.computational-logic.org/content/riss.phpSAT 预处理器可以做你想做的事。它可以被赋予一个可选的变量范围，并且只会在该范围内应用保留等价的简化。在该范围之外，它将应用更强大的、保持可满足性的简化。至少在版本 2 中是这样的。
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
