形式化方法—作业3—Z3求解SAT问题

一.背景

  课程主页: Formal Methods Foundation
  作业地址: Formal Methods Assignment3
  如果您的英文足够好,请直接点击上述链接查看相关信息
  由于课程结束上述链接失效, 请点击此处Wolai课程链接查看相关资料。

二.作业

 2.1 基本命题逻辑

  在Z3中,我们可以将两个命题声明为布尔值,这是相当自然的,因为命题可以具有真值或假值。声明两个命题P和Q:
    P = Bool('P')
    Q = Bool('Q')
  或者,我们可以进行批量声明:
    P, Q = Bools('P Q')

  使用连接词构建命题:
  Z3 支持连接词:/\(And)、 /(Or)、 ~(Not)、 ->(Implies)以及其他几个连接词。我们可以通过直接编写Lisp风格的抽象语法树来构建命题,例如,析取:P \/ Q(注意\/在Z3中称为Or)可以编码为以下AST:
    F = Or(P, Q)

  求解的过程:
  示例 A-1:Z3最简单的用法是直接将命题送到Z3求解器中,以检查满足性,这可以通过调用solve()函数来完成,solve()函数将创建一个求解器的实例,检查命题的可满足性,如果该命题是可满足的,则输出一个模型,代码如下所示:
    F = Or(P, Q)
    solve(F)
  对于上面调用Z3求解器的情况,Z3 将输出如下内容:
    [P=True, Q=False]
  这是一个对命题P和Q赋值的模型,它使命题F可以满足。显然,这只是几种可能的模型之一。

  示例 A-2:并非所有命题都是可以满足的,请考虑以下命题:
    F = And(P, Not(P))
    solve(F)
  Z3 将输出:
    no solution
  这表明命题F不满足,也就是说,命题F对于P的任何可能值都无法为真。

  获取更多可能的解决方案:
  考虑前面的示例A-1:
    F = Or(P, Q)
    solve(F)
  默认情况下,Z3 仅输出真值表中的第一行:


P    Q    P\/Q
-----------------
t    t     t
t    f     t
f    t     t
f    f     f

  毕竟,我们问Z3的是命题的满足性,所以一排情况就足够了。如果我们希望 Z3 输出所有使命题可满足的赋值情况,而不仅仅是第一行,那该怎么办?对于上面的示例,我们需要前3行的所有情况。方法是:当我们得到答案时,我们否定答案,与原始命题结合,然后再次检查模型即可。对于上面的例子:

	F = Or(P, Q)
	solve(F)   #此时输出[P=True, Q=False]
	F = And(F, Not(And(P, Not(Q))))
	solve(F)   #此时输出[P=False, Q=True]
	F = And(F, Not(And(Not(P), Q)))
	solve(F)   #此时输出[P=True, Q=True]
	F = And(F, Not(And(P, Q)))
	solve(F)   #此时输出no  solution代表已经无解

  Exercise 1-1: 求解以下命题的满足性

(P /\ Q) \/ R
P, Q, R =Bools('P Q R')  # 声明变量
F = Or((And(P, Q)), R)   # 生成表达式
solve(F)
# Z3 output this:"[R = False, Q = True, P = True]"

  Exercise 1-2: 求解以下命题的满足性

P \/ (Q \/ R)
P, Q, R =Bools('P Q R') 
F = Or(P,Or(Or(Q, R)))
solve(F)
# Z3 output this:"[R = False, Q = False, P = True]"

  Exercise 1-3: 求解以下命题的满足性

(P \/ Q) /\ (Q /\ R) /\ (P /\ ~R)
P, Q, R = Bools('P Q R') 
S = And(P, Not(R))
M = And(Q, R)
N = Or(P, Q)
F = And(N, And(M, S))
solve(F)
# Z3 output this: "no solution"

  Exercise 1-4: 求解以下命题的满足性

(P /\ ~S /\ R) /\ (R /\ ( ~P \/ (S /\ ~Q)))
P, Q, R, S = Bools('P Q R S')
# P /\ ~S /\ R
A = And(Not(S), R)
B = And(P, A)
# R /\ ( ~P \/ (S /\ ~Q))
C = And(S, Not(Q))
D = Or(Not(P), C)
E = And(R, D)
# result
F = And(B, E)
solve(F)
# Z3 output this: "no solution"

  Exercise 1-5: 输出以下命题的所有解

(P /\ Q) \/ R
P, Q, R = Bools('P Q R')
F = Or(And(P, Q), R)
solve(F)
# Z3 outputs:[P = True, Q = True, R = False]

F = And(F, Not(And(P, Q, Not(R))))
solve(F)
# Z3 outputs:[P = True, Q = True, R = True]

F = And(F, Not(And(P, Q, R)))
solve(F)
# Z3 outputs:[P = False, Q = False, R = True]

F = And(F, Not(And(Not(P), Not(Q), R)))
solve(F)
# Z3 outputs:[P = True, Q = False, R = True]

F = And(F, Not(And(P, Not(Q), R)))
solve(F)
# Z3 outputs:[P = False, Q = True, R = True]

F = And(F, Not(And(Not(P), Q, R)))
solve(F)
# Z3 outputs:
#   [R = False, Q = True, P = True]
#   [R = True, Q = True, P = True]
#   [R = True, Q = False, P = False]
#   [R = True, Q = False, P = True]
#   [R = True, Q = True, P = False]
#   no soluiton

  Exercise 1-6: 编写函数输出任意命题的所有解

def sat_all(props, f):
    """Get all solutions of given proposition set props that satisfy f

    Arguments:
        props {BoolRef} -- Proposition list
        f {Boolref} -- logical express that consist of props
    """
    solver = Solver()
    solver.add(f)
    result = []
    while solver.check() == sat:
        F=None
        m = solver.model()
        block = []
        result.append(m)
        for prop in props:
            prop_is_true = m.eval(prop, model_completion=True)
            if prop_is_true:
                new_prop = prop
            else:
                new_prop = Not(prop)
            if F is None: F=new_prop   #初始化一个条件组
            else: F=And(F,new_prop)  #依次往F添加参数值
            block.append(new_prop)
        f = And(f, Not(F))  #将答案F否定掉,继续求解,可以不断往下求
        solver.add(f)
    print("the given proposition: ", f)
    print("the number of solutions: ", len(result))

    def print_model(m):
        print(sorted([(d, m[d]) for d in m], key=lambda x: str(x[0])))

    for m in result:
        print_model(m)

 2.2 SAT(可满足性问题)

  在这一节中,我们将继续讨论如何使用Z3来检查命题的有效性。回想一下在练习2中,我们曾经使用定理证明器Coq来证明命题的有效性,所以这是另外一种方法。
  示例 B-1:正如我们在上一讲中所讨论的,命题P的有效性和可满足性之间的关系是valid(P) <==> unsat(~P)
  让我们考虑一下之前的例子:
    F = Or(P, Q)
    solve(Not(F))
  Z3 将输出以下解决方案:
    [P = False, Q = False]
  ~F是可满足的事实意味着命题F是无效的。通过这种方式,即可使用Z3这样的求解器来证明命题的有效性。

  示例 B-2:现在我们试图证明双重否定定律(~~P ->P)是有效的:
    F = Implies(Not(Not(P)), P)
    solve(Not(F))
  本节所有练习输出均为no solution,因为Valid(P)<==>Unsat(P)

  Exercise 2-2: 求解以下命题的有效性

皮尔斯定律: ((P->Q)->P)->P)
P, Q = Bools('P Q')
F = Implies(Implies(Implies(P, Q), P), P)
solve(Not(F))

  Exercise 2-3: 求解以下命题的有效性

(P -> Q) -> (~Q -> ~P)
P, Q =Bools('P Q')
X = Implies(P, Q)
Y = Implies(Not(Q), Not(P))
F = Implies(X, Y)
solve(Not(F))

  Exercise 2-4: 求解以下命题的有效性

(P -> Q /\ R) -> ((P -> Q) /\ (P -> R))
P, Q, R =Bools('P Q R')
A = Implies(P, And(Q, R))
B = Implies(P, Q)
C = Implies(P, R)
F = Implies(A, And(B, C))
solve(Not(F))

 2.3 DPLL算法

  在讲座中,我们讨论了DPLL算法。在分配的这一部分中,您需要实现 DPLL 算法。粗略地说,要实现这个算法,有以下几个步骤:首先,我们应该用一些抽象的语法来表示命题语法;其次,我们应该实现所有功能:
  nnf(P):将命题P转换为否定范式;
  cnf(P): 将命题P转换为连词范式;
  dpll(P):计算命题P的满足性P;
  前两步的目的是,将任意命题P转化为 (命题组A) /\ (命题组B) /\ (命题组C) 的形式 (命题组内部只包含~和\/);
  这样转换最大的好处在于,命题组内部只要有一个命题满足该命题组即可满足,所有命题组都必须满足,非常容易判断
  消除蕴含的规则如下:

  转换为NNF的规则如下:

  转换为CNF的规则如下:

  DPLL算法的示例如下

  DPLL算法的伪代码如下:

DPLL算法实现如下:

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))
    # 引入形成(prop.left->prop.right的格式)
    if isinstance(prop, PropTrue):
        return True
    # 永真
    if isinstance(prop, PropFalse):
        return False
    # 永假
    if 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))
    #分别形成 And Or Not

#转换成否定范式NNF
def nnf(prop: Prop) -> Prop:
    #如果否定联结符的联结对象只是命题原子的公式称为否定范式,每部分转换成原子命题即可
    if isinstance(prop, PropImplies):
        return PropOr(PropNot(nnf(prop.left)), nnf(prop.right))
        # P -> Q -> ( ~P ) | ( Q );
        # 如果含有And
    if isinstance(prop, PropAnd):
        return PropAnd(nnf(prop.left), nnf(prop.right))
        # 如果含有Or
    if isinstance(prop, PropOr):
        return PropOr(nnf(prop.left), nnf(prop.right))
        # 如果含有Not
    if isinstance(prop, PropNot):
        #~(prop.p)
        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()
        # ~T=F
        if isinstance(prop.p, PropFalse):
            return PropTrue()
        # ~F=T
        if isinstance(prop.p, PropOr):
            return PropAnd(nnf(PropNot(prop.p.left)), nnf(PropNot(prop.p.right)))
        # ~(prop.p,left or prop.p.right) -> ~prop.p,left and  ~prop.p.right
        if isinstance(prop.p, PropAnd):
            return PropOr(nnf(PropNot(prop.p.left)), nnf(PropNot(prop.p.right)))
        # ~(prop.p,left and prop.p.right) -> ~prop.p,left or  ~prop.p.right
        if isinstance(prop.p, PropImplies):
            return PropAnd(nnf(prop.p.left), nnf(PropNot(prop.p.right)))
        # ~(prop.p,left -> prop.p.right) -> ~(~prop.p,left or prop.p.right) -> prop.p.left and ~prop.p.right
    return prop

#原子命题判断
def is_atom(nnf_prop: Prop) -> bool:
    if isinstance(nnf_prop, PropOr) or isinstance(nnf_prop, PropAnd):
        return False
    return True

#转换为CNF
def cnf(nnf_prop: Prop) -> Prop:
    # def cnf_d(left: Prop, right: Prop) -> Prop:
    #     pass

    # raise1 Todo("Exercise 3-3: try to implement the `cnf`and `cnf_d` method")
        def cnf_d(left: Prop, right: Prop) -> Prop:    
		#处理cnf 左右循环递归的情况 避免 Or情况出现prop.left.left等情况,过于复杂
            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_prop
        if 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.
 1   For example: "((~p1 \\/ ~p3) /\\ (~p1 \\/ p4))" can be
    transfer to "[[~p1, ~p3], [~p1, p4]]".

    Parameters
    ----------
    cnf_prop : Prop
        CNF 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:
    flatten_cnf = flatten(cnf(nnf(prop)))

    # 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.
    # raise1 Todo("Exercise 3-4: try to implement the `dpll` algorithm")dpll(P)
    #初始化字典
    result = dict()
    for props in flatten_cnf:
        for prop1 in props:
            if isinstance(prop1, PropVar):
                result[prop1.var] = False
            if isinstance(prop1, PropNot):
                result[prop1.p.var] = False

    def select_atomic(prop: Prop) -> Prop:
        if isinstance(prop, PropVar):
            return prop
        #已经赋值,且为原子命题,直接返回
        if 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 prop
        #prop真 prop假 已经赋值 直接返回
        if isinstance(prop, PropAnd):
            if isinstance(prop.left, PropFalse) or isinstance(prop.right, PropFalse):
                return PropFalse()
            #And 情况 左右一边为假可以直接返回
            elif isinstance(prop.left, PropTrue):
                return unitProp(prop.right)
            # And 情况 左真。递归判断右边即可
            elif isinstance(prop.right, PropTrue):
                return unitProp(prop.left)
            # And 情况 右真。递归判断左边即可
            else:
                return PropAnd(unitProp(prop.left), unitProp(prop.right))
                    #左右分别递归 并用And判断
        if isinstance(prop, PropOr):
            if isinstance(prop, PropTrue) or isinstance(prop, PropTrue):
                return PropTrue()
            # Or 情况 左右一边为真可以直接返回
            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))
                # 左右分别递归 并用Or判断
        if isinstance(prop, PropNot):
            if isinstance(prop, PropTrue):
                return PropFalse()
            if isinstance(prop, PropFalse):
                return PropTrue()
            else:
                return prop
        #Not情况 返回值取反即可

    #选取命题中一个变量赋值
    def set_var_value(prop1: Prop, prop2: Prop, value: PropTrue or PropFalse): 
	# dpll算法的核心是回溯,因此需要拷贝命题,以便错误时用于回溯
        if isinstance(prop1, PropVar):
            if prop1.var == prop2.var:
                return value
        if isinstance(prop1, PropAnd):
            prop1.left = set_var_value(prop1.left, prop2, value)
            prop1.right = set_var_value(prop1.right, prop2, value)
            if isinstance(prop1.left, PropFalse) or isinstance(prop1.right, PropFalse):
                return PropFalse()
            if isinstance(prop1.left, PropTrue):
                return prop1.right
            if isinstance(prop1.right, PropTrue):
                return prop1.left
            # And 情况 具体实现同上
        if isinstance(prop1, PropOr):
            prop1.left = set_var_value(prop1.left, prop2, value)
            prop1.right = set_var_value(prop1.right, prop2, value)
            if isinstance(prop1.left, PropTrue) or isinstance(prop1.right, PropTrue):
                return PropTrue()
            if isinstance(prop1.left, PropFalse):
                return prop1.right
            if isinstance(prop1.right, PropFalse):
                return prop1.left
            #Or 情况 具体实现同上
        if isinstance(prop1, PropNot):
            prop1.p = set_var_value(prop1.p, prop2, value)
            if isinstance(prop1.p, PropTrue):
                return PropFalse()
            # ~T 返回F
            if isinstance(prop1.p, PropFalse):
                return PropTrue()
            # ~F 返回T
        return prop1

    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(prop)
        if isinstance(prop, PropTrue) | isinstance(prop, PropFalse):
            return prop
        p = select_atomic(prop)

        if p is None:
            return prop
        if isinstance(assignment, PropTrue):
            result[p.var] = True
        elif isinstance(assignment, PropFalse):
            result[p.var] = False

        prop = 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

 2.4 应用

  Exercise 3-1: 求解以下电路图的结果

#set_all为exercise1-6中的函数
def circuit_layout():
    solver = Solver()
    a, b, c, d = Bools('a b c d')
    F=Or(And(And(a,b),d),And(Not(c),And(a,b)))
    sat_all([a,b,c,d],F)
    solver.add(F)
# Z3 outputs:
#   the number of solutions:  3
#   [(a, True), (b, True), (c, False), (d, True)]
#   [(a, True), (b, True), (c, False), (d, False)]
#   [(a, True), (b, True), (c, True), (d, True)]

  Exercise 3-2: 求解以下座位的情况

def seat_arrangement():
    solver = Solver()
    # 1. First we need to modeling the problem
    # Let say:
    #   A_i means Alice takes seat Ai,
    #   B_i means Bob takes seat Bi,
    #   C_i means Carol takes seat Ci.
    # And since there are only 3 seats, so 1 <= i <= 3

    n_seat = 3
    a1, a2, a3 = Bools('a1 a2 a3')
    b1, b2, b3 = Bools('b1 b2 b3')
    c1, c2, c3 = Bools('c1 c2 c3')

    # alice must take a seat:
    alice_take_seat_1 = And(a1, Not(a2), Not(a3), Not(b1), Not(c1))
    alice_take_seat_2 = And(a2, Not(a1), Not(a3), Not(b2), Not(c2))
    alice_take_seat_3 = And(a3, Not(a1), Not(a2), Not(b3), Not(c3))
    solver.add(Or(alice_take_seat_1, alice_take_seat_2, alice_take_seat_3))
    T=[alice_take_seat_1, alice_take_seat_2, alice_take_seat_3]
    F=Or(alice_take_seat_1, alice_take_seat_2, alice_take_seat_3)
    # print("alice必须要有座位的答案如下")
    # sat_all(T,F)

    # bob must take a seat:
    # raise Todo("Exercise 5-1: try to add constraints that indicate Bob must take a seat")
    Bob_take_seat_1 = And(b1,Not(b2),Not(b3),Not(a1),Not(c1))
    Bob_take_seat_2 = And(b2, Not(b1), Not(b3), Not(a2), Not(c2))
    Bob_take_seat_3 = And(b3, Not(b2), Not(b1), Not(a3), Not(c3))
    solver.add(Or(Bob_take_seat_1, Bob_take_seat_2, Bob_take_seat_3))
    T.append(Bob_take_seat_1)
    T.append(Bob_take_seat_2)
    T.append(Bob_take_seat_3)
    F=And(F,Or(Bob_take_seat_1, Bob_take_seat_2, Bob_take_seat_3))
    solver.add(Or(F))
    # print("erexcise 5-1***************************")
    # print("Bob必须要有座位的答案如下")
    # sat_all(T, Or(And(Or(alice_take_seat_1, alice_take_seat_2, alice_take_seat_3)),Bob_take_seat_1, Bob_take_seat_2, Bob_take_seat_3))
    # carol must take a seat:
    # raise Todo("Exercise 5-2: try to add constraints that indicate Carol must take a seat")

    Carol_take_seat_1 = And(c1, Not(c2), Not(c3), Not(a1), Not(b1))
    Carol_take_seat_2 = And(c2, Not(c1), Not(c3), Not(a2), Not(b2))
    Carol_take_seat_3 = And(c3, Not(c2), Not(c1), Not(a3), Not(b3))

    T.append(Carol_take_seat_1)
    T.append(Carol_take_seat_2)
    T.append(Carol_take_seat_3)
    F = And(F, Or(Carol_take_seat_1, Carol_take_seat_2, Carol_take_seat_3))
    solver.add(Or(F))
    # print("erexcise 5-2***************************")
    # print("Carol必须要有座位的答案如下")

    print("每个人都有座位的所有情况如下*********************")
    sat_all(T,F)

    # alice can not sit near to carol:
    alice_not_near_carol = And(Implies(a1, Not(c2)), Implies(a2, Not(Or(c1, c3))), Implies(a3, Not(c2)))
    solver.add(alice_not_near_carol)
    T1=T
    F1=F
    T1.append(alice_not_near_carol)
    F1=And(F1,alice_not_near_carol)
    print("每个人都有座位且Alice不在carol旁边的所有情况如下*********************")
    sat_all(T1, F1)

    # 3. Bob can not sit right to Alice
    # raise Todo("Exercise 5-3: try to add constraints that indicate Bob can not sit right to Alice")
    # Hint: here only one solution is printed, you may change this to
    # print all the solutions to check your implementation.
    solver = Solver()
    solver.add(F)
    alice_not_near_Bob = And(Implies(a1, Not(b2)), Implies(a2, Not(Or(b1, b3))), Implies(a3, Not(b2)))
    solver.add(alice_not_near_Bob)
    T2= T
    F2 =F
    T2.append(alice_not_near_Bob)
    F2 = And(F2, alice_not_near_Bob)
    print("每个人都有座位且Bob不在Alice旁边的所有情况如下*********************")
    sat_all(T2,F2)
    print("条件1 2 都满足Bob不在Alice旁边 Alice不在carol旁边")
    T2.append(T1)
    F2=And(F2,F1)
    sat_all(T2,F2)
    print("每个人都有座位且Bob不在Alice旁边的情况如下*********************")

    solver.check()
    model = solver.model()
    # print(model)
    # fancy printing
    if model.evaluate(a1):
        print("Alice ", end='')
    if model.evaluate(b1):
        print("Bob ", end='')
    if model.evaluate(c1):
        print("Carol ", end='')
    if model.evaluate(a2):
        print("Alice ", end='')
    if model.evaluate(b2):
        print("Bob ", end='')
    if model.evaluate(c2):
        print("Carol ", end='')
    if model.evaluate(a3):
        print("Alice", end='')
    if model.evaluate(b3):
        print("Bob", end='')
    if model.evaluate(c3):
        print("Carol", end='')

# Z3 outputs:
#   每个人都有座位的所有情况如下*********************
#   the number of solutions:  6
#   Bob Alice Carol	
#   Bob Carol Alice	
#   Carol Bob Alice	
#   Carol Alice Bob	
#   Alice Carol Bob	
#   Alice Bob Carol	
#   每个人都有座位且Alice不在carol旁边的所有情况如下*********************
#   the number of solutions:  2
#   Carol Bob Alice	
#   Alice Bob Carol	
#   每个人都有座位且Bob不在Alice旁边的所有情况如下*********************
#   the number of solutions:  2
#   Bob Carol Alice	
#   Alice Carol Bob	
#   条件1 2 都满足Bob不在Alice旁边 Alice不在carol旁边
#   the number of solutions:  0
#   每个人都有座位且Bob不在Alice旁边的情况如下*********************
#   Bob Carol Alice

  Challenge: 求解N皇后问题

#本函数只有横竖两部分是完全正确的,斜的两种情况都有问题,斜的情况可以确保有但不能确保只有一个,
#由于本题是Challenge,所以也没有继续优化了
def four_queen():
    solver = Solver()
    # the basic data structure:
    N = 4
    board = [[Bool('b_{}_{}'.format(i, j)) for i in range(N)]
             for j in range(N)]

    ###这题要是类型是int 用1 0表示会简单很多
    # constraint 1: each row has just one queen:
    rows = []
    for i in range(N):
        current_row = []
        for j in range(N):
            current_row.append(board[i][j])
            for k in range(N):
                if k != j:
                    current_row.append(Not(board[i][k]))
        rows.append(current_row)

    # for row in rows:
    #     print(row)
    #     print("*****************")
    F=None
    for row in rows:
        Q=None
        T=None
        for i in range(N*N):
            if (i+1)%N==0:
                Q=And(Q,row[i])
                if(T is None): T=Q
                else: T=Or(T,Q)
            elif i%N==0:
                Q=row[i]
            else:
                Q=And(Q,row[i])
        if(F==None):F=T
        else: F=And(F,T)
    solver.add(F)

    # rows_c = [Or(board[i]) == True for i in range(N)]
    # constraint 2: each column has just one queen:
    # rows_c=[And(rows[i]) for i in range[4]]
    # raise Todo("Challenge: add constraints which describe each column has just one queen")
    colums = []
    for i in range(N):
        current_colum = []
        for j in range(N):
            current_colum.append(board[j][i])
            for k in range(N):
                if k != i:
                    current_colum.append(Not(board[j][k]))
        colums.append(current_colum)

    for colum in colums:
        Q = None
        T = None
        for i in range(N * N):
            if (i + 1) % N == 0:
                Q = And(Q, colum[i])
                if (T is None):
                    T = Q
                else:
                    T = Or(T, Q)
            elif i % N == 0:
                Q = colum[i]
            else:
                Q = And(Q, colum[i])
        F = And(F, T)
    solver.add(F)
    # colum_c = [And(rows[i]) for i in range[4]]
    # rows_c = [Or([board[i][j] for j in range(N)]) == True for i in range(N)]
    # rows_c = [Or(board[i]) == True for i in range(N)]

    # constraint 3: each diagonal has at most one queen:
    # raise Todo("Challenge: add constraints which describe each diagonal has at most one queen")
    cells_c = [Or(board[i][j] == False, board[i][j] == True) for i in range(N) for j in range(N)]
    #这种写法有问题,可以确保有,但不能确保只有一个
    # constraint 4: each anti-diagonal has at most one queen:
    # raise Todo("Challenge: add constraints which describe each anti-diagonal has at most one queen")
    diagonals_c = [Implies(And(board[i][j] == True, board[k][h] == True,i != k, j != h), abs(k - i) != abs(j - h))
                   for i in range(N) for j in range(N)
                    for k in range(N) for h in range(N)]
    # 这样如果斜的多个还是没法处理  用i-j判断或许是一种可行的思路
    four_queens_c = cells_c  + diagonals_c
    solver.add(four_queens_c)
    if solver.check() == sat:
        m = solver.model()
        r = [[m.evaluate(board[i][j]) for j in range(N)] for i in range(N)]
        print_matrix(r)
    else:
        print("failed to solve")
#output is:
#   [[False, False, True, False],
#   [True, False, False, False],
#   [False, False, False, True],
#   [False, True, False, False]]

三.下载链接

  在线下载: 请点击这儿下载
  如果下载失败,点击此百度云链接:形式化方法作业三,提取码y825
  如果您有任何疑问,请通过邮箱联系我

end
  • 作者:Yuan(联系作者)
  • 发表时间:2021-12-19 18:34
  • 版权声明:自由转载-非商用-非衍生-保持署名(创意共享3.0许可证)
  • 转载声明:如果是转载博主转载的文章,请附上原文链接
  • 公众号转载:请联系作者
  • 评论

    zy、
    Exercise 1-2: 求解以下命题的满足性 P \/ (Q \/ R) P, Q, R =Bools('P Q R') F = Or(P,Or(Or(Q, R))) solve(F) # Z3 output this:"[R = False, Q = False, P = True]" 请问下,这里的F = Or(P,Or(Or(Q, R)))是不是多写了一个Or呀?