标签: satisfiability

如何在haskell中获得随机命题公式？我最好在CNF需要配方,但我愿意

我想使用也涉及SAT求解器的性能测试公式.请注意,我的目标不是测试SAT求解器的性能!我也对非常困难的公式不感兴趣,所以难度应该是随机的,否则只包括简单的公式.

我知道我的真实世界数据导致了SAT求解器并不困难的命题公式.

目前,我使用hatt和SBV库作为数据结构来处理命题公式.我也查看了hGen库,也许它可以用来生成随机公式.但是没有文档,我没有看到hGen的源代码.

我的目标是选择n并获取包含n布尔变量的公式.

我正在尝试寻找解决问题的实用方法(例如在工程方面的努力),其中我有一堆未知值:

val a: Int32 = ???
val c: Int32 = ???
val d: Bool = ???

和表达式二进制树(在内存中),最终返回一个布尔值,例如

((a > 4) || (b == (c+2))) && (a < b) && ((2*d)) || e

我有的布尔运算符and or xor not和32位整数有比较的东西,以及加法,乘法,除法(注意:这些必须尊重32位溢出!)以及一些按位的东西(移位,按位&,| ^).但是,我不一定需要支持所有这些操作[参见:LOL_NO_IDEA]

我想得到三个答案中的一个:

• ES_POSSIBLE [我不需要知道如何,只是被告知它有可能存在的方式]
• 不可能[无论我的变量保持什么值,这个方程永远不会是真的]
• LOL_NO_IDEA [如果问题太复杂或耗时,这是可以接受的]

我正在解决的问题都不是太大或太复杂,而且条款太多(最多的是大约数百个).并且有大量的LOL_NO_IDEA可以.然而,我正在解决数以百万计的这些问题,因此不断的成本将会刺痛(例如转换为文本格式,并唤起外部解算器)

因为我是用scala做的,所以使用SAT4J看起来非常吸引人.虽然,文档很糟糕(特别是像我这样的人,他们只关注这个SAT世界几天)

但我目前的想法是,首先将每个Int32变为32个布尔值.这样我可以通过将它作为嵌套布尔表达式来表达像(a <b)这样的关系(比较msb,如果它们是eq,那么下一个等等)

然后当我有一个布尔变量和布尔表达式的大表达式树时 - 然后遍历它,同时逐步建立一个:http: //en.wikipedia.org/wiki/Conjunctive_normal_form

然后将其喂入SAT4J.

然而,所有这些看起来都非常具有挑战性 - 甚至构建CNF似乎效率很低(以天真的方式做,我实现它)并且容易出错.更不用说尝试将所有整数数学编码为布尔表达式.而且我无法为像我这样的人找到好的资源,一个想要使用SAT解决问题的工程师主要是一个黑盒子

我很感激任何反馈,即使它像"哈哈,你的白痴 - 看看X"或"是的,你的想法是正确的.享受!"

我找到了一种使用此链接中描述的方式找到所有解决方案的方法。

这工作正常，但速度很慢。由于它从一开始就重新计算约束，因此 i_e 没有利用之前的计算。

现在，我在此链接中看到 ，有一种更有效的方法可以使用 MiniSat 作为库来查找所有解决方案。但那里没有描述方法。

您能否为我指出正确的文档，以便有效地找到所有 SAT 解决方案？

谢谢。

我们知道DPLL算法是回溯+单位传播+纯文字规则。

我有一个例子。有一个示例可以解决DPLL的以下可满足性问题。如果给变量分配“ 0”先于给变量分配“ 1”，那么哪个Unit Clause (UC)或哪个Pure Literal (PL)用于解决此特定示例？

{~A \/ B \/ C}, {A \/ ~B \/ C}, {A \/ B \/ ~C}, {A \/ B \/ C}

在此示例中，使用其中两个（PL and UC）编写。为什么选择其中两个？任何的想法？

有谁知道有一个好的程序可以将每个子句包含任意数量变量的 CNF 文件转换为每个子句包含 3 个变量的 CNF 文件 (3-CNF)？我在计算机科学书籍中看到过这个算法，但在任何地方都找不到实现，如果其他人已经这样做了，我不想浪费时间自己实现它。谢谢！

我读了许多用于找到2-SAT问题的算法,即给定表达式是否可满足,可以在多项式时间内求解.例子(算法).
对于Krom的程序(维基百科),我构建了图,我可以从中轻松验证其在多项式时间内的可满足性.
现在,我想找到这个表达式的解决方案是可以满足的.
我这样想(验证它):首先我采用形成强连通分量的任何字面表示x,并将值赋值为0.然后根据算法,存在edge(x! - > y).因此y不能为0.(因为1 - > 0是假的)并且如果可能的话同样地进行.
否则取x = 0,然后只选择y = 1,同样继续获得任何可满足的实例.

现在,是在多项式时间内找到任何一个的任何可行解决方案

• 提供表达式可满足的所有可能解决方案.
• 或者这个表达式对于具有总k literals = 1的输入是可满足的.
• 或者,为了满足表达式,有多少最小文字数值为1.

对于这类问题,我没有得到任何多项式算法.