SAT DPLL——Optimized

SAT问题即命题逻辑公式的可满足性问题(satisfiability problem),是计算机科学与人工智能基本问题,是一个典型的NP完全问题,可广泛应用于许多实际问题如硬件设计、安全协议验证等,具有重要理论意义与应用价值。本设计要求基于DPLL算法实现一个完备SAT求解器,对输入的CNF范式算例文件,解析并建立其内部表示;精心设计问题中变元、文字、子句、公式等有效的物理存储结构以及一定的分支变元处理策略,使求解器具有优化的执行性能;对一定规模的算例能有效求解,输出与文件保存求解结果,统计求解时间。