自动推理 | Rye Land

合取范式

A formula that is a multiary conjunction of multiary disjunctions of literals is in conjunctive normal form (CNF).

Formulae in CNF allow easy checks of validity which avoid times exponential in the number of their atoms. ⇒ A literal is either an atom, p, or the negation of an atom.

它的每个子句是一个析取（OR, ∨）的集合，整个公式是这些子句的合取（AND, ∧）。

CNF Conversion

💡

The CNF conversion in previous slide is too expensive. There is a linear time translation to CNF that produces an equisatisfiable formula. Idea: introduce a new variable during the translation

霍恩子句

特殊的 CNF，每个子句最多只有一个未被否定的变量。例如：

Transforming a propositional logic formulae into CNF can be expensive. Formulae in CNF can be easily checked syntactically for validity but testing satisfiability is difficult. Horn clauses are a subclass of formulae that have much more efficient ways of deciding their satisfiability.

A Horn formula is a formula φ of propositional logic if it can be generated as an instance of H in the following grammar:

means false, means true

We call each instance of C a Horn clause. Horn formulae are conjunctions of Horn clauses .

其他范式

否定范式

A formula where negation is applied only to propositional atoms is said to be in Negation Normal Form (NNF).

否定运算符（¬）仅直接作用于变量，而不是子公式，没有其他的逻辑连接词被否定。

或 ❌

✔️

析取范式

A formula that is a multiary disjunction of multiary conjunctions of literals is in disjunctive normal form (DNF).

它的每个子句是一个合取（AND, ∧）连接的文字（即变量或其否定）集合，整个公式是这些子句的析取（OR, ∨）连接。

🔑

有几个完整的方案，每个方案里有一些必须全部完成的步骤。只需要从这几个方案中选择一个方案成功执行，大任务就算成功。

E.g.,

Step 1: Distribute the conjunction over the disjunction

Step 2: Convert each subformula into a clause

Step 3: Simplify the contradiction p ∧ ¬p (which is always false)

SAT 求解器

SAT 问题

布尔可满足性问题，Boolean Satisfiability Problem，确定是否存在一种变量的真假赋值方式，使得一个给定的布尔表达式为真。

SAT 问题即考虑：表达式 (A OR B) AND (NOT A OR C) 是否存在A、B、C的取值方式，使得整个表达式为真？

答案是：存在。因为如果 A 为假，B 为真，C 为真，整个表达式的值就为真。

DIMACS 格式

一个广泛采用的标准文本文件格式，SAT 求解器通常可以读取这种格式的文件，然后尝试找到满足所有子句的变量赋值，从而解决 SAT 问题。

例，，使用DIMACS格式，它将被编码如下：

c 使用了 3 个变量，有 2 个子句

注释行： 以字符 c 开头

问题行： 以字符 p 开头，后面跟着字符串 cnf，然后是变量的数量和子句的数量。

子句行： 列出每个子句中的文字（正整数表示变量，负整数表示变量的否定）。每个子句以0结尾。

DPLL 算法

(Davis-Putnam-Loveland-Logemann) The main framework behind most of SAT solvers: traversing and backtracking on a binary tree.

基于以下几个核心概念：

单位传播（Unit Propagation）：如果一个子句中除了一个变量以外的所有变量都已经被赋值为假，那么这个未赋值的变量必须赋值为真，以使得这个子句为真。

纯文字规则（Pure Literal Elimination）：如果一个变量在所有出现的地方都具有相同的真值（都是正的或负），那么可以安全地为这个变量赋值，使得所有包含这个变量的子句都为真。

分支规则（Branching Rule）：当无法通过单位传播和纯文字规则进一步推进时，算法选择一个变量并赋予一个真值（通常是先试真，然后试假），然后继续处理。

递归试错：算法会递归地尝试为变量赋值，然后检查是否有子句可以得到满足。如果所有子句都得到满足，那么算法成功；如果某个子句因为当前的赋值而无法得到满足，则回溯并尝试另一种赋值。

例

🔓

假设 = true

SMT 求解器

Satisfiability Modulo Theories (SMT) 是对 SAT 问题的扩展，它考虑布尔公式的结构的同时，还要进一步考虑公式中包含的变量和函数的某些背景理论的约束。

表达式不仅要满足逻辑上的合理性（AND、OR、NOT）而且还要满足算术上的约束（x + y > 5等）。

SMT2

SMT-Lib Version 2.0 (SMT2) is the latest standard for all SMT solvers.

Z3

Z3 (Microsoft Research Project) is winning almost every single category in the SMT solver competition . But sometime it is timed out badly.