动机(Motivation) 主要目的是证明Formel的可实现(Erfüllbar) 一般的方法： 1.真值表 2.等价转化 但是随之Atom的数量增大，上述方法的效率则越加低。//真值表的数量将呈现指数增长 于是我们想到的方法就是非等价转化，比如用 P3代替P1∧P2 P_3 代替P_1 \land P_2 为了更好的了解algorithm，需要先看一下什么是范式，具体的algo