假设我有一个带有变量(a,b,c,d,e,f,g)的CNF表达式。考虑到{a,b,c,g} = {1,0,0,1}和{a,b,c,g} = {1,1,1,1}，我将如何使用SAT求解器找到(d,e,f)的分配？如果是一个假设，请致电SAT求解器查找{d,e,f}的作业，将是直接向前的（例如，通过将单元子句添加到CNF中）。但是，如果我有多个假设怎么办？这可能吗？
这是哈罗德（Harold）试图向您描述的步骤。您在变量A，B，C，D，E，F和G。
上有一些CNF公式F。- 复制公式，称重复g。
- 在g中，用bb，c用cc和gg替换变量a，用gg。 。
- 将单位子句添加到f，以便（a，b，c，g）=（1,0,0,1）。
- 将单位子句添加到G中，以便（AA，BB，CC，GG）=（1,1,1,1）。
- 加入公式F和G，并将结果馈入SAT求解器。
求解器将找到与（a，b，c，g）和（aa，bb，cc，gg）的预设值一致的令人满意的分配。
尚不清楚您是否想要一个实用的答案或有趣的理论答案。我会追求实用。
对于每组假设，请调用一个支持求解的SAT求解器，该求解器在一组假设（示例）上使用假设。在同一求解器实例上依次执行此操作。
专利：
- 您不将相互排斥的假设集令人满意。如果一组假设a是sat sat sat for formula f，而另一组是f的f in for f，则每个对求解器的呼叫都会告诉您这些假设是否为SAT/UNSAT。
- 从第一个通话中学到的从第一个电话中学习的子句可能会进行第二个通话。中级学习的子句讨论了相同的变量。（注意：如果您具有不相交的公式
F & G，其中f超过变量x，g超过变量y和x and y共享不共享变量，则分辨率 - CDCL中使用的推理规则 - 无法得出CORME COMING f and G。除非一个实例更容易证明并提早停止，否则将两者混合在一起而不是将它们分开的明显收益。）
cons：
- 如果实例A在实践中很难解决，但是A是微不足道的，您可能会陷入A。
- 这不是平行的，因此，如果您要尽快解决两个实例，则需要其他机制。
我知道这是一个明显的答案，但值得尝试。如果失败了，您可以尝试做更奇特的事情，例如解决W.R.T.A union A'的假设，并且只有在解开解决的情况下，该假设却落后于A当时的A'。这对您的示例无济于事，因为(a,b,c,g) = (1,0,0,1)和(a,b,c,g) = (1,1,1,1)是互斥的。