Sat
SAT问题¶
子句集合上的约束求解问题
- literal 变量或者变量的取反 如$ x\ and\ \neg x $
- 把literl 析取
- 给变量赋布尔值
给定一组子句，寻找一个布尔值，使得所有子句为真
SAT是回答命题逻辑的可满足性问题（命题P 逻辑连接词）
SMT是回答一阶理论的可满足性问题 一阶理论是对命题逻辑的扩充 量词：
一阶逻辑引入了全称量词 (∀，代表"对于所有") 和存在量词 (∃，代表"存在")，允许引入变量，并表达关于对象集合的泛化和特例化。 量词使得我们能够表达像 "对于所有人，都存在一个朋友" 或 "存在一个人，他是所有人的朋友" 这样的陈述。 变量：
一阶逻辑引入了变量，这允许我们使用符号（通常用字母表示）来代表对象，而不仅仅是命题。 变量可以与量词一起使用，使得我们可以泛化命题，而不必具体指定对象。 谓词：
谓词在一阶逻辑中变得更加灵活，可以接受变量作为参数。例如，P(x) 可以表示 "x是红色的"，其中 x 是一个变量。 一阶逻辑的谓词允许我们更好地表达关于对象和其性质的信息。 函数：
一阶逻辑引入了函数符号，允许我们表示对象之间的关系，而不仅仅是命题之间的关系。 函数可以接受变量作为参数，并产生一个结果。例如，f(x) 可以表示一个将 x 映射到某个值的函数。 复杂的句法结构： P F的不同点 命题1：存在一个人，他是成年人。
表达式：∃x P(x) 命题2：存在一个人，他的年龄加1等于18。
表达式：∃x (F(x) = 18)
即 谓词 V到T|F的映射 函数 V到V'的映射 允许把谓词和函数放在量词后的就是高阶逻辑