基于解析方法的SAT求解器
HSE算法和软件设计离散数学课程中的家庭作业项目。 基于解析工具。
任务描述
给定2-CNF中的布尔公式,请使用解析方法确定是否可满足要求。 2-CNF的子句可以是以下两种形式之一:α\ /β或α->β,其中α和β是文字(p或〜p,其中p是变量)。 CNF以常用符号表示,例如:(p-> q)/ \(〜r \ / s)/ \(〜q-> p)
例
$ python hw_ply.py
input > (p -> q) /\ (~r \/ s) /\ (~q -> p)
Resolution: (~p\/q)/\(~r\/s)/\(q\/p)/\(None\/q)
Sat
1