SAT SMT
SAT
穷举算法
assign可理解为赋值，比如所有式子中共有变量1,2,3,4（反面形式是-1,-2,-3,-4），assign是完整的是指对于1,2,3,4所有变量都找到了true的情况（比如一组1,-2,-3,4）
优化1 : 冲突检测
不需要完整赋值就能知道结果
冲突：
算法：
优化2 : 赋值推导
赋值推导：出现部分赋值时，可以对其他地方的变量推出赋值
比如这里不用全赋值走一遍，就推出-1,-4都必须为false时，一定冲突，可以直接结束
标准推导方法：
Unit Propagation：其他文字都为假，剩下的一个文字必定为真
Unate Propagation：当一个子句存在为真的文字时，可以从子句集合中删 除
Pure Literal elimination：当一个变量只有为真或者为假的形式的时候，可以把 包含该变量的子句删除，比如始终都有-4，没用了，直接选择-4，{-4,6}，{-4,-6}
DPLL算法
优化3 ：变量选择
在上例中，优先选择最短子句里的变量，优先选择最常出现的变量（比如上例中选到变量1或2）
优化4：冲突导向的子句学习
CDCL：Conflict-Driven Clause Learning
在加入x7时发生冲突（x9必须为1又必须为0），找到推出x9相关的直接子结构，作为一个conflict加入conflict clause。
由于冲突记录，回到将x3=1的一步（x8是自动被推导为0），然后将x7置于0
CDCL算法
注意从新添加约束出发的推导实际保证了之前探过的冲突赋值不会出现
所以不再需要记录之前遍历过的赋值，每次任意选择剩下的变量和赋值即可，所以此时如果出现了空赋值（学习到了足够多的冲突，在已有的conflict clause中assign没有赋值可选了，全都会冲突），空赋值推出冲突意味着UNSAT
SMT
从SAT到SMT
Eager方法
将SMT问题编码成SAT问题
符号替代：A替代f(a)
引入布尔变量替代等式：P_{A=c}
为传递性添加约束
缺点：
很多理论存在专门的求解算法，编码成SAT之后，SAT求解器无法利用这些算法
模块化程度低，每种理论都要设计单独的编码方法，不同理论混合使用时要保证编码方法兼容
lazy方法
交互调用SAT求解器和其他各种理论求解器
理论求解器：
示例：
加入红色的{-1,2,4}相当于就是把原来的赋值禁掉了（不能同时出现）
优势：新的理论只需要实现公共接口就可以集成到SMT求解器中，模块化好
问题：
下例：
EUF求解器需要将它的信息传给SAT，也就是说在SAT的赋值推导步骤可以做更多事
于是需要给理论求解器添加接口函数
给理论求解器添加接口函数：
propagate
get_unsatisfiable_core
DPLL(T)
赋值推导和冲突检测()：每推一步做的其实就是这个的类似过程：
T求解器可以是EUF等等别的求解器
添加新约束：由于之前的赋值推导和冲突检测()返回false可能是因为T求解器，SAT本身并不知道哪里冲突了，在推到图上看不出冲突走到这里的原因。如果是这种情况，就走else分支
缺点：
即a=b与f(a)=f(b)需要丢给不同的solver求解，但是变量是共享的，可能有联系无法处理到
寻找接口属性：
Nelson-Oppen方法
理论性质要求：
给理论求解器添加接口方法：
具体处理详见ppt例子了
https://xiongyingfei.github.io/SA/2020/13_SMT.pdf p26