自动推理笔记

命题逻辑（还记得我吗？）

命题公式

由若干布尔变量和运算符（$\neg, \cap, \cup, \rightarrow, \leftrightarrow$）得到的公式

有一些命题，我们能否从中得到另一个命题

将问题转化成更“正式”的问题

使用自动化程序解决“正式”的问题

 

通过形式化，可以将每个概念转化成符号

 

方法1：真值表证明该式为重言式，如果能证明是重言式，那么就能证明

但是，这个方法是O(2^n)的，虽然在这里还可以，但是如果n再大就不好用了

方法2：可满足式

一个式子是可满足的，如果其值可以为真

反之，如果其值恒为假，那么则不可满足

 如果一个式子是重言式，那么这个式子的否命题就是不可满足式

判定一个式子是否是可满足式的任务被称为SAT（short for satisfiability）

许多问题可以变成SAT，比如想要检测一个微处理器是否运作正常，可以用另一个微处理器与其比较，如果非(micro1<->micro2)不可满足

不过，所有已知的方法最差的情况下都是指数级的

鸽巢公式：一个不可满足公式，但想要证明公式本身不可满足比较困难

有n*(n+1)个布尔变量

设$C_n=\bigwedge_{j=1}^{n+1}(\bigvee_{i=1}^{n}P_{ij})$

$R_n=\bigwedge_{i=1...n, 1\leq j <k \leq n+1}(\neg P_{ij} \cup \neg P_{ik})$

$PF_n=C_n \cap R_n$

 

Same for disjunction

可以把上面的式子换成矩阵

 

于是，$C_n$的意思就是，对于第j列，至少有一项为真，而j从1至n，所以就是每一列都要有至少一项为真

所以至少有n+1项为真

而对于$R_n$的意思，对于第i行而言，每两个变量里至多有一个为真，所以n行最多有n个变量为真

而$PF_n$要求$C_n$和$R_n$都为真，这是不可能的。

鸽巢原理：如果有n+1个鸽子进了n个巢穴，至少有一个巢穴进了两个鸽子

注意到，所有的约束都是必须的，如果有一个约束被移除，那么式子就变成可满足式了

这里我们也看到了$C_n$是至少一个而$R_n$是至多一个，我们之后会经常用到。

使用计算机证明鸽巢式是很困难的

接下来我们会见识一种无关可满足性，常用自动推理解决的问题

模型验证：

 

如果二者为真，那么给二者赋假

问题：能否从全真到全假？

同样，类似的问题可能有很多状态，如果想要一个一个搜索过去会很困难

模型检测：

有有限个状态，有起始状态、转移方式，一些需要到达的状态，问是否能到达

程序检验：可能需要同时考虑多种状态转移，非确定性的状态

我们称初始状态的描述以及状态转移的描述为模型，因此检测一个模型是否具有某些性质就叫模型检验

将模型的描述形式化为符号，之后作检验的方法称为符号模型检验

自然，我们检验可以用SAT，但我们需要考虑更好的模型，这被称作重要的（Crucial）模型

SAT的解法：Z3、Yices

 一种基本的符号模型检测方法：Binary Decision Diagrams（二进制决策图），NuSMV。

并非所有命题都可以转化成命题逻辑，首先是SMT：Satisfiablity Modulo Theories，可满足性模型理论，这里主要研究线性不等式的理论，即变量不只是布尔，而是整数和实数

注意，SMT依然适用SAT的一些术语，比如说给整数赋值如果能满足，那么依然称为SAT

SMT-LIB语法

 

 

注意是语法使用的是前缀表达式，2*a=(* 2 a)

 

 

SMT可以转化成SAT解决

当然，还有比命题逻辑更难的逻辑，谓词逻辑

 不再限制域在数值上，而是在集合上

$\forall$ and $\exists$

等式逻辑

 基本上就是数理逻辑的完整部分了

模型逻辑/时序逻辑（temporal logic）

Computation Tree Logic，计算树逻辑

首先是命题逻辑

时间复杂性和空间复杂性

magnitude，规模

$f(n)=O(g(n))$

注意$\Omega$是指式子大于等于

SAT无线性时间

决策问题

决策问题是指你问一种事，回答你是或者否

P是指所有有多项式算法的决策问题，即在多项式时间内可以回答你问的事

引入证据（certificate，验证方法，中文常常称作解而且不这么说）一词

NP问题是指：

如果一个决策问题的正确结果是否，那么其一定没有可供验证的解

如果正确结果是真，那么我们可以在多项式时间内验证某个解是否符合要求

以SAT为例子，如果决策问题结果本身就绝对不可满足，那么自然不可能找到一个解，而如果可满足，那么才能多项式时间内验证

对于大部分问题这挺显然的，不过对于素数判定似乎有点问题，可以开学问老师

非确定性线性时间

很显然，P问题全都是NP问题

但是我们无法确定NP问题是否都是P问题

NP完全问题：如果有一个NP问题A，而且假设A也是P的，那么可以得到P=NP，那么称A为NP完全。或者也就是说所有NP问题可以归约到这个问题上

（注意，规约并不是双向的，考虑解二元一次方程和解一元一次方程，二元一次方程归约到一元一次方程是可能的，但反过来是不可能的）

SAT是NP完全的，因此许多其他问题也是NP完全的。此外，SAT可以规约到其他一切问题上，但反之则不可

由于NP完全问题存在，所以不太可能有P的

SAT是地基

一些典型NPC问题：走过所有点，是否有路径≤n？

这一问题与TSP密切相关（自我练习TSP<->SAT）

给一个无向图，是否存在一个哈密尔顿回路，经过每个点恰好一次？

给一些东西，能否将其分成两组，两组重量相同？

命题逻辑中的算数：二进制算术=命题逻辑算数

由于算数可以转化成二进制算术，而二进制算术可以使用SAT来考虑性质，所以我们可以将算术问题转化成SAT

 

乘法也可以做，不过考虑到乘法其实是加法的重复，所以可以重用加法，我们后面会进一步了解这方面的内容