From 5c1f797943b07bb6cfae24800302cf16576826d1 Mon Sep 17 00:00:00 2001 From: Yuri Victorovich Date: Mon, 7 Oct 2024 17:10:58 -0700 Subject: =?UTF-8?q?math/py-z3-solver:=20update=204.8.17=20=E2=86=92=204.13?= =?UTF-8?q?.2?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This fixes the problem from bug#280689. PR: 280689 --- math/py-z3-solver/files/example-eight-queens.py | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) create mode 100644 math/py-z3-solver/files/example-eight-queens.py (limited to 'math/py-z3-solver/files/example-eight-queens.py') diff --git a/math/py-z3-solver/files/example-eight-queens.py b/math/py-z3-solver/files/example-eight-queens.py new file mode 100644 index 000000000000..06eb2955fd02 --- /dev/null +++ b/math/py-z3-solver/files/example-eight-queens.py @@ -0,0 +1,22 @@ +# example from https://ericpony.github.io/z3py-tutorial/guide-examples.htm + +from z3 import Int, And, Distinct, If, solve, print_matrix + + +# We know each queen must be in a different row. +# So, we represent each queen by a single integer: the column position +Q = [ Int('Q_%i' % (i + 1)) for i in range(8) ] + +# Each queen is in a column {1, ... 8 } +val_c = [ And(1 <= Q[i], Q[i] <= 8) for i in range(8) ] + +# At most one queen per column +col_c = [ Distinct(Q) ] + +# Diagonal constraint +diag_c = [ If(i == j, + True, + And(Q[i] - Q[j] != i - j, Q[i] - Q[j] != j - i)) + for i in range(8) for j in range(i) ] + +solve(val_c + col_c + diag_c) -- cgit v1.2.3