简化CNF公式，同时保留所有包含某些变量的解 [英] Simplifying CNF formula while preserving all solutions wrt certain variables
问题描述
相关: CNF简化(实际上，我认为该问题的提交者可能是在我之后要在这里
Related: CNF simplification (in fact, I think the submitter of that question might have been after what I want here)
存在许多用于简化(或在求解之前进行预处理")DIMACS格式CNF公式的工具，并且大多数SAT求解器都包含一些工具.但是，我所知道的全部都是将一个可满足条件的公式简化为具有零个或一个变量的可满足条件的CNF，即它们仅试图保持该公式的可满足性.我至少尝试过SatELite和cryptominisat的预处理模式.
A number of tools exist for simplifying (or "preprocessing" before solving) DIMACS format CNF formulas, and most SAT solvers incorporate some. However, all that I am aware of simplify a trivially satisfiable formula into a trivially satisfiable CNF with zero or one variables, i.e. they only attempt to preserve the satisfiability of the formula. I have tried at least SatELite and cryptominisat's preprocess mode.
但是，对于构造一个大问题的CNF，在我看来，一次简化一个明确定义的问题子集非常有用，然后可以在最后一次重复很多次CNF在这些子公式中的某些变量之间具有附加约束.
However, for constructing CNF of a large problem, it seems to me that it would be quite useful to simplify a well-defined subset of the problem at a time, which may then be repeated a large number of times in the final CNF with additional constraints between some variables in these subformulas.
那么，是否存在任何工具，或者可以以某种巧妙的方式使用普通的SAT求解器(或其他求解器，例如Z3，我正在使用它来生成CNF，我想将其最小化)来简化CNF公式，而保留给定变量集的所有解决方案?
So, do any tools exist, or can ordinary SAT solvers (or other solvers like Z3, which I'm using to produce the CNF I would like to minimize) be somehow used with some cleverness, to simplify a CNF formula while preserving all solutions wrt a given set of variables?
推荐答案
协处理器 SAT预处理器可以执行您想要的操作.可以给它一个可选的变量范围，并且只会在该范围内应用保持等价的简化形式.在此范围之外，它将应用更强大的，可满足性的简化方法.至少在版本2中就是这种情况.
The Coprocessor SAT preprocessor can do what you want. It can be given an optional variable scope and will only apply equivalence-preserving simplifications within that scope. Outside that scope, it will apply stronger, satisfiability-preserving simplifications. At least that was the case in version 2.
这篇关于简化CNF公式，同时保留所有包含某些变量的解的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
