SATSMTZ3和符号执行
Posted 白马负金羁
tags:
篇首语：本文由小常识网(cha138.com)小编为大家整理，主要介绍了SATSMTZ3和符号执行相关的知识，希望对你有一定的参考价值。
符号执行（symbolic execution）是一种计算机科学领域的程序分析技术，通过采用抽象的符号代替精确值作为程序输入变量，得出每个路径抽象的输出结果。 这一技术在软件测试中有很重要的应用，能够有效地发现程序中的漏洞。本专栏中前面已经介绍过在angr中使用符号执行来解决CTF题目的例子。本文要更进一步地探讨其背后的一些知识。
一、SAT
SAT在计算理论中是非常重要的一个问题（参见【1】）。我们都知道布尔公式（Boolean formula）是包含布尔变量和运算的表达式。例如
就是一个布尔公式。如果对变量的某个0、1赋值使得一个公式的值等于1，则该公式是可满足的（satisfiable）。上面的布尔公式是可满足的，因为当
，
，
时，公式的计算结果就是1
以上是关于SATSMTZ3和符号执行的主要内容，如果未能解决你的问题，请参考以下文章