问题标签 [cnf]

我想用模型检查器测试我的代码，并以自动化的方式制作一个 FSM。为此，我需要一个模型检查器并将 FSM 结果转换为 CNF。

有什么建议我可以在 Python 中做到这一点吗？我只知道 CBMC，但仅限于 C。

谢谢阿德里安

我在使用通用导航框架构建的视图中有一棵树。我有一个包含 IFolder 对象的自定义项 MyTreeEntry。

我想将 MyTreeEntry 项的所有菜单条目视为 IFolder（新建，在新窗口中打开...），并且当调用某个操作时，它必须对包含的 IFolder 起作用。

有可能吗？怎么做？

我正在尝试使用适当的基准 Java 类（cnf.files）加载我的 java Harness 类（DaCapo Benchmark 套件）。在 Windows 中，命令“java Harness 工作得非常好。但是，由于我是 Linux 新手，当我尝试加载我的 java 线束类时，我会收到消息“未知基准”。请注意，“java Harness -l”显示所有可用的基准这个 java Harness 类的。

您知道如何像在 Windows 中那样加载我的 java Harness 类吗？

我正在尝试通过 R 连接到 MySQL 服务器，它与以下行完美配合：

但是，我想使用 cnf 文件，以便我的用户/密码凭据不会出​​现在我的代码中，并尝试了以下操作：

这就是我的 cnf 文件的外观：

它与我当前工作目录的 R 脚本位于同一文件夹中。但是，我遇到了以下错误：

请问有什么建议吗？

非常感谢

我正在尝试使用 Microsoft Solver Foundation SatSolver 通过 Visual Studio（C# 或 VB）解决一个简单的 CNF 问题。谁能发布一个简单的例子来解释如何做到这一点？

这是一个简短的例子：

结果应该只有一个值为 1 的变量，其余的应该有 0，但解是 1,1,1,0。

谢了，兄弟们

我设法将表达式简化为以下表达式（根据 WolphramAlpha，原始表达式和下面的版本都解析为相同的 CNF）。

接下来是什么？

我有一个 DIMACS cnf 格式的文件，我需要将其处理为 SAT Solver 所需的格式。

具体来说，我需要得到：

至

谢谢您的帮助！

所以这是一个我似乎很困惑的简单问题，我一直在研究这个输入问题，并试图将用户输入的某些部分存储到分段列表中。

用户输入将输入一个 CNF（连接范式）。示例：+ = or, * = and, ( and ) 中的任何内容都是子句

(A+B)*(C+D)

因此，由于此输入有两个子句，我需要将每个子句作为它们自己的项目存储到列表中。我无法弄清楚如何遍历我已经制作的列表并让我的 if 语句对每个子句进行分段，我从逻辑上理解它应该如何工作，我只需要与将某些内容动态存储到列表。

我全心全意地理解为什么索引不起作用，我基本上是在寻找索引方法的反面，我需要找到与我的索引关联的项目。

例如，当我找到一个开放的括号“（”时，我需要开始将一个新子句存储到我的列表中，到目前为止我只找到了如何返回索引本身而不是通过索引返回项目。这应该是一个简单的解决方案对此，但我根本找不到与明智地显示此方法相关的任何内容。

我的代码作为指导

我知道证明喇叭公式是否可满足更容易。我的问题是：为什么使用喇叭公式而不是普通 CNF 更容易？

听起来 Package Explorer 视图的全部内容都是通过 Common Navigator Framework 公开的。

我怎样才能访问这些数据？我想查看其中所有项目、文件和方法的名称。我得到的最接近的是：

但 els 是空的，可能是因为我不知道将什么传递给 getElements。

一些有趣的调试：当我使用调试器深入 getElements 调用时，看起来 findRootContentExtensions 找到了一堆看起来很有希望的 NavigatorContentDescriptor，但随后它们没有返回，因为它们未通过 isActive 和 isRootExtension 检查。然后它继续尝试找到其他要返回的东西，但它考虑到我传入的对象，并继续不起作用。我不知道发生了什么事。

我发现的所有文档都侧重于使用 CNF 添加新视图，而不是查看工作区的现有内容。有什么好的文档吗？谢谢！