基本算法思想来源于DPLL算法,对于变元策略进行了改进。具体可以参考https://github.com/Billy1900/DPLL-Algorithm

DPLL算法思想如下:

Status DPLL( S) {
/* S为公式对应的子句集。若其满足,返回TURE;否则返回FALSE. */
while(S中存在单子句) { 
在S中选一个单子句L,并将单子句装入结果数组,value置为1;
依据单子句规则,利用L化简S;
if S = Φ return(TRUE);
else if (S中有空子句 ) return(FALSE);
}
对子句集中的所有变元出现次数进行排序,出现次数最多的选为最终的变元choose(次数统计规则--例:1和-1表示变元1出现了2次)
V = choose;
if DPLL(S ∪v )return(TURE);
return DPLL(S ∪¬v);
}

说明:优化算法相比DPLL算法 来讲,在选取变元策略上进行了优化。其余算法流程基本保持不变。

1)读取文件的路径在CreateClause函数中被写死,在文件的第58行,可以在此修改。

2)main函数中将文件名写死,在程序文件的第293行,可以在此做修改。