Решение математической задачи. 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, чтобы решить ее, но я не знаю, с чего начать решая это. Я не хотел бы получить ответ, но подсказка о том, как правильно это сделать.

Спасибо!

Answer 1

Можно использовать Z3py , с открытым исходным кодом SAT / SMT решатель. Все ограничения записываются с использованием логических операций , в основном And и Or. Затем ограничения будут распространяться до тех пор, пока решение не будет найдено (или решатель убедится, что решения не существует). Решатель ищет только одно возможное решение. Чтобы знать, что это единственный, решатель может быть запущен снова с дополнительным предложением, чтобы найти другое решение.

Эта конкретная проблема c кажется немного сложной для преобразования в такие ограничения. Кроме того, ограничение «ровно одно» для # 614 должно быть написано более сложным. Тем не менее система находит единственное решение.

Код можно несколько очистить с помощью функций, которые явно проверяют составные ограничения.

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())