将数学陈述转换为SAT公式

Question

是可以编写一个数学陈述（例如goldbach的猜想，例如）作为非活动的3-sat公式，这是满足的，IFF的陈述是真的吗？IFF它是假的吗？IFF它与ZFC的公理无关？因此，对于任何陈述，您将拥有（最多）3个公式，只有一个可以满足的公式。此字段中是否有任何工作（您可以使用PythAgorean定理作为更简单的示例）？

Answer 1

如果您想知道是否存在一般方法/算法，它可以转换任何给定的数学陈述（由其指用逻辑编写的语句（说出一阶逻辑，二阶逻辑......等））到sat公式是真的 iff 该陈述是真的，那么答案是否定的。

是评估SAT公式是否为真或假的原因是可解除的（如果不快），则这些逻辑通常是 UNSCIVED 。因此，不存在这种算法。

当然，有逻辑可译码，并且可以通过特定算法将这些逻辑的声明转换为SAT公式（也可以像@ D.W的琐碎的字段）。请参阅： http://www.lsv.fr/~haase/documents/h18。pdf

Answer 2

取决于数学陈述。如果它有形式

$$ \在s_1 \ cdots中存在x_1 \ \存在于s_n中的x_n \。 \ varphi（x_1，\ dots，x_n）$$

其中 $ \ varphi（x_1，\ dots，x_n）$ 是 $ x_1，\ dots的某些条件， x_n $ 和 $ s_1，\ dots，s_n $ 是有限集，然后是是，它可以以直接的方式表示为3cnf公式。< / p> 但是，S_2中的S_1 \ forall y \中存在 $ \存在的语句。 \ varphi（x，y）$ 或 $ \存在x_1 \ in \ mathbb {r} \ cdots \存在x_n \ in \ mathbb {r}。 \ varphi（x_1，\ dots，x_n）$ 更难。

有一个琐碎的意义，答案是肯定的：每个数学陈述都是真或假的，所以它对应于3cnf公式 $ \ text {true} $ < / span>（即 $（x_1 \ lor \ neg x_1）$ ）或3cnf公式 $ \ text {false $ （即 $（x_1）\ land（\ neg x_1）$ ）。这种减少是非结构，但可能不是可计算的。

您可能对 https：//existential_theory_of_the_reals。

未定定是语言的属性，而不是数学陈述。也许你的意思是“独立于ZFC的原理”。