在浏览在线资源时,我注意到可满足性的不同之处。
有时资源要求显示给定的命题是否可以满足?
但是,有时他们会要求证明一组命题是否可满足?
我对可满足性到底与什么有关感到困惑。它必须与单个命题或一组命题有关吗?
在浏览在线资源时,我注意到可满足性的不同之处。
有时资源要求显示给定的命题是否可以满足?
但是,有时他们会要求证明一组命题是否可满足?
我对可满足性到底与什么有关感到困惑。它必须与单个命题或一组命题有关吗?
两者都有道理。
通常,当您有一组命题并要求可满足性时,您是在询问是否存在使所有这些命题同时为真的令人满意的分配。因此,您可以将单个命题视为单例集,在这种情况下,它的可满足性与恰好只有一个元素的一组命题的可满足性相同。
旁白:当你谈论一组命题时,你应该清楚空集的可能性。空的命题集是可满足的吗?答案很简单:是的,微不足道。任何分配都满足一组空的命题。这类似于True
布尔连接的标识元素。
正如@Tim 在评论中指出的那样,另一个方向是考虑如果集合是无限的会发生什么。那么可满足性是如何定义的呢?在这种情况下,我们提到紧凑性(https://en.wikipedia.org/wiki/Compactness_theorem),它表明如果所有有限子集都是可满足的,则可以满足无限的命题集。不过,细节可能超出了 OP 的意图,因此将其留给另一个问题。
请注意,在 SAT 和 SMT 求解器的大多数实际应用中,除非您有量词,否则您无需担心无限情况。只要你坚持无量词子集,一切都是有限的。