标签: satisfiability

我写了一个我认为是一个非常有趣的问题的答案,但不幸的是,在我发帖之前,这个问题被其作者删除了.我正在重新发布问题的摘要和我的答案,以防它可能对其他人有用.

假设我有一个SAT求解器,给定一个联合正规形式的布尔公式,返回一个解决方案(满足公式的变量赋值)或问题不可满足的信息.

我可以使用此求解器找到所有解决方案吗？

我想解析一个String描述命题公式,然后用SAT求解器找到命题公式的所有模型.

现在我可以用hatt包解析一个命题公式; 看testParse下面的功能.

我也可以用SBV库运行SAT求解器调用; 看testParse下面的功能.

问题: 如何在运行时生成Predicate类似于myPredicateSBV库中的类型值,该值表示我刚从String中解析的命题公式？我只知道如何手动键入forSome_ $ \x y z -> ...表达式,而不知道如何将转换器函数从Expr值写入类型的值Predicate.

-- cabal install sbv hatt
import Data.Logic.Propositional
import Data.SBV


-- Random test formula:
-- (x or ~z) and (y or ~z)

-- graphical depiction, see: https://www.wolframalpha.com/input/?i=%28x+or+~z%29+and+%28y+or+~z%29

testParse = parseExpr "test source" "((X | ~Z) & (Y | ~Z))"

myPredicate :: Predicate
myPredicate = forSome_ $ \x y z -> …

只是一个好奇的问题.还记得在课堂小组中,教授会把人分成一定数量的小组(n)吗？

我的一些教授会列出n一个想要与之合作的n人和一个不想与每个学生一起工作的人的名单,然后神奇地将n学生与他们喜欢的人匹配的小组变成一组,避免与他们一起工作他们不喜欢的人.

对我来说,这个算法听起来很像背包问题,但我想我会问你对这类问题的解决方法是什么.

编辑:找到一篇描述与我的问题完全相同的ACM文章.为了似曾相识,请阅读第二段.

SMT-Solver可用于约束求解.众所周知,CSP求解器也用于求解约束多年.那么SMT求解器优于CSP求解器的优势是什么？

我知道布尔可满足性是NP-Complete,但它是布尔表达式的最小化/简化,我的意思是以符号形式给出一个给定的表达式,并以符号形式生成一个等价但简化的表达式,NP-Complete？我不确定从可满足性到最小化的减少,但我觉得可能存在.有人有确切消息么？

我有一个布尔公式:(x_ {1}或x_ {2})和(x_ {3}或x_ {4})和.....和(x_ {2r-1}或x_ {2r}),其中x_ {i}属于集合:{p_ {1},p_ {2},... p_ {99},~p_ {1},~p_ {2},... ~p_ {99}}我必须确定给定公式的x_ {i}的某些值是否为真.

我知道这一般在计算上很困难.但是,有什么特别快的方法可以解决这个特殊问题吗？到目前为止,我已经尝试了回溯 - 这是在递归中我对每个可能的值(0或1所以不是很多)代入每个可能的变量,并且每个尚未获得值的变量都是非常正确的.在我深入了解递归之前,我会查看公式(即使并非所有变量都有值),如果它是假的,我也不会更深入.但它太慢了.有任何想法吗？我非常感谢你的帮助.

为了解决一组布尔方程,我正在使用以下输入试验Constraint-Programming Solver MiniZinc:

%  Solve system of Brent's equations modulo 2

%  Matrix dimensions
int: aRows = 3;
int: aCols = 3;
int: bCols = 3;
int: noOfProducts = 23;

%  Dependent parameters
int: bRows = aCols;
int: cRows = aRows;
int: cCols = bCols;
set of int: products = 1..noOfProducts;

%  Corefficients are stored in arrays
array[1..aRows, 1..aCols, products] of var bool: A;
array[1..bRows, 1..bCols, products] of var bool: B;
array[1..cRows, 1..cCols, products] of var …

SAT是NP完全的证明是一个建设性的证明,因此应该可以将它作为一个程序来实现.有没有人这样做过？

我正在寻找一个程序(编译器),它将一个程序(返回true或false)作为输入,并输出一个SAT公式.

因此,例如,编译器可以采用以下程序(以pythonic语法显示,但任何语言都适合我)作为输入,并输出SAT公式.将SAT公式提供给SAT求解器将给出参数"证书"的解决方案.在这种情况下,解决方案将是[False,True,True,True,False],表明{-3,-2,5}是一个解决方案.

def verify(certificate):
  problem = [-7, -3, -2, 5, 8]
  sum = 0
  for (x, b) in zip(problem, certificate):
    if b:
      sum += x
  return sum == 0

显然,输出SAT公式将具有其他辅助变量,因此编译器必须指示哪些变量对应于证书.

这样的编译器已经存在吗？他们中的任何一个都是开源的？

问题

我正在研究SAT优化问题的一个特殊子集.对于那些不熟悉SAT和相关主题的人,这里是相关的维基百科文章.

TRUE=(a OR b OR c OR d) AND (a OR f) AND ...

没有NOTs,它是联合正常形式.这很容易解决.但是,我正在尝试最小化真正的赋值数,以使整个语句成立.我找不到解决这个问题的方法.

可能的解决方案

我提出了以下解决方法:

1. 转换为有向图并搜索最小生成树,仅跨越顶点子集.有Edmond的算法,但它给出了完整图形的MST而不是顶点的子集.
   • 也许有一个版本的Edmond算法可以解决顶点子集的问题？
   • 也许有一种方法可以用原始问题构建一个可以用其他算法解决的图形？
2. 使用SAT求解器,LIP求解器或穷举搜索.我对这些解决方案不感兴趣,因为我正在尝试将此问题用作讲义材料.

题

你有什么想法/意见吗？你能想出其他可行的方法吗？

今天我也想看看在haskell中解决SAT的选项.首先,我想把自己的接口写入picosat求解器.

然后我发现有SBV库.它是Z3,Yices,CVC4和Boolector的接口.

此外,我在github上进行了谷歌搜索,它甚至可以使用Picosat绑定.

考虑到快速/高性能的限制,是否有任何其他针对SAT求解器的haskell绑定值得关注.Carification:适用于高性能SAT解决(例如,运行数天的问题,以及需要在检查2 ^ 20或更多SAT问题时尽快完成的问题).例如,我在hackage上特别缺少的是绑定到像Plingeling这样的快速并行 SAT求解器.(另外,我在github上发现了当前更新的picosat绑定更多的意外,我很可能会错过其他选项)

SBV库的默认选项是Z3 SMT解算器.在我受过良好教育的猜测中,我是否正确,对于简单的SAT解决而言,picosat比Z3更快？