问题标签 [cnf]

我正在尝试动态生成数学逻辑并将其传递给递归函数 dfsCompute 但我无法这样做。我想知道我应该传递什么以便将传递的值视为一个数组并进行相应的评估。请找到下面的代码片段：

请让我知道如何动态生成逻辑并将其传递给递归函数并在 if 条件中进行检查。

当我使用 Common Navigator Framework 时，我找不到如何让它像 TreeViewer 一样支持复选框。

一开始打算用Check Tree View，但是不能充分利用RCP机制，所以决定用Common Navigator Framework....

我最近一直在尝试学习逻辑，但我遇到了一个我做不到的查询，我不太确定我哪里出错了。将查询转换为 CNF 时，遇到这种特殊情况会怎么做？

我将如何重新安排它以使其成为 CNF 形式？我做错了什么吗？

谢谢你的帮助，肖恩

如果 PCFG 是这样的，

什么是 CNF 形式？会是以下吗？

还是别的什么？

给定以下概率上下文无关语法 -

CNF 会是什么？

我在 Verilog 中有一个示例组合循环，我可以按照说明进行逻辑综合并生成 blif 文件。

但是，我需要的是从电路中生成 CNF 公式。ABC 等工具仅允许从组合斜接生成（即，具有 1 个输出）。

我尝试了 yosys 指令“sat -dump_cnf FILE”，确实可以生成 CNF 文件。但是，我不确定如何将 CNF 中的变量与电路中的 I/O 映射。

有没有人研究过 Yosys 的“sat -dump_cnf”功能并可以给我一个指针？

I am developing a 3.x based Eclipse RCP application. In the part of application, I am implementing Common-navigator plugin of Eclipse itself, in order to display resources in the workspace. I'have created the navigator view shown below:

But I would like display only one tree child element. More specifically, I only want clause folder and its elements to be shown.

What is the accurate way to do it?

我使用 C++ 程序自动生成这样的子句：

然后我需要用一些工具（比如 MiniSat）检查它们的可满足性，但是在将它们输入这样的工具之前，我需要在 DIMACS CNF 中转换它们，你知道有什么工具可以自动为我完成吗？

谢谢！

编辑：

非 CNF sat 求解器也可以正常工作！

我需要一个 SAT 求解器，它不仅可以将 CNF 文件作为输入，还可以将包含命题子句的普通 txt 文件（仅使用and or and not编写）作为输入。

我找不到任何东西。你能指出一个吗？

我在根据给定特征模型设计CNF（连接范式）文件时遇到了问题。例如，SPL 中有一个通用的特征模型。

• A、B、C 和 D是 4 个特征。
• B是A的强制子特征
• C和D是A的两个可选子功能。

如何编写上述约束的 CNF 文件？任何帮助表示赞赏！

也许 CNF 文件看起来像下面的形式，