基于符号模拟和变量划分的SAT算法

SAT Algorithm Based on Symbolic Simulation and Variable Partitions

针对SAT算法中回溯次数较多的问题,采用基于符号模拟和变量划分的方法来解决其不足。基于符号模拟和变量划分的SAT算法将一个较大的CNF分解为两个子集,每个子集所包含的变量又划分为两个互不相交的子集,仅对那些无法判断的子集,赋以符号值,从而限定了赋予符号值的变量范围,即可减少算法的回溯次数,又能降低内存占用率。理论及实验结果均证明,该算法是合理且有效的。

To solve the problem that SAT solvers usually has excessive backtraces during assigning binary values to an unassigned variables, a new SAT solver based on symbohc simulation and variable partition, which lower not only the number of backtrack but the memory blow-up, was presented. The SAT solver partitions a big CNF into two smaller subset A and B, then divides the set of variables into three disjoint set. Through the constraint that the symbolic values are only assigned to the variable in the set which occur in both A and B, the symbolic simulation-based SAT solver get both the low backtrack number and memory occupation. Experimental result showed the SAT solver is sound and efficient.