python-3.x - 解决一道数学题。Python3猜三个数字

Question

我必须解决这个问题：寻找三个数字，规则如下。

#682 one number and its position correct
#614 one number is correct but its position incorrect
#206 two numbers are correct but their position isnt
#738 nothing is correct 
#780 one number is correct but its position wrong

我想用python来解决它，但我不知道从哪里开始解决它。我不希望得到答案，而是如何正确地做到这一点的线索。

谢谢 ！

标签： python-3.xmathnumbers

Answer 1

一种可能是使用Z3py，一个开源的SAT/SMT求解器。所有约束都是使用逻辑运算编写的，主要是And和Or。然后，约束将传播，直到找到解决方案（或求解器确保不存在解决方案）。求解器只寻找一种可能的解决方案。要知道它是唯一的，可以使用附加子句再次运行求解器以找到不同的解决方案。

这个特定的问题似乎有点复杂，要转换成这样的约束。此外，#614 的“exactly one”约束应该写得更复杂。然而，系统找到了唯一的解决方案。

可以通过显式检查复合约束的函数对代码进行一些清理。

from z3 import Solver, Int, And, Or, Xor

a, b, c = Int('a'), Int('b'), Int('c')
s = Solver()
s.add(And(a >= 0, a <= 9))
s.add(And(b >= 0, b <= 9))
s.add(And(c >= 0, c <= 9))
# 682 one digit and its position correct
s.add(Or(And(a == 6, b != 8, c != 2), And(b == 8, a != 6, c != 2), And(c == 2, b != 8, a != 6)))
# 614 one digit is correct but its position incorrect
s.add(And(a != 6, b != 1, c != 4))
s.add(Or([a == 1, a == 4, b == 6, b == 4, c == 6, c == 1]))  # should be: exactly one
# 206 two digits are correct but their position isn't
s.add(And(a != 2, b != 0, c != 6))
n206_2 = And(Or(a == 0, c == 0), Or(a == 6, b == 6), And(b != 2, c != 2))
n206_0 = And(Or(b == 2, c == 2), Or(a == 6, b == 6), And(a != 0, c != 0))
n206_6 = And(Or(b == 2, c == 2), Or(a == 0, c == 0), And(a != 6, b != 6))
s.add(Or(n206_2, n206_0, n206_6))
# 738 nothing is correct
s.add(And([a != 7, b != 7, c != 7, a != 3, b != 3, c != 3, a != 8, b != 8, c != 8]))
# 780 one digit is correct but its position wrong
s.add(And(a != 7, b != 8, c != 0))
n780_0 = And(c != 7, c != 8, a != 8, b != 7, Xor(a == 0, b == 0))
n780_8 = And(b != 0, b != 7, a != 8, c != 0, Xor(a == 8, c == 8))
n780_7 = And(a != 0, a != 8, c != 8, b != 0, Xor(b == 7, c == 7))
s.add(Or(n780_0, n780_8, n780_7))
print(s.check())
print(s.model())