基于解析方法的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