问题标签 [satisfiability]

The Subgraph Isomorphism (SI) problem is a computational task in which two graphs G and H are given as input, and one must determine whether G contains a subgraph that is isomorphic to H.

This is a NP-Complete problem .

I want to know its relation with the SAT problem.
In particular, I want instances of this problem can be solved throughout SAT Solver(like miniSAT).I need an alorithm which can do a mapping from SI to SAT problem in polynomial time and then SAT assignment can be used to find a mapping from nodes of G to nodes of H .

Any idea ???

只是尝试使用 smtlib。我没有看到以下内容有什么问题...

使用 z3 运行它，错误是：（错误“第 7 行第 2 列：无效的合格/索引标识符，'_' 或 'as' 预期的”）

为了求解一组布尔方程，我正在使用以下输入对Constraint-Programming Solver MiniZinc进行试验：

MiniZinc确实找到了小参数的解决方案(rows=cols=2, products=7)，但并没有随着略微增加的参数而结束。我想将生成的FlatZinc模型输入到SAT 求解器中，例如Cryptominisat、Lingeling或Clasp。我希望这些工具的性能可能优于现有的 MiniZinc 后端。

我的问题：
是否有任何工具可以将纯 Boolean FlatZinc模型转换为CNF (DIMACS)？由于某些 MiniZinc 后端似乎不支持它，
我能做些什么来替换谓词？xorall()

我的代码得到了错误的答案

n 是变量的数量，公式是包含子句的列表

给定一个包含“n”个变量和在列表“公式”中编码的子句的 SAT 实例，如果该实例可满足，则返回“可满足”，否则返回“不可满足”。'formula' 的每个元素代表一个子句，是一个整数列表，其中整数 i 表示文字 Xi 存在于子句中，整数 -i 表示文字 ~Xi 存在于子句中。例如，子句“X1 v ~X11 v X7”用列表 [1, -11, 7] 表示。

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

现在我可以用hatt包解析命题公式了；请参阅testParse下面的功能。

我还可以使用 SBV 库运行 SAT 求解器调用；请参阅testParse下面的功能。

问题： 在运行时，我如何在 SBV 库中生成一个类型的值，该值Predicate表示myPredicate我刚刚从字符串中解析的命题公式？我只知道如何手动键入forSome_ $ \x y z -> ...表达式，但不知道如何编写从Expr值到类型值的转换器函数Predicate。

可能有用的信息：

这是 BitVectors.Data 的链接：http: //hackage.haskell.org/package/sbv-3.0/docs/src/Data-SBV-BitVectors-Data.html

这是示例代码形式 Examples.Puzzles.PowerSet：

这是 Expr 数据类型（来自 hatt 库）：

在我的最后一个问题中，我问我如何解析一个命题表达式，然后在 SBV 库的帮助下找到公式的所有模型。我使用 hatt 库来解析布尔表达式。

不幸的是，SBV 似乎不适合相当快速的 SAT 求解，或者查找所有模型的“allSat”功能没有实现速度。毕竟 SBV 是针对 SMT 解决的。

我使用证明器 Z3 和 CVC4 测试了 haskell SBV 包的性能，并与 picosat 进行了比较。我使用了一个包含 36 个变量和 840 个有效模型的命题公式。picosat 的结果是用了 0.5 秒，而 Z3 用了 3 分钟，CVC4 用了 6 分钟。SBV 和“allSat”函数有一些性能技巧可以为命题公式修剪它。或者其他一些证明器可能比 Z3 更快。

但我现在假设我可能需要使用更快的选项来解决 SAT 问题，并且我想使用 PicoSAT 或 MiniSAT，因为我过去取得了不错的成绩，而且 SAT 比赛的成绩看起来也不错。

问题：

• 是否存在适用于查找命题公式的所有模型（即在 C/C++ 级别以获得快速结果）的 Picosat 或 MiniSAT 绑定？例如，与 picosat 的 python 绑定具有一个功能“itersolve”，它就是这样做的。但是我找不到用于 haskell picosat 或 miniSAT 绑定的这个函数（也许我忽略了它们）。

• 我应该如何从使用 hatt 包解析的字符串到适用于 picosat/miniSat 的“int 列表”。因此，从 hatt 库中的类型表达式Expr变为以适合于例如 picosat 的样式表示 CNF 公式。Picosat 使用整数列表的常见 SAT 格式。请注意，我从字符串解析的公式最初已经在 CNF 中。要么我直接从一个 hat Expr 到 int 列表。或者，我将上一个问题中的代码用于适合allSatSBV 功能的格式，并重新实现 SBV 功能的变体allSAT以使用 picosat/miniSAT 的 hasekll 绑定。

链接：

• 我的最后一个问题
• SBV 库
• 哈特图书馆
• haskell picosat 绑定
• 小卫星

如何在haskell中获得随机命题公式？最好我需要 CNF 中的公式，但我会

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

我知道我的真实世界数据导致的命题公式对于 SAT 求解者来说并不困难。

目前，我使用hatt和SBV库作为数据结构来处理命题公式。我还查看了hGen库，也许它可以用来生成随机公式。但是没有文档，而且我通过查看hGen的源代码也没有走多远。

我的目标是选择n并取回一个包含n布尔变量的公式。

给定一组子句，我想首先检查它们是否可满足。如果是，我想简化它们并创建一个 CNF，例如，(a OR b) ^ (NOT b) 应该简化为：a ^ (NOT b)。我只使用命题公式。我尝试使用 Java SAT4j 库来执行此操作。它可以告诉我这组子句是否可以满足，但似乎没有任何方法可以让我返回一个简化的 CNF。我可以做些什么来有效地简化 CNF？是否有任何 Java 或 Python 实现？

I would like to parse string with a propositional formula in CNF to DIMACS, thus a nested int list in haskell. The format is suitable for the haskell picosat bindings that seem to be more performant then other options for SAT solving.

The problem is that my code that implemented this is too complicated and now I am looking for a possible bug that is not obvious to find.

(My approach was to use the haskell hatt package, change the package so it uses Strings instead of single characters for variables names, parse the expression with hatt and then convert the resulting expression to the DIMACS format.)

I want to parse a string that represents a propositional formula in CNF notation (see example below). The result shoud be a nested list of ints. Thus the result should be suitable for solveAll that is part of the haskell picosat bindings.

Input:

Result:

问题：如何更改上面的示例以并行运行两个 sat 调用，即使用并发？如果有不同的选择，我对性能感兴趣。

（只是检查一下：据我了解，ST monad 是正交的，不能与并行化/并发一起使用。ST monad 一开始让我有点困惑，这是我问这个问题的原因之一。）