A constraint workbench for quantitative professionals

Queens is the smallest useful model.

A regional board turns strategy into an explicit model: variables, partitions, conflicts, a solver contract, and evidence you can inspect rather than merely trust.

Boolean grid Finite domains Transparent search

01 / live model

Regional Queens

Draft assumptions and rule changes, then run the bounded teaching checker. The baseline remains a separate, supplied solver evidence layer.

Precomputed Z3 result Verified 7×7 baseline: SAT and unique; a separate blocking-clause query was UNSAT.

Derived model analysis Run 1: 4 active rule families · 0 active assumptions · 19 deterministic nodes.

Illustrative search Teaching trace only — not Z3’s internal trace.

Precomputed baseline Draft assumption Active run witness Region partition

Selected cell

A1 · Amber

No draft assumption here. A witness queen, if shown, belongs to the active run.

Draft constraint families Rowsexactly one selection per row∀r. Σc qᵣ,ᶜ = 1 Columnsexactly one selection per column∀c. Σr qᵣ,ᶜ = 1 Regionsexactly one selection per coloured region∀g. Σ(r,c)∈g qᵣ,ᶜ = 1 Non-touchingadjacent cells, including orthogonal and diagonal neighbors, cannot both be selectedmax(|Δr|, |Δc|) = 1 ⇒ qᵤ + qᵥ ≤ 1

Variables49 Bool

Active exact-one21

Active adjacency pairs156

Draft / active / witness0 / 0 / 7

The Python baseline uses 21 exact-one equalities and 312 directed neighbor implications. The normalized model has 156 undirected adjacent pairs; with row and column rules active, 84 orthogonal pairs are redundant and 72 diagonal pairs remain. The Non-touching toggle itself always covers all 156 adjacent pairs independently.

Illustrative search · active run 1

Step trace

not Z3’s internal trace

Start from the visible fixed assumptions; choose an unsatisfied partition deterministically.

1 / 29

Portable active run

SMT-LIB source

; Constraint Atlas — 7×7 Boolean-grid encoding
; Baseline provenance: Z3 SAT; blocking this model is UNSAT (unique).
(set-logic QF_FD)
(set-option :produce-models true)
(declare-const q_0_0 Bool)
(declare-const q_0_1 Bool)
(declare-const q_0_2 Bool)
(declare-const q_0_3 Bool)
(declare-const q_0_4 Bool)
(declare-const q_0_5 Bool)
(declare-const q_0_6 Bool)
(declare-const q_1_0 Bool)
(declare-const q_1_1 Bool)
(declare-const q_1_2 Bool)
(declare-const q_1_3 Bool)
(declare-const q_1_4 Bool)
(declare-const q_1_5 Bool)
(declare-const q_1_6 Bool)
(declare-const q_2_0 Bool)
(declare-const q_2_1 Bool)
(declare-const q_2_2 Bool)
(declare-const q_2_3 Bool)
(declare-const q_2_4 Bool)
(declare-const q_2_5 Bool)
(declare-const q_2_6 Bool)
(declare-const q_3_0 Bool)
(declare-const q_3_1 Bool)
(declare-const q_3_2 Bool)
(declare-const q_3_3 Bool)
(declare-const q_3_4 Bool)
(declare-const q_3_5 Bool)
(declare-const q_3_6 Bool)
(declare-const q_4_0 Bool)
(declare-const q_4_1 Bool)
(declare-const q_4_2 Bool)
(declare-const q_4_3 Bool)
(declare-const q_4_4 Bool)
(declare-const q_4_5 Bool)
(declare-const q_4_6 Bool)
(declare-const q_5_0 Bool)
(declare-const q_5_1 Bool)
(declare-const q_5_2 Bool)
(declare-const q_5_3 Bool)
(declare-const q_5_4 Bool)
(declare-const q_5_5 Bool)
(declare-const q_5_6 Bool)
(declare-const q_6_0 Bool)
(declare-const q_6_1 Bool)
(declare-const q_6_2 Bool)
(declare-const q_6_3 Bool)
(declare-const q_6_4 Bool)
(declare-const q_6_5 Bool)
(declare-const q_6_6 Bool)
(assert (or q_0_0 q_0_1 q_0_2 q_0_3 q_0_4 q_0_5 q_0_6))
(assert (not (and q_0_0 q_0_1)))
(assert (not (and q_0_0 q_0_2)))
(assert (not (and q_0_0 q_0_3)))
(assert (not (and q_0_0 q_0_4)))
(assert (not (and q_0_0 q_0_5)))
(assert (not (and q_0_0 q_0_6)))
(assert (not (and q_0_1 q_0_2)))
(assert (not (and q_0_1 q_0_3)))
(assert (not (and q_0_1 q_0_4)))
(assert (not (and q_0_1 q_0_5)))
(assert (not (and q_0_1 q_0_6)))
(assert (not (and q_0_2 q_0_3)))
(assert (not (and q_0_2 q_0_4)))
(assert (not (and q_0_2 q_0_5)))
(assert (not (and q_0_2 q_0_6)))
(assert (not (and q_0_3 q_0_4)))
(assert (not (and q_0_3 q_0_5)))
(assert (not (and q_0_3 q_0_6)))
(assert (not (and q_0_4 q_0_5)))
(assert (not (and q_0_4 q_0_6)))
(assert (not (and q_0_5 q_0_6)))
(assert (or q_1_0 q_1_1 q_1_2 q_1_3 q_1_4 q_1_5 q_1_6))
(assert (not (and q_1_0 q_1_1)))
(assert (not (and q_1_0 q_1_2)))
(assert (not (and q_1_0 q_1_3)))
(assert (not (and q_1_0 q_1_4)))
(assert (not (and q_1_0 q_1_5)))
(assert (not (and q_1_0 q_1_6)))
(assert (not (and q_1_1 q_1_2)))
(assert (not (and q_1_1 q_1_3)))
(assert (not (and q_1_1 q_1_4)))
(assert (not (and q_1_1 q_1_5)))
(assert (not (and q_1_1 q_1_6)))
(assert (not (and q_1_2 q_1_3)))
(assert (not (and q_1_2 q_1_4)))
(assert (not (and q_1_2 q_1_5)))
(assert (not (and q_1_2 q_1_6)))
(assert (not (and q_1_3 q_1_4)))
(assert (not (and q_1_3 q_1_5)))
(assert (not (and q_1_3 q_1_6)))
(assert (not (and q_1_4 q_1_5)))
(assert (not (and q_1_4 q_1_6)))
(assert (not (and q_1_5 q_1_6)))
(assert (or q_2_0 q_2_1 q_2_2 q_2_3 q_2_4 q_2_5 q_2_6))
(assert (not (and q_2_0 q_2_1)))
(assert (not (and q_2_0 q_2_2)))
(assert (not (and q_2_0 q_2_3)))
(assert (not (and q_2_0 q_2_4)))
(assert (not (and q_2_0 q_2_5)))
(assert (not (and q_2_0 q_2_6)))
(assert (not (and q_2_1 q_2_2)))
(assert (not (and q_2_1 q_2_3)))
(assert (not (and q_2_1 q_2_4)))
(assert (not (and q_2_1 q_2_5)))
(assert (not (and q_2_1 q_2_6)))
(assert (not (and q_2_2 q_2_3)))
(assert (not (and q_2_2 q_2_4)))
(assert (not (and q_2_2 q_2_5)))
(assert (not (and q_2_2 q_2_6)))
(assert (not (and q_2_3 q_2_4)))
(assert (not (and q_2_3 q_2_5)))
(assert (not (and q_2_3 q_2_6)))
(assert (not (and q_2_4 q_2_5)))
(assert (not (and q_2_4 q_2_6)))
(assert (not (and q_2_5 q_2_6)))
(assert (or q_3_0 q_3_1 q_3_2 q_3_3 q_3_4 q_3_5 q_3_6))
(assert (not (and q_3_0 q_3_1)))
(assert (not (and q_3_0 q_3_2)))
(assert (not (and q_3_0 q_3_3)))
(assert (not (and q_3_0 q_3_4)))
(assert (not (and q_3_0 q_3_5)))
(assert (not (and q_3_0 q_3_6)))
(assert (not (and q_3_1 q_3_2)))
(assert (not (and q_3_1 q_3_3)))
(assert (not (and q_3_1 q_3_4)))
(assert (not (and q_3_1 q_3_5)))
(assert (not (and q_3_1 q_3_6)))
(assert (not (and q_3_2 q_3_3)))
(assert (not (and q_3_2 q_3_4)))
(assert (not (and q_3_2 q_3_5)))
(assert (not (and q_3_2 q_3_6)))
(assert (not (and q_3_3 q_3_4)))
(assert (not (and q_3_3 q_3_5)))
(assert (not (and q_3_3 q_3_6)))
(assert (not (and q_3_4 q_3_5)))
(assert (not (and q_3_4 q_3_6)))
(assert (not (and q_3_5 q_3_6)))
(assert (or q_4_0 q_4_1 q_4_2 q_4_3 q_4_4 q_4_5 q_4_6))
(assert (not (and q_4_0 q_4_1)))
(assert (not (and q_4_0 q_4_2)))
(assert (not (and q_4_0 q_4_3)))
(assert (not (and q_4_0 q_4_4)))
(assert (not (and q_4_0 q_4_5)))
(assert (not (and q_4_0 q_4_6)))
(assert (not (and q_4_1 q_4_2)))
(assert (not (and q_4_1 q_4_3)))
(assert (not (and q_4_1 q_4_4)))
(assert (not (and q_4_1 q_4_5)))
(assert (not (and q_4_1 q_4_6)))
(assert (not (and q_4_2 q_4_3)))
(assert (not (and q_4_2 q_4_4)))
(assert (not (and q_4_2 q_4_5)))
(assert (not (and q_4_2 q_4_6)))
(assert (not (and q_4_3 q_4_4)))
(assert (not (and q_4_3 q_4_5)))
(assert (not (and q_4_3 q_4_6)))
(assert (not (and q_4_4 q_4_5)))
(assert (not (and q_4_4 q_4_6)))
(assert (not (and q_4_5 q_4_6)))
(assert (or q_5_0 q_5_1 q_5_2 q_5_3 q_5_4 q_5_5 q_5_6))
(assert (not (and q_5_0 q_5_1)))
(assert (not (and q_5_0 q_5_2)))
(assert (not (and q_5_0 q_5_3)))
(assert (not (and q_5_0 q_5_4)))
(assert (not (and q_5_0 q_5_5)))
(assert (not (and q_5_0 q_5_6)))
(assert (not (and q_5_1 q_5_2)))
(assert (not (and q_5_1 q_5_3)))
(assert (not (and q_5_1 q_5_4)))
(assert (not (and q_5_1 q_5_5)))
(assert (not (and q_5_1 q_5_6)))
(assert (not (and q_5_2 q_5_3)))
(assert (not (and q_5_2 q_5_4)))
(assert (not (and q_5_2 q_5_5)))
(assert (not (and q_5_2 q_5_6)))
(assert (not (and q_5_3 q_5_4)))
(assert (not (and q_5_3 q_5_5)))
(assert (not (and q_5_3 q_5_6)))
(assert (not (and q_5_4 q_5_5)))
(assert (not (and q_5_4 q_5_6)))
(assert (not (and q_5_5 q_5_6)))
(assert (or q_6_0 q_6_1 q_6_2 q_6_3 q_6_4 q_6_5 q_6_6))
(assert (not (and q_6_0 q_6_1)))
(assert (not (and q_6_0 q_6_2)))
(assert (not (and q_6_0 q_6_3)))
(assert (not (and q_6_0 q_6_4)))
(assert (not (and q_6_0 q_6_5)))
(assert (not (and q_6_0 q_6_6)))
(assert (not (and q_6_1 q_6_2)))
(assert (not (and q_6_1 q_6_3)))
(assert (not (and q_6_1 q_6_4)))
(assert (not (and q_6_1 q_6_5)))
(assert (not (and q_6_1 q_6_6)))
(assert (not (and q_6_2 q_6_3)))
(assert (not (and q_6_2 q_6_4)))
(assert (not (and q_6_2 q_6_5)))
(assert (not (and q_6_2 q_6_6)))
(assert (not (and q_6_3 q_6_4)))
(assert (not (and q_6_3 q_6_5)))
(assert (not (and q_6_3 q_6_6)))
(assert (not (and q_6_4 q_6_5)))
(assert (not (and q_6_4 q_6_6)))
(assert (not (and q_6_5 q_6_6)))
(assert (or q_0_0 q_1_0 q_2_0 q_3_0 q_4_0 q_5_0 q_6_0))
(assert (not (and q_0_0 q_1_0)))
(assert (not (and q_0_0 q_2_0)))
(assert (not (and q_0_0 q_3_0)))
(assert (not (and q_0_0 q_4_0)))
(assert (not (and q_0_0 q_5_0)))
(assert (not (and q_0_0 q_6_0)))
(assert (not (and q_1_0 q_2_0)))
(assert (not (and q_1_0 q_3_0)))
(assert (not (and q_1_0 q_4_0)))
(assert (not (and q_1_0 q_5_0)))
(assert (not (and q_1_0 q_6_0)))
(assert (not (and q_2_0 q_3_0)))
(assert (not (and q_2_0 q_4_0)))
(assert (not (and q_2_0 q_5_0)))
(assert (not (and q_2_0 q_6_0)))
(assert (not (and q_3_0 q_4_0)))
(assert (not (and q_3_0 q_5_0)))
(assert (not (and q_3_0 q_6_0)))
(assert (not (and q_4_0 q_5_0)))
(assert (not (and q_4_0 q_6_0)))
(assert (not (and q_5_0 q_6_0)))
(assert (or q_0_1 q_1_1 q_2_1 q_3_1 q_4_1 q_5_1 q_6_1))
(assert (not (and q_0_1 q_1_1)))
(assert (not (and q_0_1 q_2_1)))
(assert (not (and q_0_1 q_3_1)))
(assert (not (and q_0_1 q_4_1)))
(assert (not (and q_0_1 q_5_1)))
(assert (not (and q_0_1 q_6_1)))
(assert (not (and q_1_1 q_2_1)))
(assert (not (and q_1_1 q_3_1)))
(assert (not (and q_1_1 q_4_1)))
(assert (not (and q_1_1 q_5_1)))
(assert (not (and q_1_1 q_6_1)))
(assert (not (and q_2_1 q_3_1)))
(assert (not (and q_2_1 q_4_1)))
(assert (not (and q_2_1 q_5_1)))
(assert (not (and q_2_1 q_6_1)))
(assert (not (and q_3_1 q_4_1)))
(assert (not (and q_3_1 q_5_1)))
(assert (not (and q_3_1 q_6_1)))
(assert (not (and q_4_1 q_5_1)))
(assert (not (and q_4_1 q_6_1)))
(assert (not (and q_5_1 q_6_1)))
(assert (or q_0_2 q_1_2 q_2_2 q_3_2 q_4_2 q_5_2 q_6_2))
(assert (not (and q_0_2 q_1_2)))
(assert (not (and q_0_2 q_2_2)))
(assert (not (and q_0_2 q_3_2)))
(assert (not (and q_0_2 q_4_2)))
(assert (not (and q_0_2 q_5_2)))
(assert (not (and q_0_2 q_6_2)))
(assert (not (and q_1_2 q_2_2)))
(assert (not (and q_1_2 q_3_2)))
(assert (not (and q_1_2 q_4_2)))
(assert (not (and q_1_2 q_5_2)))
(assert (not (and q_1_2 q_6_2)))
(assert (not (and q_2_2 q_3_2)))
(assert (not (and q_2_2 q_4_2)))
(assert (not (and q_2_2 q_5_2)))
(assert (not (and q_2_2 q_6_2)))
(assert (not (and q_3_2 q_4_2)))
(assert (not (and q_3_2 q_5_2)))
(assert (not (and q_3_2 q_6_2)))
(assert (not (and q_4_2 q_5_2)))
(assert (not (and q_4_2 q_6_2)))
(assert (not (and q_5_2 q_6_2)))
(assert (or q_0_3 q_1_3 q_2_3 q_3_3 q_4_3 q_5_3 q_6_3))
(assert (not (and q_0_3 q_1_3)))
(assert (not (and q_0_3 q_2_3)))
(assert (not (and q_0_3 q_3_3)))
(assert (not (and q_0_3 q_4_3)))
(assert (not (and q_0_3 q_5_3)))
(assert (not (and q_0_3 q_6_3)))
(assert (not (and q_1_3 q_2_3)))
(assert (not (and q_1_3 q_3_3)))
(assert (not (and q_1_3 q_4_3)))
(assert (not (and q_1_3 q_5_3)))
(assert (not (and q_1_3 q_6_3)))
(assert (not (and q_2_3 q_3_3)))
(assert (not (and q_2_3 q_4_3)))
(assert (not (and q_2_3 q_5_3)))
(assert (not (and q_2_3 q_6_3)))
(assert (not (and q_3_3 q_4_3)))
(assert (not (and q_3_3 q_5_3)))
(assert (not (and q_3_3 q_6_3)))
(assert (not (and q_4_3 q_5_3)))
(assert (not (and q_4_3 q_6_3)))
(assert (not (and q_5_3 q_6_3)))
(assert (or q_0_4 q_1_4 q_2_4 q_3_4 q_4_4 q_5_4 q_6_4))
(assert (not (and q_0_4 q_1_4)))
(assert (not (and q_0_4 q_2_4)))
(assert (not (and q_0_4 q_3_4)))
(assert (not (and q_0_4 q_4_4)))
(assert (not (and q_0_4 q_5_4)))
(assert (not (and q_0_4 q_6_4)))
(assert (not (and q_1_4 q_2_4)))
(assert (not (and q_1_4 q_3_4)))
(assert (not (and q_1_4 q_4_4)))
(assert (not (and q_1_4 q_5_4)))
(assert (not (and q_1_4 q_6_4)))
(assert (not (and q_2_4 q_3_4)))
(assert (not (and q_2_4 q_4_4)))
(assert (not (and q_2_4 q_5_4)))
(assert (not (and q_2_4 q_6_4)))
(assert (not (and q_3_4 q_4_4)))
(assert (not (and q_3_4 q_5_4)))
(assert (not (and q_3_4 q_6_4)))
(assert (not (and q_4_4 q_5_4)))
(assert (not (and q_4_4 q_6_4)))
(assert (not (and q_5_4 q_6_4)))
(assert (or q_0_5 q_1_5 q_2_5 q_3_5 q_4_5 q_5_5 q_6_5))
(assert (not (and q_0_5 q_1_5)))
(assert (not (and q_0_5 q_2_5)))
(assert (not (and q_0_5 q_3_5)))
(assert (not (and q_0_5 q_4_5)))
(assert (not (and q_0_5 q_5_5)))
(assert (not (and q_0_5 q_6_5)))
(assert (not (and q_1_5 q_2_5)))
(assert (not (and q_1_5 q_3_5)))
(assert (not (and q_1_5 q_4_5)))
(assert (not (and q_1_5 q_5_5)))
(assert (not (and q_1_5 q_6_5)))
(assert (not (and q_2_5 q_3_5)))
(assert (not (and q_2_5 q_4_5)))
(assert (not (and q_2_5 q_5_5)))
(assert (not (and q_2_5 q_6_5)))
(assert (not (and q_3_5 q_4_5)))
(assert (not (and q_3_5 q_5_5)))
(assert (not (and q_3_5 q_6_5)))
(assert (not (and q_4_5 q_5_5)))
(assert (not (and q_4_5 q_6_5)))
(assert (not (and q_5_5 q_6_5)))
(assert (or q_0_6 q_1_6 q_2_6 q_3_6 q_4_6 q_5_6 q_6_6))
(assert (not (and q_0_6 q_1_6)))
(assert (not (and q_0_6 q_2_6)))
(assert (not (and q_0_6 q_3_6)))
(assert (not (and q_0_6 q_4_6)))
(assert (not (and q_0_6 q_5_6)))
(assert (not (and q_0_6 q_6_6)))
(assert (not (and q_1_6 q_2_6)))
(assert (not (and q_1_6 q_3_6)))
(assert (not (and q_1_6 q_4_6)))
(assert (not (and q_1_6 q_5_6)))
(assert (not (and q_1_6 q_6_6)))
(assert (not (and q_2_6 q_3_6)))
(assert (not (and q_2_6 q_4_6)))
(assert (not (and q_2_6 q_5_6)))
(assert (not (and q_2_6 q_6_6)))
(assert (not (and q_3_6 q_4_6)))
(assert (not (and q_3_6 q_5_6)))
(assert (not (and q_3_6 q_6_6)))
(assert (not (and q_4_6 q_5_6)))
(assert (not (and q_4_6 q_6_6)))
(assert (not (and q_5_6 q_6_6)))
(assert (or q_0_0 q_0_1 q_0_5 q_1_0 q_1_1 q_1_2 q_1_3 q_1_5 q_2_0 q_2_1 q_2_2 q_2_3 q_2_4 q_2_5 q_3_0 q_3_1 q_3_2 q_3_3 q_3_4 q_4_0 q_4_1 q_4_3 q_4_4 q_5_3 q_5_4))
(assert (not (and q_0_0 q_0_1)))
(assert (not (and q_0_0 q_0_5)))
(assert (not (and q_0_0 q_1_0)))
(assert (not (and q_0_0 q_1_1)))
(assert (not (and q_0_0 q_1_2)))
(assert (not (and q_0_0 q_1_3)))
(assert (not (and q_0_0 q_1_5)))
(assert (not (and q_0_0 q_2_0)))
(assert (not (and q_0_0 q_2_1)))
(assert (not (and q_0_0 q_2_2)))
(assert (not (and q_0_0 q_2_3)))
(assert (not (and q_0_0 q_2_4)))
(assert (not (and q_0_0 q_2_5)))
(assert (not (and q_0_0 q_3_0)))
(assert (not (and q_0_0 q_3_1)))
(assert (not (and q_0_0 q_3_2)))
(assert (not (and q_0_0 q_3_3)))
(assert (not (and q_0_0 q_3_4)))
(assert (not (and q_0_0 q_4_0)))
(assert (not (and q_0_0 q_4_1)))
(assert (not (and q_0_0 q_4_3)))
(assert (not (and q_0_0 q_4_4)))
(assert (not (and q_0_0 q_5_3)))
(assert (not (and q_0_0 q_5_4)))
(assert (not (and q_0_1 q_0_5)))
(assert (not (and q_0_1 q_1_0)))
(assert (not (and q_0_1 q_1_1)))
(assert (not (and q_0_1 q_1_2)))
(assert (not (and q_0_1 q_1_3)))
(assert (not (and q_0_1 q_1_5)))
(assert (not (and q_0_1 q_2_0)))
(assert (not (and q_0_1 q_2_1)))
(assert (not (and q_0_1 q_2_2)))
(assert (not (and q_0_1 q_2_3)))
(assert (not (and q_0_1 q_2_4)))
(assert (not (and q_0_1 q_2_5)))
(assert (not (and q_0_1 q_3_0)))
(assert (not (and q_0_1 q_3_1)))
(assert (not (and q_0_1 q_3_2)))
(assert (not (and q_0_1 q_3_3)))
(assert (not (and q_0_1 q_3_4)))
(assert (not (and q_0_1 q_4_0)))
(assert (not (and q_0_1 q_4_1)))
(assert (not (and q_0_1 q_4_3)))
(assert (not (and q_0_1 q_4_4)))
(assert (not (and q_0_1 q_5_3)))
(assert (not (and q_0_1 q_5_4)))
(assert (not (and q_0_5 q_1_0)))
(assert (not (and q_0_5 q_1_1)))
(assert (not (and q_0_5 q_1_2)))
(assert (not (and q_0_5 q_1_3)))
(assert (not (and q_0_5 q_1_5)))
(assert (not (and q_0_5 q_2_0)))
(assert (not (and q_0_5 q_2_1)))
(assert (not (and q_0_5 q_2_2)))
(assert (not (and q_0_5 q_2_3)))
(assert (not (and q_0_5 q_2_4)))
(assert (not (and q_0_5 q_2_5)))
(assert (not (and q_0_5 q_3_0)))
(assert (not (and q_0_5 q_3_1)))
(assert (not (and q_0_5 q_3_2)))
(assert (not (and q_0_5 q_3_3)))
(assert (not (and q_0_5 q_3_4)))
(assert (not (and q_0_5 q_4_0)))
(assert (not (and q_0_5 q_4_1)))
(assert (not (and q_0_5 q_4_3)))
(assert (not (and q_0_5 q_4_4)))
(assert (not (and q_0_5 q_5_3)))
(assert (not (and q_0_5 q_5_4)))
(assert (not (and q_1_0 q_1_1)))
(assert (not (and q_1_0 q_1_2)))
(assert (not (and q_1_0 q_1_3)))
(assert (not (and q_1_0 q_1_5)))
(assert (not (and q_1_0 q_2_0)))
(assert (not (and q_1_0 q_2_1)))
(assert (not (and q_1_0 q_2_2)))
(assert (not (and q_1_0 q_2_3)))
(assert (not (and q_1_0 q_2_4)))
(assert (not (and q_1_0 q_2_5)))
(assert (not (and q_1_0 q_3_0)))
(assert (not (and q_1_0 q_3_1)))
(assert (not (and q_1_0 q_3_2)))
(assert (not (and q_1_0 q_3_3)))
(assert (not (and q_1_0 q_3_4)))
(assert (not (and q_1_0 q_4_0)))
(assert (not (and q_1_0 q_4_1)))
(assert (not (and q_1_0 q_4_3)))
(assert (not (and q_1_0 q_4_4)))
(assert (not (and q_1_0 q_5_3)))
(assert (not (and q_1_0 q_5_4)))
(assert (not (and q_1_1 q_1_2)))
(assert (not (and q_1_1 q_1_3)))
(assert (not (and q_1_1 q_1_5)))
(assert (not (and q_1_1 q_2_0)))
(assert (not (and q_1_1 q_2_1)))
(assert (not (and q_1_1 q_2_2)))
(assert (not (and q_1_1 q_2_3)))
(assert (not (and q_1_1 q_2_4)))
(assert (not (and q_1_1 q_2_5)))
(assert (not (and q_1_1 q_3_0)))
(assert (not (and q_1_1 q_3_1)))
(assert (not (and q_1_1 q_3_2)))
(assert (not (and q_1_1 q_3_3)))
(assert (not (and q_1_1 q_3_4)))
(assert (not (and q_1_1 q_4_0)))
(assert (not (and q_1_1 q_4_1)))
(assert (not (and q_1_1 q_4_3)))
(assert (not (and q_1_1 q_4_4)))
(assert (not (and q_1_1 q_5_3)))
(assert (not (and q_1_1 q_5_4)))
(assert (not (and q_1_2 q_1_3)))
(assert (not (and q_1_2 q_1_5)))
(assert (not (and q_1_2 q_2_0)))
(assert (not (and q_1_2 q_2_1)))
(assert (not (and q_1_2 q_2_2)))
(assert (not (and q_1_2 q_2_3)))
(assert (not (and q_1_2 q_2_4)))
(assert (not (and q_1_2 q_2_5)))
(assert (not (and q_1_2 q_3_0)))
(assert (not (and q_1_2 q_3_1)))
(assert (not (and q_1_2 q_3_2)))
(assert (not (and q_1_2 q_3_3)))
(assert (not (and q_1_2 q_3_4)))
(assert (not (and q_1_2 q_4_0)))
(assert (not (and q_1_2 q_4_1)))
(assert (not (and q_1_2 q_4_3)))
(assert (not (and q_1_2 q_4_4)))
(assert (not (and q_1_2 q_5_3)))
(assert (not (and q_1_2 q_5_4)))
(assert (not (and q_1_3 q_1_5)))
(assert (not (and q_1_3 q_2_0)))
(assert (not (and q_1_3 q_2_1)))
(assert (not (and q_1_3 q_2_2)))
(assert (not (and q_1_3 q_2_3)))
(assert (not (and q_1_3 q_2_4)))
(assert (not (and q_1_3 q_2_5)))
(assert (not (and q_1_3 q_3_0)))
(assert (not (and q_1_3 q_3_1)))
(assert (not (and q_1_3 q_3_2)))
(assert (not (and q_1_3 q_3_3)))
(assert (not (and q_1_3 q_3_4)))
(assert (not (and q_1_3 q_4_0)))
(assert (not (and q_1_3 q_4_1)))
(assert (not (and q_1_3 q_4_3)))
(assert (not (and q_1_3 q_4_4)))
(assert (not (and q_1_3 q_5_3)))
(assert (not (and q_1_3 q_5_4)))
(assert (not (and q_1_5 q_2_0)))
(assert (not (and q_1_5 q_2_1)))
(assert (not (and q_1_5 q_2_2)))
(assert (not (and q_1_5 q_2_3)))
(assert (not (and q_1_5 q_2_4)))
(assert (not (and q_1_5 q_2_5)))
(assert (not (and q_1_5 q_3_0)))
(assert (not (and q_1_5 q_3_1)))
(assert (not (and q_1_5 q_3_2)))
(assert (not (and q_1_5 q_3_3)))
(assert (not (and q_1_5 q_3_4)))
(assert (not (and q_1_5 q_4_0)))
(assert (not (and q_1_5 q_4_1)))
(assert (not (and q_1_5 q_4_3)))
(assert (not (and q_1_5 q_4_4)))
(assert (not (and q_1_5 q_5_3)))
(assert (not (and q_1_5 q_5_4)))
(assert (not (and q_2_0 q_2_1)))
(assert (not (and q_2_0 q_2_2)))
(assert (not (and q_2_0 q_2_3)))
(assert (not (and q_2_0 q_2_4)))
(assert (not (and q_2_0 q_2_5)))
(assert (not (and q_2_0 q_3_0)))
(assert (not (and q_2_0 q_3_1)))
(assert (not (and q_2_0 q_3_2)))
(assert (not (and q_2_0 q_3_3)))
(assert (not (and q_2_0 q_3_4)))
(assert (not (and q_2_0 q_4_0)))
(assert (not (and q_2_0 q_4_1)))
(assert (not (and q_2_0 q_4_3)))
(assert (not (and q_2_0 q_4_4)))
(assert (not (and q_2_0 q_5_3)))
(assert (not (and q_2_0 q_5_4)))
(assert (not (and q_2_1 q_2_2)))
(assert (not (and q_2_1 q_2_3)))
(assert (not (and q_2_1 q_2_4)))
(assert (not (and q_2_1 q_2_5)))
(assert (not (and q_2_1 q_3_0)))
(assert (not (and q_2_1 q_3_1)))
(assert (not (and q_2_1 q_3_2)))
(assert (not (and q_2_1 q_3_3)))
(assert (not (and q_2_1 q_3_4)))
(assert (not (and q_2_1 q_4_0)))
(assert (not (and q_2_1 q_4_1)))
(assert (not (and q_2_1 q_4_3)))
(assert (not (and q_2_1 q_4_4)))
(assert (not (and q_2_1 q_5_3)))
(assert (not (and q_2_1 q_5_4)))
(assert (not (and q_2_2 q_2_3)))
(assert (not (and q_2_2 q_2_4)))
(assert (not (and q_2_2 q_2_5)))
(assert (not (and q_2_2 q_3_0)))
(assert (not (and q_2_2 q_3_1)))
(assert (not (and q_2_2 q_3_2)))
(assert (not (and q_2_2 q_3_3)))
(assert (not (and q_2_2 q_3_4)))
(assert (not (and q_2_2 q_4_0)))
(assert (not (and q_2_2 q_4_1)))
(assert (not (and q_2_2 q_4_3)))
(assert (not (and q_2_2 q_4_4)))
(assert (not (and q_2_2 q_5_3)))
(assert (not (and q_2_2 q_5_4)))
(assert (not (and q_2_3 q_2_4)))
(assert (not (and q_2_3 q_2_5)))
(assert (not (and q_2_3 q_3_0)))
(assert (not (and q_2_3 q_3_1)))
(assert (not (and q_2_3 q_3_2)))
(assert (not (and q_2_3 q_3_3)))
(assert (not (and q_2_3 q_3_4)))
(assert (not (and q_2_3 q_4_0)))
(assert (not (and q_2_3 q_4_1)))
(assert (not (and q_2_3 q_4_3)))
(assert (not (and q_2_3 q_4_4)))
(assert (not (and q_2_3 q_5_3)))
(assert (not (and q_2_3 q_5_4)))
(assert (not (and q_2_4 q_2_5)))
(assert (not (and q_2_4 q_3_0)))
(assert (not (and q_2_4 q_3_1)))
(assert (not (and q_2_4 q_3_2)))
(assert (not (and q_2_4 q_3_3)))
(assert (not (and q_2_4 q_3_4)))
(assert (not (and q_2_4 q_4_0)))
(assert (not (and q_2_4 q_4_1)))
(assert (not (and q_2_4 q_4_3)))
(assert (not (and q_2_4 q_4_4)))
(assert (not (and q_2_4 q_5_3)))
(assert (not (and q_2_4 q_5_4)))
(assert (not (and q_2_5 q_3_0)))
(assert (not (and q_2_5 q_3_1)))
(assert (not (and q_2_5 q_3_2)))
(assert (not (and q_2_5 q_3_3)))
(assert (not (and q_2_5 q_3_4)))
(assert (not (and q_2_5 q_4_0)))
(assert (not (and q_2_5 q_4_1)))
(assert (not (and q_2_5 q_4_3)))
(assert (not (and q_2_5 q_4_4)))
(assert (not (and q_2_5 q_5_3)))
(assert (not (and q_2_5 q_5_4)))
(assert (not (and q_3_0 q_3_1)))
(assert (not (and q_3_0 q_3_2)))
(assert (not (and q_3_0 q_3_3)))
(assert (not (and q_3_0 q_3_4)))
(assert (not (and q_3_0 q_4_0)))
(assert (not (and q_3_0 q_4_1)))
(assert (not (and q_3_0 q_4_3)))
(assert (not (and q_3_0 q_4_4)))
(assert (not (and q_3_0 q_5_3)))
(assert (not (and q_3_0 q_5_4)))
(assert (not (and q_3_1 q_3_2)))
(assert (not (and q_3_1 q_3_3)))
(assert (not (and q_3_1 q_3_4)))
(assert (not (and q_3_1 q_4_0)))
(assert (not (and q_3_1 q_4_1)))
(assert (not (and q_3_1 q_4_3)))
(assert (not (and q_3_1 q_4_4)))
(assert (not (and q_3_1 q_5_3)))
(assert (not (and q_3_1 q_5_4)))
(assert (not (and q_3_2 q_3_3)))
(assert (not (and q_3_2 q_3_4)))
(assert (not (and q_3_2 q_4_0)))
(assert (not (and q_3_2 q_4_1)))
(assert (not (and q_3_2 q_4_3)))
(assert (not (and q_3_2 q_4_4)))
(assert (not (and q_3_2 q_5_3)))
(assert (not (and q_3_2 q_5_4)))
(assert (not (and q_3_3 q_3_4)))
(assert (not (and q_3_3 q_4_0)))
(assert (not (and q_3_3 q_4_1)))
(assert (not (and q_3_3 q_4_3)))
(assert (not (and q_3_3 q_4_4)))
(assert (not (and q_3_3 q_5_3)))
(assert (not (and q_3_3 q_5_4)))
(assert (not (and q_3_4 q_4_0)))
(assert (not (and q_3_4 q_4_1)))
(assert (not (and q_3_4 q_4_3)))
(assert (not (and q_3_4 q_4_4)))
(assert (not (and q_3_4 q_5_3)))
(assert (not (and q_3_4 q_5_4)))
(assert (not (and q_4_0 q_4_1)))
(assert (not (and q_4_0 q_4_3)))
(assert (not (and q_4_0 q_4_4)))
(assert (not (and q_4_0 q_5_3)))
(assert (not (and q_4_0 q_5_4)))
(assert (not (and q_4_1 q_4_3)))
(assert (not (and q_4_1 q_4_4)))
(assert (not (and q_4_1 q_5_3)))
(assert (not (and q_4_1 q_5_4)))
(assert (not (and q_4_3 q_4_4)))
(assert (not (and q_4_3 q_5_3)))
(assert (not (and q_4_3 q_5_4)))
(assert (not (and q_4_4 q_5_3)))
(assert (not (and q_4_4 q_5_4)))
(assert (not (and q_5_3 q_5_4)))
(assert (or q_5_5 q_6_4 q_6_5 q_6_6))
(assert (not (and q_5_5 q_6_4)))
(assert (not (and q_5_5 q_6_5)))
(assert (not (and q_5_5 q_6_6)))
(assert (not (and q_6_4 q_6_5)))
(assert (not (and q_6_4 q_6_6)))
(assert (not (and q_6_5 q_6_6)))
(assert (or q_5_0 q_5_1 q_6_0 q_6_1))
(assert (not (and q_5_0 q_5_1)))
(assert (not (and q_5_0 q_6_0)))
(assert (not (and q_5_0 q_6_1)))
(assert (not (and q_5_1 q_6_0)))
(assert (not (and q_5_1 q_6_1)))
(assert (not (and q_6_0 q_6_1)))
(assert (or q_4_2 q_5_2 q_6_2 q_6_3))
(assert (not (and q_4_2 q_5_2)))
(assert (not (and q_4_2 q_6_2)))
(assert (not (and q_4_2 q_6_3)))
(assert (not (and q_5_2 q_6_2)))
(assert (not (and q_5_2 q_6_3)))
(assert (not (and q_6_2 q_6_3)))
(assert (or q_0_2 q_0_3 q_0_4 q_1_4))
(assert (not (and q_0_2 q_0_3)))
(assert (not (and q_0_2 q_0_4)))
(assert (not (and q_0_2 q_1_4)))
(assert (not (and q_0_3 q_0_4)))
(assert (not (and q_0_3 q_1_4)))
(assert (not (and q_0_4 q_1_4)))
(assert (or q_3_5 q_4_5 q_4_6 q_5_6))
(assert (not (and q_3_5 q_4_5)))
(assert (not (and q_3_5 q_4_6)))
(assert (not (and q_3_5 q_5_6)))
(assert (not (and q_4_5 q_4_6)))
(assert (not (and q_4_5 q_5_6)))
(assert (not (and q_4_6 q_5_6)))
(assert (or q_0_6 q_1_6 q_2_6 q_3_6))
(assert (not (and q_0_6 q_1_6)))
(assert (not (and q_0_6 q_2_6)))
(assert (not (and q_0_6 q_3_6)))
(assert (not (and q_1_6 q_2_6)))
(assert (not (and q_1_6 q_3_6)))
(assert (not (and q_2_6 q_3_6)))
(assert (not (and q_0_0 q_0_1)))
(assert (not (and q_0_0 q_1_0)))
(assert (not (and q_0_0 q_1_1)))
(assert (not (and q_0_1 q_0_2)))
(assert (not (and q_0_1 q_1_0)))
(assert (not (and q_0_1 q_1_1)))
(assert (not (and q_0_1 q_1_2)))
(assert (not (and q_0_2 q_0_3)))
(assert (not (and q_0_2 q_1_1)))
(assert (not (and q_0_2 q_1_2)))
(assert (not (and q_0_2 q_1_3)))
(assert (not (and q_0_3 q_0_4)))
(assert (not (and q_0_3 q_1_2)))
(assert (not (and q_0_3 q_1_3)))
(assert (not (and q_0_3 q_1_4)))
(assert (not (and q_0_4 q_0_5)))
(assert (not (and q_0_4 q_1_3)))
(assert (not (and q_0_4 q_1_4)))
(assert (not (and q_0_4 q_1_5)))
(assert (not (and q_0_5 q_0_6)))
(assert (not (and q_0_5 q_1_4)))
(assert (not (and q_0_5 q_1_5)))
(assert (not (and q_0_5 q_1_6)))
(assert (not (and q_0_6 q_1_5)))
(assert (not (and q_0_6 q_1_6)))
(assert (not (and q_1_0 q_1_1)))
(assert (not (and q_1_0 q_2_0)))
(assert (not (and q_1_0 q_2_1)))
(assert (not (and q_1_1 q_1_2)))
(assert (not (and q_1_1 q_2_0)))
(assert (not (and q_1_1 q_2_1)))
(assert (not (and q_1_1 q_2_2)))
(assert (not (and q_1_2 q_1_3)))
(assert (not (and q_1_2 q_2_1)))
(assert (not (and q_1_2 q_2_2)))
(assert (not (and q_1_2 q_2_3)))
(assert (not (and q_1_3 q_1_4)))
(assert (not (and q_1_3 q_2_2)))
(assert (not (and q_1_3 q_2_3)))
(assert (not (and q_1_3 q_2_4)))
(assert (not (and q_1_4 q_1_5)))
(assert (not (and q_1_4 q_2_3)))
(assert (not (and q_1_4 q_2_4)))
(assert (not (and q_1_4 q_2_5)))
(assert (not (and q_1_5 q_1_6)))
(assert (not (and q_1_5 q_2_4)))
(assert (not (and q_1_5 q_2_5)))
(assert (not (and q_1_5 q_2_6)))
(assert (not (and q_1_6 q_2_5)))
(assert (not (and q_1_6 q_2_6)))
(assert (not (and q_2_0 q_2_1)))
(assert (not (and q_2_0 q_3_0)))
(assert (not (and q_2_0 q_3_1)))
(assert (not (and q_2_1 q_2_2)))
(assert (not (and q_2_1 q_3_0)))
(assert (not (and q_2_1 q_3_1)))
(assert (not (and q_2_1 q_3_2)))
(assert (not (and q_2_2 q_2_3)))
(assert (not (and q_2_2 q_3_1)))
(assert (not (and q_2_2 q_3_2)))
(assert (not (and q_2_2 q_3_3)))
(assert (not (and q_2_3 q_2_4)))
(assert (not (and q_2_3 q_3_2)))
(assert (not (and q_2_3 q_3_3)))
(assert (not (and q_2_3 q_3_4)))
(assert (not (and q_2_4 q_2_5)))
(assert (not (and q_2_4 q_3_3)))
(assert (not (and q_2_4 q_3_4)))
(assert (not (and q_2_4 q_3_5)))
(assert (not (and q_2_5 q_2_6)))
(assert (not (and q_2_5 q_3_4)))
(assert (not (and q_2_5 q_3_5)))
(assert (not (and q_2_5 q_3_6)))
(assert (not (and q_2_6 q_3_5)))
(assert (not (and q_2_6 q_3_6)))
(assert (not (and q_3_0 q_3_1)))
(assert (not (and q_3_0 q_4_0)))
(assert (not (and q_3_0 q_4_1)))
(assert (not (and q_3_1 q_3_2)))
(assert (not (and q_3_1 q_4_0)))
(assert (not (and q_3_1 q_4_1)))
(assert (not (and q_3_1 q_4_2)))
(assert (not (and q_3_2 q_3_3)))
(assert (not (and q_3_2 q_4_1)))
(assert (not (and q_3_2 q_4_2)))
(assert (not (and q_3_2 q_4_3)))
(assert (not (and q_3_3 q_3_4)))
(assert (not (and q_3_3 q_4_2)))
(assert (not (and q_3_3 q_4_3)))
(assert (not (and q_3_3 q_4_4)))
(assert (not (and q_3_4 q_3_5)))
(assert (not (and q_3_4 q_4_3)))
(assert (not (and q_3_4 q_4_4)))
(assert (not (and q_3_4 q_4_5)))
(assert (not (and q_3_5 q_3_6)))
(assert (not (and q_3_5 q_4_4)))
(assert (not (and q_3_5 q_4_5)))
(assert (not (and q_3_5 q_4_6)))
(assert (not (and q_3_6 q_4_5)))
(assert (not (and q_3_6 q_4_6)))
(assert (not (and q_4_0 q_4_1)))
(assert (not (and q_4_0 q_5_0)))
(assert (not (and q_4_0 q_5_1)))
(assert (not (and q_4_1 q_4_2)))
(assert (not (and q_4_1 q_5_0)))
(assert (not (and q_4_1 q_5_1)))
(assert (not (and q_4_1 q_5_2)))
(assert (not (and q_4_2 q_4_3)))
(assert (not (and q_4_2 q_5_1)))
(assert (not (and q_4_2 q_5_2)))
(assert (not (and q_4_2 q_5_3)))
(assert (not (and q_4_3 q_4_4)))
(assert (not (and q_4_3 q_5_2)))
(assert (not (and q_4_3 q_5_3)))
(assert (not (and q_4_3 q_5_4)))
(assert (not (and q_4_4 q_4_5)))
(assert (not (and q_4_4 q_5_3)))
(assert (not (and q_4_4 q_5_4)))
(assert (not (and q_4_4 q_5_5)))
(assert (not (and q_4_5 q_4_6)))
(assert (not (and q_4_5 q_5_4)))
(assert (not (and q_4_5 q_5_5)))
(assert (not (and q_4_5 q_5_6)))
(assert (not (and q_4_6 q_5_5)))
(assert (not (and q_4_6 q_5_6)))
(assert (not (and q_5_0 q_5_1)))
(assert (not (and q_5_0 q_6_0)))
(assert (not (and q_5_0 q_6_1)))
(assert (not (and q_5_1 q_5_2)))
(assert (not (and q_5_1 q_6_0)))
(assert (not (and q_5_1 q_6_1)))
(assert (not (and q_5_1 q_6_2)))
(assert (not (and q_5_2 q_5_3)))
(assert (not (and q_5_2 q_6_1)))
(assert (not (and q_5_2 q_6_2)))
(assert (not (and q_5_2 q_6_3)))
(assert (not (and q_5_3 q_5_4)))
(assert (not (and q_5_3 q_6_2)))
(assert (not (and q_5_3 q_6_3)))
(assert (not (and q_5_3 q_6_4)))
(assert (not (and q_5_4 q_5_5)))
(assert (not (and q_5_4 q_6_3)))
(assert (not (and q_5_4 q_6_4)))
(assert (not (and q_5_4 q_6_5)))
(assert (not (and q_5_5 q_5_6)))
(assert (not (and q_5_5 q_6_4)))
(assert (not (and q_5_5 q_6_5)))
(assert (not (and q_5_5 q_6_6)))
(assert (not (and q_5_6 q_6_5)))
(assert (not (and q_5_6 q_6_6)))
(assert (not (and q_6_0 q_6_1)))
(assert (not (and q_6_1 q_6_2)))
(assert (not (and q_6_2 q_6_3)))
(assert (not (and q_6_3 q_6_4)))
(assert (not (and q_6_4 q_6_5)))
(assert (not (and q_6_5 q_6_6)))
(check-sat)
(get-model)

02 / representations

Same semantics, different leverage.

Boolean grid

q[r,c] ∈ Bool

Contract: a cell is selected or not; all requested partitions are exact-one.

Trade-off: most transparent for audits and regional rules; 49 variables here, quadratic pairwise exclusions.

Integer per row

col[r] ∈ 0..6

Contract: each row chooses one column; distinctness captures columns.

Trade-off: compact for classical Queens; regions and conditional rules need element/lookup constraints.

Conflict graph

∀(u,v)∈E. xᵤ + xᵥ ≤ 1

Contract: vertices are choices; edges are incompatible pairs; partitions encode coverage.

Trade-off: makes sparse conflicts legible; loses row/column geometry without annotations.

03 / transfer lab

Translate the structure, not the chessboard.

Assignment

Variables: person × role choices. Partitions: each person and role. Conflicts: unavailable pairs or incompatible certifications. Objective: maximize fit or minimize cost.

Scheduling

Variables: job × time-slot choices. Partitions: each job and resource. Conflicts: overlap, setup, adjacency. Objective: minimize makespan or lateness.

Portfolio / mandate

Variables: mandate × instrument selections. Partitions: mandates, sleeves, exposure buckets. Conflicts: concentration and policy exclusions. Objective: maximize expected utility under limits.

Configuration / verification

Variables: component × setting choices. Partitions: required interfaces and zones. Conflicts: incompatible versions or safety rules. Objective: feasible configuration, then preferred cost/performance.

04 / solver context

How Z3 fits

Z3 is a general-purpose satisfiability modulo theories solver. In a Boolean encoding, a SAT-style engine proposes assignments and learns from conflicts; theory solvers add disciplined reasoning for domains such as arithmetic, arrays, and bit-vectors. CDCL(T) is the useful conceptual pipeline: encode a contract → search a Boolean skeleton → check theory consistency → learn a blocking explanation → return SAT with a model, UNSAT, or UNKNOWN. This page’s trace is deliberately a small transparent backtracker, not a reconstruction of that internal process. For the real mechanics, a recorded conflict-driven run with learned clauses and Z3’s measured engine route, read How Z3 solves Queens.

05 / research ledger

Claims with a trail.

The LinkedIn Queens variant used here requires exactly one queen in every row, column, and coloured region, while forbidding queens in adjacent cells, including orthogonally and diagonally. Because the row and column equations already exclude orthogonal neighbors, only the 72 local diagonal pairs add nonredundant exclusions when both those rule families are active. Classical N-Queens instead forbids attacks across full diagonals.

Z3: An Efficient SMT Solver — original architecture paper.
Programming Z3 and Z3 Internals — primary technical references.
Z3 Guide: propositional logic and arithmetic optimization.
LinkedIn Queens help — game rule source.
User-friendly explanations for constraint programming and Visualization for Structured Constraint Satisfaction Problems.