问题标签 [satisfiability]

采取以下一组逻辑语句：

A：B是假的

B：C 是假的

C：B 或 A 为真

我被赋予了将其形式化的任务，以便“DPLL”可以确定是否存在不会导致矛盾的解决方案（哪些规则是正确的，哪些是错误的）。

问题是：我不知道该怎么做。在线求解器需要某种格式的表达式，比如这里的这个：http: //www.inf.ufpr.br/dpasqualin/d3-dpll/

我如何将我的陈述转换成这些数字？

我试图通过在 Z3 网站上放置以下内容来使用 Z3 解决 2^x=4： https ://rise4fun.com/z3/tutorial 。

Z3出品

我在滥用 Z3 吗？

所以我得到了这个作业问题，我们被要求将一个 k 独立集可满足性问题简化为合取范式下的 3-SAT 子句集。

所以对于G (V, E) 我们有顶点集
V = {x1, x2, x3, x4, x5, x6}
和边集
E = { e1 = (x1,x3), e2 = (x1,x5), e3 = (x1,x6), e4 = (x2,x5), e5 = (x2,x6), e6 = (x3,x4), e7 = (x3,x5), e8 = (x5,x6) }

我的第一种方法是每条边都有一个子句，因为我们不能在独立集中的两个顶点之间有一条边：
e1: (¬x1 v ¬x3)
e2: (¬x1 v ¬x5)
e3: (¬ x1 v ¬x6)
e4: (¬x2 v ¬x5)
e5: (¬x2 v ¬x6)
e6: (¬x3 v ¬x4)
e7: (¬x3 v ¬x5)
e8: (¬x5 v ¬x6)

但问题是，例如，对于 k = 3，如何编写子句以确保至少 3 个不同的变量 (xi) 设置为 true ？
使用加权 2 可满足性可以实现这一点，但仅使用良好的旧 3-SAT 似乎很难实现。
有关如何进行的任何提示？

我有以下条款：

我必须分别使用 DP 和 DPLL 来证明可满足性。问题是我对每种算法都得到了不同的结果。带DP：

所以是不能满足的。但是使用 DPLL：

这意味着它是令人满意的......我做错了什么？

在浏览在线资源时，我注意到可满足性的不同之处。

有时资源要求显示给定的命题是否可以满足？

但是，有时他们会要求证明一组命题是否可满足？

我对可满足性到底与什么有关感到困惑。它必须与单个命题或一组命题有关吗？

有没有人使用过基本约束？我对鸽子洞法的理解有问题我几天来一直试图理解这三个公式，我已经绝望了。谁能用一个例子向我解释这三个公式吗？

我还添加了整篇文章的链接

https://static.cambridge.org/content/id/urn:cambridge.org:id:article:S1471068413000112/resource/name/tlp2013026.pdf

我发现了这样一个例子

我可能写对了

10）公式-我认为符号和公式10我理解了。如我错了请纠正我

我需要解释第 9 和第 11 个公式

有没有人使用过基本约束？我在理解鸽洞法时遇到了问题。这是一种令人满意的方法。我已经尝试理解这三个公式几天了，我已经绝望了。谁能用一个例子向我解释这三个公式吗？

我还添加了整篇文章的链接

https://static.cambridge.org/content/id/urn:cambridge.org:id:article:S1471068413000112/resource/name/tlp2013026.pdf

我发现了这样一个例子

谁能解释一下这个例子中的公式 9-11 吗？

我可以为如下查询获取多个模型吗？

而不仅仅是

我想得到 0, 1, -1, 2, ...

假设我在 Z3 中有一组逻辑断言，我想检查可满足性。有没有办法限制令人满意的模型中的真/假总数？

例如，我可能有一组涉及 100 个布尔变量的断言，但我只对至少有 90 个 True 的解决方案感兴趣。

我想访问 Ocaml 中 Z3 的量词消除策略，以避免实现我需要的所有有效性和量词消除方法。

为此，我想知道如何从 Ocaml 调用 Z3 API（例如，来自 Python 的 Z3 作为黑盒）。

任何人都可以帮忙吗？

PS：这个活动会被称为多范式编程吗？我问这个是为了在将来找到有关类似问题的更多信息。