问题标签 [sat]

我想构建一个模块/应用程序，将 .SAT 格式转换为 .3mf 之类的 3D 打印文件格式，并且我希望它建立在 ACIS 内核上，以便我可以使用预定义的函数和...

我可以访问 ACIS 内核源代码，但我不知道从哪里开始。我知道他们有一个名为 RADF 的框架，但我不确定它是否能帮助我实现我想要的。

我的问题非常基本，但如果你能回答，我真的很感激。

1. 完全基于内核构建应用程序意味着什么？假设我正在使用 VS、C# 编程语言并且我有 ACIS 内核源代码。我是否必须在 VS 中启动一个新项目并向其中添加 ACIS 库才能使用它的功能？我真的需要一个好的和翔实的答案，所以提前谢谢你！

2. RADF 在这种情况下会做什么？我需要它吗？如果我想用C#，有必要吗？（因为ACIS是用C++写的）

3. 如果上一个问题的答案是肯定的，我真的需要一些帮助来构建 RADF 和 SPADotnet 解决方案。如果有人有这方面的经验，我可以提问。

4. 正如我所说，我希望我的应用程序的输出是 .3mf 文件，这是否意味着我必须使用由联盟开发的 .3mf 源代码？（在 GitHub 上的那个）

最后我想说的是，我真的很想通过在线阅读文档和其他东西来学习这些东西，但我就是找不到答案

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

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

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

在将弧一致性（AC3）算法应用于一个约束满足问题中，如果一个变量的域为空，下一步是什么？

解决方案（4）。我认为（1）是正确的，因为这意味着我们找不到任何一致的分配并停止。任何人都可以描述为什么（4）是真的？

我正在研究 minisat 的来源，这里有一个跟随内联函数

哪个recibes作为输入一个整数var（DIMAC文件的一个整数）并返回一个文字p，我不明白为什么var加上var然后加上符号？你能帮忙理解一下吗？

有没有办法在 Z3 中表达假设（我正在使用 Z3Py 库），这样引擎不会检查它们的有效性，而是将它们作为基础理论，就像在定理证明中一样？

例如，假设我有两个参数类型为 Real 的一元函数。我想告诉 Z3 引擎，对于所有输入值，f1(t) 等于 f2(t)。

在 Z3Py 中编码如下所示：
t = Real("t")
假设 1 = ForAll(t, f1(t) = f2(t))。

所呈现代码的问题是我的断言集非常大并且我使用量词（我试图证明实时系统的可满足性）。如果我将上述断言添加到其他断言集中，则检查过程不会终止。

我正在编写一个需要在模型上调用 Alloy 并在返回的实例上执行某些操作的程序。问题是每次调用Alloy命令时都会打开Alloy接口。我想知道是否无论如何我们都可以在不打开接口的情况下从 Java 代码调用 Alloy。

只需使用加法、减法和移位就可以将两个数字相乘。该过程的重要部分是找到此类操作的最小（最佳）序列。使用蛮力找到序列会导致难度呈指数增长，因此使用了各种启发式方法，也许最常见的是Robert Bernstein的论文乘以整数常数。

乘以 113 的示例，如Vincent Lefevre的乘以整数常数中所述：

我偶然发现了一个非常有趣的答案，这让我想知道：是否可以使用 Z3（或类似的）来找到将数字乘以给定常数的最小运算符序列？我对所有这些 SAT 和 SMT 都很陌生，所以我不确定它在布尔可满足性问题的背景下是否有意义？

据我了解，增量 SAT 求解有助于评估彼此非常接近的不同模型。

我想用它来评估模型，如果我稍后更改它，使用以前的解决方案再次重新评估它以获得更快的结果。然而，在研究了各种 SAT 求解器（Sat4J、Minisat、mathsat5）之后，似乎它们只能在一次运行中呈现所有模型时才能增量求解。

我对SAT解决很陌生，所以我可能会忽略一些东西。有没有办法保存解决实例供以后使用？关闭实例会丢失所有学习内容吗？

定义 SAT2016 = {\phi | \phi 是一个 CNF 公式，最多有 2016 个子句}。假设 P \neq NP，SAT2016 NP-complete 吗？

由于每个子句中的文字数量没有限制，因此尚不清楚是否存在多项式时间算法来检查具有恒定子句数量限制的公式的可满足性。

欢迎您的想法。

在java中，我有一组相互连接的对象。让我们假设它们在一起是一些模型，让我们这样称呼它。

我想根据一些规范（定义为一组条件）验证该模型。条件可能是这样的：

可以有很多这样的条件，并且必须满足所有这些条件才能说模型符合规范。所有的条件都是一些由变量和逻辑表达式组成的谓词，我想处理的是 SAT 问题的一个实例。

我不关心该解决方案的复杂性，我只想使用 Prolog 来执行查找适当的变量替换（如果存在，则意味着模型符合规范）。

我正在寻找一种如何轻松创建 Prolog 知识库的方法，该知识库将由代表创建我的模型的对象的语句组成。

你有什么值得推荐的吗？或者，也许您可​​以建议一些其他方法来解决该问题？