计算机数理逻辑-一阶逻辑-SMT

2022-03-10

1. SAT vs SMT 布尔可满足性问题 vs 可满足性模理论

SMT将SAT推广到涉及实数、整数和/或各种数据结构（如列表、数组、位向量和字符串
由于布尔可满足性已经是 NP 完全的，所以 SMT 问题通常是 NP困难的，并且对于许多理论来说它是不可判定(nondeterministic)

SMT是指另外一类公式的可满足性判定问题。这一类公式具有两个特点：

在命题逻辑公式里面混入了一些一阶逻辑表达式
具有任意的布尔结构

SAT solvers are automatic and efficient
However, systems are usually designed and modeled at a higher level than the Boolean level and the translation to Boolean logic can be expensive. A primary goal of research in Satisfiability Modulo Theories (SMT) is to create verification engines that can reason natively at a higher level of abstraction, while still retaining the speed and automation of today’s Boolean engines

SMT Solver = SAT Solver + Theory Solver

2. Solver vs Checker

In model checking, you have a model and a specification (or property), and you check if the model meets the specification.
In SAT solving, you have a formula and you try to find a satisfying assignment to it.

To perform model checking a reachability analysis is needed and to do this the program transitions are often executed symbolically
The solution to the resulting satisfaction problem is created by a solver

3. overflow 溢出

3.1. arithmetic overflow 算术溢出

当计算产生出来的结果是非常大的，大于寄存器或存储器所能存储或表示的能力限制
任何数除以零的计算（Divided by zero）“不是”算术溢出的一种。在数学上只能明显算是不明确的定义（Undefined）；它计算出来的结果只能当成是“没有”值，而不是非常大的无限数值

3.2. arithmetic underflow算术下溢

算术下溢也称为浮点数下溢，是指计算机浮点数计算的结果小于可以表示的最小数
例如，浮点数指数范围为-128至127，一个绝对值小于2−127的浮点数就会造成下溢（假设-128的阶码用于表示负无穷）

4. Theory 理论

A theory T is a consistent一致的 set of first-order formulas
- Equality (also called theory of uninterpreted functions UF
- Linear arithmetic
- Arrays
- …

4.1. 一致性（consistency)

指一个形式系统中不蕴涵矛盾
- 语义上：当一个命题S是由许多命题组成时，如果所有命题可同时为真，则S是一致的，否则S是不一致的
- 语法上：公理系统不能推导出两个相反的结果。亦即不存在命题P，使得P→Q和P→~Q同时成立

4.2. Validity modulo theories 有效性模式理论

$T_1∪T_2∪…∪T_n \models{} ∀\bar{x}F(\bar{x})$
here each $T_i$ is a first-order theory and $F(\bar{x})$ is a quantifier-free formule

$\simeq{}$ 大概是指logical equivalence
- 非反常识的，可以用常识来理解

4.3. Satisfiability Modulo Theories 可满足性模式理论

From Validity Modulo Theories to Satisfiability Modulo Theories:

4.4. SMT solvers

5. Theory of equality (QF_UF and UF)

QF是指quantifier-free

Function congruence: 函数同构
- 差不多相当于双射？

issue

Equality axioms are very prolific多产的, resolution will quickly generate many irrelevant clauses.
Resolving with symmetry axiom we can produce all permutations of left and right sides of all equations. Transitivity axiom can resolve with symmetry axioms and itself producing longer clauses.

5.1. Inference rules

Paramodulation: 调节

example

Idea: Only replace “bigger” terms by “smaller” terms
注意第七步不是 $f(b)=f(b)$ ，不要马虎

5.2. Uninterpreted function

In mathematical logic, an uninterpreted function or function symbol is one that has no other property than its name and n-ary form. Function symbols are used, together with constants and variables, to form terms.
- 相当于单纯0-ary符号$f$
The theory of uninterpreted functions is also sometimes called the free theory, because it is freely generated, and thus a free object
- 不被量词约束的

6. Theory of Arrays

Array signature $Σarray =< { select/2, store/3 } , { \simeq{}} >$

6.1. Axioms公理

$∀A, I , E [select(store(A, I , E ), I ) \simeq{} E ]$
- if we store an element in an array and read from the same position then we should obtain the same element
- 注意store的返回值是一个新的Array
$∀A, I , J, E [I \not\simeq{} J → select(store(A, I , E ), J) \simeq{} select(A, J)]$
- if we store an element at position i then at all other positions elements are unchanged