202404112103 DPLL algorithm for SAT solver

原始的DPLL在每一步选择一个变量并赋值（搜索树分支），然后应用Unit Propagation。当发现冲突时沿着搜索树回退，直到找到一个决策节点，其对应的变量的两种情况还没有被穷尽。

如果发现冲突时无法再回退，公式是不可满足的；如果所有变量都被赋值，则公式是可满足的，且unit clauses组成model。