Неправильная модель после z3py pu sh, но правильная модель без - PullRequest
Новая
       91

Неправильная модель после z3py pu sh, но правильная модель без

1 голос
/ 28 мая 2020
• 1000 1007 *

Однако, если я добавлю s.add (ans6 == 4), а также s.add (ans9 == 3) piror к s.pu sh (), модель будет правильной как unsat.

Это ошибка или я неправильно использую Z3? Я думал, что это может быть выражено мягкими ограничениями, но в документации не упоминается.

полный исходный код выглядит следующим образом: 

#!/usr/bin/env python
# coding: utf-8

from z3 import *

# ten multiple choices
ans = [Int('ans%d' % (i)) for i in range(10)]

letters = {}
for i in range(5):
    letters[i] = "0ABCD"[i]

choice_a = 1
choice_b = 2
choice_c = 3
choice_d = 4
choice_shitty = 999
choices = [choice_a, choice_b, choice_c, choice_d]

s = Solver()
for i in range(10):
    s.add(Or(ans[i] == choice_a, ans[i] == choice_b, ans[i] == choice_c, ans[i] == choice_d))

#2
s.add(Or(And(ans[1] == choice_a, ans[4] == choice_c),
         And(ans[1] == choice_b, ans[4] == choice_d),
         And(ans[1] == choice_c, ans[4] == choice_a),
         And(ans[1] == choice_d, ans[4] == choice_b)))

#3
s.add(Or(And(ans[2] == choice_a, And(ans[2] != ans[5], ans[5] == ans[1], ans[1] == ans[3])),
         And(ans[2] == choice_b, And(ans[5] != ans[2], ans[2] == ans[1], ans[1] == ans[3])),
         And(ans[2] == choice_c, And(ans[1] != ans[2], ans[2] == ans[5], ans[5] == ans[3])),
         And(ans[2] == choice_d, And(ans[3] != ans[5], ans[2] == ans[5], ans[5] == ans[1]))))

#4
s.add(Or(And(ans[3] == choice_a, ans[0] == ans[4]),
         And(ans[3] == choice_b, ans[1] == ans[6]),
         And(ans[3] == choice_c, ans[0] == ans[8]),
         And(ans[3] == choice_d, ans[5] == ans[9])))

#5
s.add(Or(And(ans[4] == choice_a, ans[4] == ans[7]),
         And(ans[4] == choice_b, ans[4] == ans[3]),
         And(ans[4] == choice_c, ans[4] == ans[8]),
         And(ans[4] == choice_d, ans[4] == ans[6])))

#6
s.add(Or(And(ans[5] == choice_a, And(ans[1] == ans[3], ans[3] == ans[7])),
         And(ans[5] == choice_b, And(ans[0] == ans[5], ans[5] == ans[7])),
         And(ans[5] == choice_c, And(ans[2] == ans[9], ans[9] == ans[7])),
         And(ans[5] == choice_d, And(ans[4] == ans[8], ans[8] == ans[7]))))

#7


#8
s.add(Or(And(ans[7] == choice_a, Not(Or(ans[0] - ans[6] == 1, ans[0] - ans[6] == -1))),
         And(ans[7] == choice_b, Not(Or(ans[0] - ans[4] == 1, ans[0] - ans[4] == -1))),
         And(ans[7] == choice_c, Not(Or(ans[0] - ans[1] == 1, ans[0] - ans[1] == -1))),
         And(ans[7] == choice_d, Not(Or(ans[0] - ans[9] == 1, ans[0] - ans[9] == -1)))))

#9
s.add(Or(And(ans[8] == choice_a, Or(And((ans[0] == ans[5]), Not(ans[5] == ans[4])), 
                                      And(Not(ans[0] == ans[5]), (ans[5] == ans[4])))),
         And(ans[8] == choice_b, Or(And((ans[0] == ans[5]), Not(ans[9] == ans[4])), 
                                      And(Not(ans[0] == ans[5]), (ans[9] == ans[4])))),
         And(ans[8] == choice_c, Or(And((ans[0] == ans[5]), Not(ans[1] == ans[4])), 
                                      And(Not(ans[0] == ans[5]), (ans[1] == ans[4])))),
         And(ans[8] == choice_d, Or(And((ans[0] == ans[5]), Not(ans[8] == ans[4]))), 
                                      And(Not(ans[0] == ans[5]), (ans[8] == ans[4])))))

#10
# max - min count

#for c in s.assertions():
#    print (c)
#s.check()
#print (s.model())

#s.add(ans[6] == 4)
#s.add(ans[9] == 3)


result = []
while True:    
    if s.check() == unsat:
        print ("no solution or search done(?)")
        print ("RESULT FOUND = ", len(result))
        break
    elif s.check() == sat:
        m = s.model()
        #print (m)        

        # prevent next model from using the SAME assignment as a previous model
        block = []
        for cond in m:
            clause = cond()
            block.append(clause != m[cond])
        #print(block)


        # special case: #7和#10
        s.push()

        cnt = {}
        for c in choices:
            cnt[c] = sum([1 for a in ans if m[a] == c])
        mincnt_choice = min(cnt, key=cnt.get)
        maxcnt_choice = max(cnt, key=cnt.get)
        mincnt = cnt[mincnt_choice]
        maxcnt = cnt[maxcnt_choice]
        diff = maxcnt - mincnt
        print ('ANSWER LETTER COUNTS： ', cnt, 'MIN： ', letters[mincnt_choice], 'MAX： ', letters[maxcnt_choice])
        print ('DIFF for #10：', diff)

        #7 
        if mincnt_choice == choice_a:
            s.add(ans[6] == choice_c)
        elif mincnt_choice == choice_b:
            s.add(ans[6] == choice_b)
        elif mincnt_choice == choice_c:
            s.add(ans[6] == choice_a)
        elif mincnt_choice == choice_d:
            s.add(ans[6] == choice_d)
        else:
            # impossible
            s.add(ans[6] == choice_shitty)


        #10
        if diff == 3:
            s.add(ans[9] == choice_a)
        elif diff == 2:
            s.add(ans[9] == choice_b)
        elif diff == 4:
            s.add(ans[9] == choice_c)
        elif diff == 1:
            s.add(ans[9] == choice_d)
        else:
            # impossible
            s.add(ans[9] == choice_shitty)

        for c in s.assertions():
            print (c)

        if s.check() == unsat:
            print ("#7/#10 constraint failed\n")
            s.pop()      

            s.add(Or(block)) 

        elif s.check() == sat:
            print ('SOLUTION: -------------------\n')
            print (m)
            #for i in range(10):
            #    sys.stdout.write (str(i+1)+". "+letters[int(str(m[ans[i]]))]+"\n")
            #print ("\n")
            result.append(m)      

            # prevent next model from using the SAME assignment as a previous model
            block = []
            for cond in m:
                clause = cond()
                block.append(clause != m[cond])
            s.pop()
            s.add(Or(block)) 
        else:
            print ("exception")
    else:
        print ("exception")
...