python z3 解决 dpll 算法

主要思路是转化为SAT问题。在求解SAT问题之前，为了方便将原子命题进行替换。需要将原始命题转换为否定范式，然后再由否定范式转化为合取范式。这样就可以保证整个命题式中只有命题变量，~，∧，∨等符号。主要的实现方法是递归，但是在每一次递归中，我们如果之前对某个原子变量做了替换，就需要先对整个命题进行简化，比如原始命题为 p ∧ q，我们在前一次递归中，将p赋值为True，那么在下一次递归中，就需要通过简化，使得原始命题变成 q 。然后最新的命题中只剩下了原子命题q，我们可以对q进行取值，最终目的是使得整个命题成立。

以下代码主要参考此篇文章：
https://www.pythonf.cn/read/98943

import unittest
from typing import Listfrom z3 import *# In this problem, you will implement the DPLL algorithm as discussed
# in the class.# a utility class to represent the code you should fill in.
class Todo(Exception):def __init__(self, msg):self.msg = msgdef __str__(self):return self.msgdef __repr__(self):return self.__str__()########################################
# This bunch of code declare the syntax for the propositional logic, we
# repeat here:
'''
P ::= p| T| F| P /\ P| P \/ P| P -> P| ~P
'''class Prop:def __repr__(self):return self.__str__()class PropVar(Prop):def __init__(self, var):self.var = vardef __str__(self):return self.vardef __hash__(self):return hash(self.var)def __eq__(self, other):return other.__class__ == self.__class__ and self.var == other.varclass PropTrue(Prop):def __init__(self):passdef __str__(self):return "True"def __eq__(self, other):return other.__class__ == self.__class__class PropFalse(Prop):def __init__(self):passdef __str__(self):return "False"def __eq__(self, other):return other.__class__ == self.__class__class PropAnd(Prop):def __init__(self, left, right):self.left = leftself.right = rightdef __str__(self):return f"({self.left} /\\ {self.right})"class PropOr(Prop):def __init__(self, left, right):self.left = leftself.right = rightdef __str__(self):return f"({self.left} \\/ {self.right})"class PropImplies(Prop):def __init__(self, left, right):self.left = leftself.right = rightdef __str__(self):return f"({self.left} -> {self.right})"class PropNot(Prop):def __init__(self, p):self.p = pdef __str__(self):return f"~{self.p}"# we can convert the above defined syntax into Z3's representation, so
# that we can check it's validity easily:
def to_z3(prop):if isinstance(prop, PropVar):return Bool(prop.var)if isinstance(prop, PropImplies):return Implies(to_z3(prop.left), to_z3(prop.right))if isinstance(prop, PropTrue):return Trueif isinstance(prop, PropFalse):return Falseif isinstance(prop, PropAnd):return And(to_z3(prop.left), to_z3(prop.right))if isinstance(prop, PropOr):return Or(to_z3(prop.left), to_z3(prop.right))if isinstance(prop, PropNot):return Not(to_z3(prop.p))#####################
# TODO: please implement the nnf(), cnf() and dpll() algorithm, as discussed
# in the class.
#转换成否定范式
def nnf(prop: Prop) -> Prop:# 如果含有"->"if isinstance(prop, PropImplies):return PropOr(PropNot(nnf(prop.left)), nnf(prop.right))# 如果含有Andif isinstance(prop, PropAnd):return PropAnd(nnf(prop.left), nnf(prop.right))# 如果含有Orif isinstance(prop, PropOr):return PropOr(nnf(prop.left), nnf(prop.right))# 如果含有Notif isinstance(prop, PropNot):if isinstance(prop.p, PropVar):return PropNot(nnf(prop.p))if isinstance(prop.p, PropNot):return nnf(prop.p.p)if isinstance(prop.p, PropTrue):return PropFalse()if isinstance(prop.p, PropFalse):return PropTrue()if isinstance(prop.p, PropOr):return PropAnd(nnf(PropNot(prop.p.left)), nnf(PropNot(prop.p.right)))if isinstance(prop.p, PropAnd):return PropOr(nnf(PropNot(prop.p.left)), nnf(PropNot(prop.p.right)))if isinstance(prop.p, PropImplies):return PropAnd(nnf(prop.p.left), nnf(PropNot(prop.p.right)))# 对于命题变量，true，false，直接返回return propdef is_atom(nnf_prop: Prop) -> bool:if isinstance(nnf_prop, PropOr) or isinstance(nnf_prop, PropAnd):return Falsereturn Truedef cnf(nnf_prop: Prop) -> Prop:def cnf_d(left: Prop, right: Prop) -> Prop:if isinstance(left, PropAnd):return PropAnd(cnf_d(left.left, right), cnf_d(left.right, right))if isinstance(right, PropAnd):return PropAnd(cnf_d(left, right.left), cnf_d(left, right.right))return PropOr(left, right)if isinstance(nnf_prop, PropAnd):return PropAnd(cnf(nnf_prop.left), cnf(nnf_prop.right))if isinstance(nnf_prop, PropOr):return cnf_d(cnf(nnf_prop.left), cnf(nnf_prop.right))if isinstance(nnf_prop, PropVar):return nnf_propif isinstance(nnf_prop, PropNot):return PropNot(nnf_prop.p)def flatten(cnf_prop: Prop) -> List[List[Prop]]:"""Flatten CNF Propositions to nested list structure .The CNF Propositions generated by `cnf` method is AST.This method can flatten the AST to a nested list of Props.For example: "((~p1 \\/ ~p3) /\\ (~p1 \\/ p4))" can betransfer to "[[~p1, ~p3], [~p1, p4]]".Parameters----------cnf_prop : PropCNF Propositions generated by `cnf` method.Returns-------List[List[Prop]A nested list of Props, first level lists are connected by `And`,and second level lists is connected by `Or`."""def get_atom_from_disjunction(prop: Prop) -> List[Prop]:if is_atom(prop):return [prop]if isinstance(prop, PropOr):return get_atom_from_disjunction(prop.left) + get_atom_from_disjunction(prop.right)if isinstance(cnf_prop, PropAnd):return flatten(cnf_prop.left) + flatten(cnf_prop.right)elif isinstance(cnf_prop, PropOr):return [get_atom_from_disjunction(cnf_prop)]elif is_atom(cnf_prop):return [[cnf_prop]]def dpll(prop: Prop) -> dict:result = dict()flatten_cnf = flatten(cnf(nnf(prop)))#初始化字典for props in flatten_cnf:for pp in props:if isinstance(pp, PropVar):result[pp.var] = Falseif isinstance(pp, PropNot):result[pp.p.var] = False# implement the dpll algorithm we've discussed in the lecture# you can deal with flattened cnf which generated by `flatten` method for convenience,# or, as another choice, you can process the original cnf destructure generated by `cnf` method## your implementation should output the result as dict like :# {"p1": True, "p2": False, "p3": False, "p4": True} if there is solution;# output "unsat" if there is no solution## feel free to add new method.# 挑选原子命题def select_atomic(prop: Prop) -> Prop:if isinstance(prop, PropVar):return propif isinstance(prop, PropAnd) or isinstance(prop, PropOr):if not isinstance(select_atomic(prop.left), PropTrue) and not isinstance(select_atomic(prop.left),PropFalse):return select_atomic(prop.left)if not isinstance(select_atomic(prop.right), PropTrue) and not isinstance(select_atomic(prop.right),PropFalse):return select_atomic(prop.right)if isinstance(prop, PropNot):return select_atomic(prop.p)# 简化命题，比如已经用某个命题中的原子命题已经被赋值，那么就可以简化该命题，直接返回，或进行下一轮的原子命题替换def unitProp(prop):if isinstance(prop, PropTrue) or isinstance(prop, PropFalse) or isinstance(prop, PropVar):return propif isinstance(prop, PropAnd):if isinstance(prop.left, PropFalse) or isinstance(prop.right, PropFalse):return PropFalse()elif isinstance(prop.left, PropTrue):return unitProp(prop.right)elif isinstance(prop.right, PropTrue):return unitProp(prop.left)else:return PropAnd(unitProp(prop.left), unitProp(prop.right))if isinstance(prop, PropOr):if isinstance(prop, PropTrue) or isinstance(prop, PropTrue):return PropTrue()elif isinstance(prop.left, PropFalse):return unitProp(prop.right)elif isinstance(prop.right, PropFalse):return unitProp(prop.left)else:return PropOr(unitProp(prop.left), unitProp(prop.right))if isinstance(prop, PropNot):if isinstance(prop, PropTrue):return PropFalse()if isinstance(prop, PropFalse):return PropTrue()else:return prop# 将原子命题替换为某个值def set_var_value(prop: Prop, x: Prop, value: PropTrue or PropFalse):if isinstance(prop, PropVar):if prop.var == x.var:return valueif isinstance(prop, PropNot):prop.p = set_var_value(prop.p, x, value)if isinstance(prop.p, PropTrue):return PropFalse()if isinstance(prop.p, PropFalse):return PropTrue()if isinstance(prop, PropOr):prop.left = set_var_value(prop.left, x, value)prop.right = set_var_value(prop.right, x, value)if isinstance(prop.left, PropTrue) or isinstance(prop.right, PropTrue):return PropTrue()if isinstance(prop.left, PropFalse):return prop.rightif isinstance(prop.right, PropFalse):return prop.leftif isinstance(prop, PropAnd):prop.left = set_var_value(prop.left, x, value)prop.right = set_var_value(prop.right, x, value)if isinstance(prop.left, PropFalse) or isinstance(prop.right, PropFalse):return PropFalse()if isinstance(prop.left, PropTrue):return prop.rightif isinstance(prop.right, PropTrue):return prop.leftreturn prop# 对命题进行拷贝，用于回溯def copy(prop):if isinstance(prop, PropVar):return PropVar(prop.var)if isinstance(prop, PropAnd):return PropAnd(copy(prop.left), copy(prop.right))if isinstance(prop, PropOr):return PropOr(copy(prop.left), copy(prop.right))if isinstance(prop, PropNot):return PropNot(copy(prop.p))def dpll1(prop: Prop, assignment: Prop) -> Prop:#实际使用中，unitProp()可以注释掉，因为该功能被包含在了set_var_value()中unitProp(prop)if isinstance(prop, PropTrue):return propelif isinstance(prop, PropFalse):return propp = select_atomic(prop)if p is None:return propif isinstance(assignment, PropTrue):result[p.var] = Trueelif isinstance(assignment, PropFalse):result[p.var] = Falseprop = set_var_value(prop, p, assignment)prop_copy = copy(prop)if isinstance(dpll1(prop, PropTrue()), PropTrue):return PropTrue()return dpll1(prop_copy, PropFalse())newProp = cnf(nnf(prop))dpll1(newProp, PropTrue())print(result)return result#####################
# test cases:# p -> (q -> ~p)
test_prop_1 = PropImplies(PropVar('p'), PropImplies(PropVar('q'), PropVar('p')))# ~((p1 \/ ~p2) /\ (p3 \/ ~p4))
test_prop_2 = PropNot(PropAnd(PropOr(PropVar("p1"), PropNot(PropVar("p2"))),PropOr(PropVar("p3"), PropNot(PropVar("p4")))
))# #####################
class TestDpll(unittest.TestCase):def test_to_z3_1(self):self.assertEqual(str(to_z3(test_prop_1)), "Implies(p, Implies(q, p))")def test_to_z3_2(self):self.assertEqual(str(to_z3(test_prop_2)), "Not(And(Or(p1, Not(p2)), Or(p3, Not(p4))))")def test_nnf_1(self):self.assertEqual(str(nnf(test_prop_1)), "(~p \\/ (~q \\/ p))")def test_nnf_2(self):self.assertEqual(str(nnf(test_prop_2)), "((~p1 /\\ p2) \\/ (~p3 /\\ p4))")def test_cnf_1(self):self.assertEqual(str(cnf(nnf(test_prop_1))), "(~p \\/ (~q \\/ p))")def test_cnf_2(self):self.assertEqual(str(cnf(nnf(test_prop_2))),"(((~p1 \\/ ~p3) /\\ (~p1 \\/ p4)) /\\ ((p2 \\/ ~p3) /\\ (p2 \\/ p4)))")def test_cnf_flatten_1(self):self.assertEqual(str(flatten(cnf(nnf(test_prop_1)))), "[[~p, ~q, p]]")def test_cnf_flatten_2(self):self.assertEqual(str(flatten(cnf(nnf(test_prop_2)))),"[[~p1, ~p3], [~p1, p4], [p2, ~p3], [p2, p4]]")def test_dpll_1(self):s = Solver()res = dpll(test_prop_1)self.assertEqual(str(s.check()), "sat")s.add(Not(Implies(res["p"], Implies(res["q"], res["p"]))))self.assertEqual(str(s.check()), "unsat")def test_dpll_2(self):s = Solver()res = dpll(test_prop_2)s.add(Not(Not(And(Or(res["p1"], Not(res["p2"])), Or(res["p3"], Not(res["p4"]))))))self.assertEqual(str(s.check()), "unsat")if __name__ == '__main__':unittest.main()

本文来自互联网用户投稿，文章观点仅代表作者本人，不代表本站立场，不承担相关法律责任。如若转载，请注明出处。 如若内容造成侵权/违法违规/事实不符，请点击【内容举报】进行投诉反馈！