【软件分析课程11讲-学习笔记】布尔可满足性SAT

前言

创作开始时间：2022年11月16日15:59:22

如题，学习一下布尔可满足性SAT的相关知识。参考：熊英飞老师2018《软件分析》课件。

正文

路径敏感性

流敏感（flow-sensitive）：考虑程序语句执行的顺序
路径敏感（path-sensitive）：依据条件分支语句的不同谓词，计算不同的分析信息
上下文敏感（context-sensitive）：过程间分析（Interprocedural Analysis）时，考虑函数调用的上下文信息。

• 几个基本概念辨析：流敏感，路径敏感和上下文敏感 https://blog.csdn.net/qysh123/article/details/17789285

例子：

int f(int x){
	if (x > 5)
	x = 10;
	return x;
}
1
2
3
4
5

假设输入区间为(5, 10]
不考虑路径敏感时，分析得到的函数返回值：(5, 10]
考虑路径敏感时，分析得到的函数返回值：[10, 10]

约束求解

约束求解：给定一组约束，求这组约束是否可满足。
SMT包含：SAT、Linear、Array、String四个solver

局限：1）速度慢；2）算法发展分散，各自只能解小部分约束。

SAT问题：最早被证明的 NP 完全问题之一（1971）
文字literal：变量
子句clause：文字的析取（或）
布尔赋值：变量到布尔值上的映射
合取范式：子句的合取（且）

SAT问题：子句集上的约束求解问题。给定一组子句，寻找一组布尔赋值，使得所有子句为真。通常通过合取范式定义。

任何命题逻辑公式可以表达为合取范式，SAT问题可以求解任何命题逻辑公式。

SAT基本求解算法

• 穷举法：优化方法（冲突检测、赋值推导）
• 标准推导方法

小结

先学到这里，后续再更新。

创作结束时间：2022年11月16日16:18:18