doctest failure in src/example_sudoku_solver.md:15-21 ```jldoctest label4; output = false using Satisfiability # Create a 9x9 matrix of integer variables (for the Sudoku grid) @satvariable(X[1:9, 1:9], Int); # output ``` Subexpression: using Satisfiability # Create a 9x9 matrix of integer variables (for the Sudoku grid) @satvariable(X[1:9, 1:9], Int); Evaluated output: 9×9 Matrix{IntExpr}: X_1_1 X_1_2 X_1_3 X_1_4 X_1_5 X_1_6 X_1_7 X_1_8 X_1_9 X_2_1 X_2_2 X_2_3 X_2_4 X_2_5 X_2_6 X_2_7 X_2_8 X_2_9 X_3_1 X_3_2 X_3_3 X_3_4 X_3_5 X_3_6 X_3_7 X_3_8 X_3_9 X_4_1 X_4_2 X_4_3 X_4_4 X_4_5 X_4_6 X_4_7 X_4_8 X_4_9 X_5_1 X_5_2 X_5_3 X_5_4 X_5_5 X_5_6 X_5_7 X_5_8 X_5_9 X_6_1 X_6_2 X_6_3 X_6_4 X_6_5 X_6_6 X_6_7 X_6_8 X_6_9 X_7_1 X_7_2 X_7_3 X_7_4 X_7_5 X_7_6 X_7_7 X_7_8 X_7_9 X_8_1 X_8_2 X_8_3 X_8_4 X_8_5 X_8_6 X_8_7 X_8_8 X_8_9 X_9_1 X_9_2 X_9_3 X_9_4 X_9_5 X_9_6 X_9_7 X_9_8 X_9_9 Expected output: diff = Warning: Diff output requires color. 9×9 Matrix{IntExpr}: X_1_1 X_1_2 X_1_3 X_1_4 X_1_5 X_1_6 X_1_7 X_1_8 X_1_9 X_2_1 X_2_2 X_2_3 X_2_4 X_2_5 X_2_6 X_2_7 X_2_8 X_2_9 X_3_1 X_3_2 X_3_3 X_3_4 X_3_5 X_3_6 X_3_7 X_3_8 X_3_9 X_4_1 X_4_2 X_4_3 X_4_4 X_4_5 X_4_6 X_4_7 X_4_8 X_4_9 X_5_1 X_5_2 X_5_3 X_5_4 X_5_5 X_5_6 X_5_7 X_5_8 X_5_9 X_6_1 X_6_2 X_6_3 X_6_4 X_6_5 X_6_6 X_6_7 X_6_8 X_6_9 X_7_1 X_7_2 X_7_3 X_7_4 X_7_5 X_7_6 X_7_7 X_7_8 X_7_9 X_8_1 X_8_2 X_8_3 X_8_4 X_8_5 X_8_6 X_8_7 X_8_8 X_8_9 X_9_1 X_9_2 X_9_3 X_9_4 X_9_5 X_9_6 X_9_7 X_9_8 X_9_9

doctest failure in src/example_sudoku_solver.md:30-47 ```jldoctest label4; output = false # Each cell contains a value between 1 and 9 cells_c = [and(1 <= X[i, j], X[i, j] <= 9) for i in 1:9, j in 1:9]; # Each row contains distinct values rows_c = [distinct(X[i, :]) for i in 1:9]; # Each column contains distinct values cols_c = [distinct(X[:, j]) for j in 1:9]; # Each 3x3 square contains distinct values sq_c = [distinct([X[3*i0 + i, 3*j0 + j] for i in 1:3, j in 1:3]) for i0 in 0:2, j0 in 0:2]; # Combine all constraints into one list sudoku_c = vcat(cells_c..., rows_c..., cols_c..., sq_c...); # output ``` Subexpression: # Each cell contains a value between 1 and 9 cells_c = [and(1 <= X[i, j], X[i, j] <= 9) for i in 1:9, j in 1:9]; # Each row contains distinct values rows_c = [distinct(X[i, :]) for i in 1:9]; # Each column contains distinct values cols_c = [distinct(X[:, j]) for j in 1:9]; # Each 3x3 square contains distinct values sq_c = [distinct([X[3*i0 + i, 3*j0 + j] for i in 1:3, j in 1:3]) for i0 in 0:2, j0 in 0:2]; # Combine all constraints into one list sudoku_c = vcat(cells_c..., rows_c..., cols_c..., sq_c...); Evaluated output: 108-element Vector{BoolExpr}: and_c744d09714c6b14d | leq_645af7f208a4da3c | | X_1_1 | | const_9 = 9 | leq_b9cca733c2dec3a6 | | const_1 = 1 | | X_1_1 and_39b2ec5c0a615082 | leq_77064d0c37cef03b | | X_2_1 | | const_9 = 9 | leq_7c949875888eaac | | const_1 = 1 | | X_2_1 and_9057b9b839281483 | leq_643a45c9c4210ebd | | const_1 = 1 | | X_3_1 | leq_911d7fb062ce69ab | | X_3_1 | | const_9 = 9 and_6526834eb65fd333 | leq_3d535577b3d0b8c8 | | X_4_1 | | const_9 = 9 | leq_eeaf732a5182e069 | | const_1 = 1 | | X_4_1 and_d9478c60aa64e7ef | leq_9b2ca968bc0ed01 | | const_1 = 1 | | X_5_1 | leq_d559424db9872568 | | X_5_1 | | const_9 = 9 and_cbf22e358992c26c | leq_a0655f0f4aa23067 | | X_6_1 | | const_9 = 9 | leq_f4b1ab179c46d645 | | const_1 = 1 | | X_6_1 and_c8a8bbef41ca3f99 | leq_adf3e69c17355765 | | const_1 = 1 | | X_7_1 | leq_beb8f736c1044207 | | X_7_1 | | const_9 = 9 and_4fbec5152e86692f | leq_171cceb01a439470 | | const_1 = 1 | | X_8_1 | leq_a7070fac90ae789a | | X_8_1 | | const_9 = 9 and_7dc45ca7c107f13d | leq_a4c536ae7698603f | | const_1 = 1 | | X_9_1 | leq_d5c1534f0ecfa75f | | X_9_1 | | const_9 = 9 and_ba21f78747952015 | leq_5b23829fba9c70fd | | const_1 = 1 | | X_1_2 | leq_646aa29126778889 | | X_1_2 | | const_9 = 9 ⋮ and_3cf875017d80d7de | distinct_144b268b845b89de | | X_1_2 | | X_3_3 | distinct_16c005f5218af0e7 | | X_3_2 | | X_2_3 | distinct_194106dfc762e673 | | X_1_1 | | X_2_2 | distinct_34e8e82858755f88 | | X_2_2 | | X_2_3 | distinct_35913f068777eedf | | X_2_2 | | X_3_3 | distinct_35c637a2e77c2391 | | X_1_1 | | X_3_1 | distinct_431fbbf57a6c0a70 | | X_2_2 | | X_1_3 | distinct_447823859ee1f311 | | X_2_2 | | X_3_2 | distinct_4b32fb74d2e3c238 | | X_3_1 | | X_2_2 | distinct_5320a508d8f555b0 | | X_1_2 | | X_1_3 | distinct_5d3c50dcc88ac479 | | X_2_1 | | X_1_3 | distinct_6f0bf6d619426707 | | X_1_2 | | X_2_2 | distinct_72fed0d579901b1f | | X_2_1 | | X_3_3 | distinct_7a8b3dcb10b7a496 | | X_1_2 | | X_2_3 | distinct_829d2124ff9cc818 | | X_1_1 | | X_1_2 | distinct_87863bb57070b750 | | X_2_3 | | X_3_3 | distinct_91c83b9372df210d | | X_1_3 | | X_3_3 | distinct_9c8d54d417e34a5f | | X_3_2 | | X_3_3 | distinct_9cec02e49b01629d | | X_1_1 | | X_3_3 | distinct_9d35ae4a473e2a14 | | X_3_1 | | X_2_3 | distinct_9da45cc1f8e153d5 | | X_1_1 | | X_2_1 | distinct_a283cefdc90eb145 | | X_2_1 | | X_1_2 | distinct_a7a466c6669b9f05 | | X_1_1 | | X_1_3 | distinct_aa0230e322f0b313 | | X_1_1 | | X_3_2 | distinct_aa4276f692fcb777 | | X_1_1 | | X_2_3 | distinct_afb66a9ec3621ee8 | | X_3_1 | | X_3_3 | distinct_b34bb7db9e6e2af6 | | X_2_1 | | X_2_3 | distinct_b97b9347a692deea | | X_1_2 | | X_3_2 | distinct_bbce2e895cf15674 | | X_2_1 | | X_2_2 | distinct_c21bf85847b5d82b

doctest failure in src/example_sudoku_solver.md:54-68 ```jldoctest label4; output = false instance = [ (5, 3, 0, 0, 7, 0, 0, 0, 0), (6, 0, 0, 1, 9, 5, 0, 0, 0), (0, 9, 8, 0, 0, 0, 0, 6, 0), (8, 0, 0, 0, 6, 0, 0, 0, 3), (4, 0, 0, 8, 0, 3, 0, 0, 1), (7, 0, 0, 0, 2, 0, 0, 0, 6), (0, 6, 0, 0, 0, 0, 2, 8, 0), (0, 0, 0, 4, 1, 9, 0, 0, 5), (0, 0, 0, 0, 8, 0, 0, 7, 9) ]; # output ``` Subexpression: instance = [ (5, 3, 0, 0, 7, 0, 0, 0, 0), (6, 0, 0, 1, 9, 5, 0, 0, 0), (0, 9, 8, 0, 0, 0, 0, 6, 0), (8, 0, 0, 0, 6, 0, 0, 0, 3), (4, 0, 0, 8, 0, 3, 0, 0, 1), (7, 0, 0, 0, 2, 0, 0, 0, 6), (0, 6, 0, 0, 0, 0, 2, 8, 0), (0, 0, 0, 4, 1, 9, 0, 0, 5), (0, 0, 0, 0, 8, 0, 0, 7, 9) ]; Evaluated output: 9-element Vector{NTuple{9, Int64}}: (5, 3, 0, 0, 7, 0, 0, 0, 0) (6, 0, 0, 1, 9, 5, 0, 0, 0) (0, 9, 8, 0, 0, 0, 0, 6, 0) (8, 0, 0, 0, 6, 0, 0, 0, 3) (4, 0, 0, 8, 0, 3, 0, 0, 1) (7, 0, 0, 0, 2, 0, 0, 0, 6) (0, 6, 0, 0, 0, 0, 2, 8, 0) (0, 0, 0, 4, 1, 9, 0, 0, 5) (0, 0, 0, 0, 8, 0, 0, 7, 9) Expected output: diff = Warning: Diff output requires color. 9-element Vector{NTuple{9, Int64}}: (5, 3, 0, 0, 7, 0, 0, 0, 0) (6, 0, 0, 1, 9, 5, 0, 0, 0) (0, 9, 8, 0, 0, 0, 0, 6, 0) (8, 0, 0, 0, 6, 0, 0, 0, 3) (4, 0, 0, 8, 0, 3, 0, 0, 1) (7, 0, 0, 0, 2, 0, 0, 0, 6) (0, 6, 0, 0, 0, 0, 2, 8, 0) (0, 0, 0, 4, 1, 9, 0, 0, 5) (0, 0, 0, 0, 8, 0, 0, 7, 9)

doctest failure in src/example_sudoku_solver.md:75-82 ```jldoctest label4; output = false # Constraints to set the values of the cells based on the puzzle instance instance_c = [ ite(instance[i][j] == 0, X[i, j] == X[i, j], X[i, j] == instance[i][j]) for i in 1:9, j in 1:9 ]; # output ``` Subexpression: # Constraints to set the values of the cells based on the puzzle instance instance_c = [ ite(instance[i][j] == 0, X[i, j] == X[i, j], X[i, j] == instance[i][j]) for i in 1:9, j in 1:9 ]; Evaluated output: 9×9 Matrix{BoolExpr}: eq_dcf604d979b7fa47 | X_1_1 | const_5 = 5 … eq_2d017e8e50553990 | X_1_9 | X_1_9 eq_bbe7cfe32f2c86ce | X_2_1 | const_6 = 6 eq_ebc64589fcc890cc | X_2_9 | X_2_9 eq_db84c42bcfacc50e | X_3_1 | X_3_1 eq_95f73805835f69cb | X_3_9 | X_3_9 eq_d941bd305d656f1f | X_4_1 | const_8 = 8 eq_290cc45b1804d9df | X_4_9 | const_3 = 3 eq_a9de797a69e79898 | X_5_1 | const_4 = 4 eq_8ae5b89d9de60fb9 | X_5_9 | const_1 = 1 eq_36cfe09d42965739 | X_6_1 | const_7 = 7 … eq_1187474addf2ab2e | X_6_9 | const_6 = 6 eq_4fbdfd428c370ae | X_7_1 | X_7_1 eq_147e360d5715143b | X_7_9 | X_7_9 eq_7e608dc16ec3aa85 | X_8_1 | X_8_1 eq_40e977cc36265ac6 | X_8_9 | const_5 = 5 eq_350c35e834afcd83 | X_9_1 | X_9_1 eq_29b7b29789ac23ed | X_9_9 | const_9 = 9 Expected output: diff = Warning: Diff output requires color. 9×9 Matrix{BoolExpr}: eq_dcf604d979b7fa47 | X_1_1 | const_5 = 5 … eq_2d017e8e50553990 | X_1_9 | X_1_9 eq_bbe7cfe32f2c86ce | X_2_1 | const_6 = 6 eq_ebc64589fcc890cc | X_2_9 | X_2_9 eq_db84c42bcfacc50e | X_3_1 | X_3_1 eq_95f73805835f69cb | X_3_9 | X_3_9 eq_d941bd305d656f1f | X_4_1 | const_8 = 8 eq_290cc45b1804d9df | X_4_9 | const_3 = 3 eq_a9de797a69e79898 | X_5_1 | const_4 = 4 eq_8ae5b89d9de60fb9 | X_5_9 | const_1 = 1 eq_36cfe09d42965739 | X_6_1 | const_7 = 7 … eq_1187474addf2ab2e | X_6_9 | const_6 = 6 eq_4fbdfd428c370ae | X_7_1 | X_7_1 eq_147e360d5715143b | X_7_9 | X_7_9 eq_7e608dc16ec3aa85 | X_8_1 | X_8_1 eq_40e977cc36265ac6 | X_8_9 | const_5 = 5 eq_350c35e834afcd83 | X_9_1 | X_9_1 eq_29b7b29789ac23ed | X_9_9 | const_9 = 9

doctest failure in src/example_sudoku_solver.md:86-91 ```jldoctest label4; output = false # Combine the sudoku constraints and the puzzle instance constraints constraints = vcat(sudoku_c..., instance_c...); # output ``` Subexpression: # Combine the sudoku constraints and the puzzle instance constraints constraints = vcat(sudoku_c..., instance_c...); Evaluated output: 189-element Vector{BoolExpr}: and_c744d09714c6b14d | leq_645af7f208a4da3c | | X_1_1 | | const_9 = 9 | leq_b9cca733c2dec3a6 | | const_1 = 1 | | X_1_1 and_39b2ec5c0a615082 | leq_77064d0c37cef03b | | X_2_1 | | const_9 = 9 | leq_7c949875888eaac | | const_1 = 1 | | X_2_1 and_9057b9b839281483 | leq_643a45c9c4210ebd | | const_1 = 1 | | X_3_1 | leq_911d7fb062ce69ab | | X_3_1 | | const_9 = 9 and_6526834eb65fd333 | leq_3d535577b3d0b8c8 | | X_4_1 | | const_9 = 9 | leq_eeaf732a5182e069 | | const_1 = 1 | | X_4_1 and_d9478c60aa64e7ef | leq_9b2ca968bc0ed01 | | const_1 = 1 | | X_5_1 | leq_d559424db9872568 | | X_5_1 | | const_9 = 9 and_cbf22e358992c26c | leq_a0655f0f4aa23067 | | X_6_1 | | const_9 = 9 | leq_f4b1ab179c46d645 | | const_1 = 1 | | X_6_1 and_c8a8bbef41ca3f99 | leq_adf3e69c17355765 | | const_1 = 1 | | X_7_1 | leq_beb8f736c1044207 | | X_7_1 | | const_9 = 9 and_4fbec5152e86692f | leq_171cceb01a439470 | | const_1 = 1 | | X_8_1 | leq_a7070fac90ae789a | | X_8_1 | | const_9 = 9 and_7dc45ca7c107f13d | leq_a4c536ae7698603f | | const_1 = 1 | | X_9_1 | leq_d5c1534f0ecfa75f | | X_9_1 | | const_9 = 9 and_ba21f78747952015 | leq_5b23829fba9c70fd | | const_1 = 1 | | X_1_2 | leq_646aa29126778889 | | X_1_2 | | const_9 = 9 ⋮ eq_2d017e8e50553990 | X_1_9 | X_1_9 eq_ebc64589fcc890cc | X_2_9 | X_2_9 eq_95f73805835f69cb | X_3_9 | X_3_9 eq_290cc45b1804d9df | X_4_9 | const_3 = 3 eq_8ae5b89d9de60fb9 | X_5_9 | const_1 = 1 eq_1187474addf2ab2e | X_6_9 | const_6 = 6 eq_147e360d5715143b | X_7_9 | X_7_9 eq_40e977cc36265ac6 | X_8_9 | const_5 = 5 eq_29b7b29789ac23ed | X_9_9 | const_9 = 9 Expected output: diff = Warning: Diff output requires color. 189-element Vector{BoolExpr}: and_c744d09714c6b14d | leq_645af7f208a4da3c | | X_1_1 | | const_9 = 9 | leq_b9cca733c2dec3a6 | | const_1 = 1 | | X_1_1 and_39b2ec5c0a615082 | leq_77064d0c37cef03b | | X_2_1 | | const_9 = 9 | leq_7c949875888eaac | | const_1 = 1 | | X_2_1 and_9057b9b839281483 | leq_643a45c9c4210ebd | | const_1 = 1 | | X_3_1 | leq_911d7fb062ce69ab | | X_3_1 | | const_9 = 9 and_6526834eb65fd333 | leq_3d535577b3d0b8c8 | | X_4_1 | | const_9 = 9 | leq_eeaf732a5182e069 | | const_1 = 1 | | X_4_1 and_d9478c60aa64e7ef | leq_9b2ca968bc0ed01 | | const_1 = 1 | | X_5_1 | leq_d559424db9872568 | | X_5_1 | | const_9 = 9 and_cbf22e358992c26c | leq_a0655f0f4aa23067 | | X_6_1 | | const_9 = 9 | leq_f4b1ab179c46d645 | | const_1 = 1 | | X_6_1 and_c8a8bbef41ca3f99 | leq_adf3e69c17355765 | | const_1 = 1 | | X_7_1 | leq_beb8f736c1044207 | | X_7_1 | | const_9 = 9 and_4fbec5152e86692f | leq_171cceb01a439470 | | const_1 = 1 | | X_8_1 | leq_a7070fac90ae789a | | X_8_1 | | const_9 = 9 and_7dc45ca7c107f13d | leq_a4c536ae7698603f | | const_1 = 1 | | X_9_1 | leq_d5c1534f0ecfa75f | | X_9_1 | | const_9 = 9 and_ba21f78747952015 | leq_5b23829fba9c70fd | | const_1 = 1 | | X_1_2 | leq_646aa29126778889 | | X_1_2 | | const_9 = 9 ⋮ eq_2d017e8e50553990 | X_1_9 | X_1_9 eq_ebc64589fcc890cc | X_2_9 | X_2_9 eq_95f73805835f69cb | X_3_9 | X_3_9 eq_290cc45b1804d9df | X_4_9 | const_3 = 3 eq_8ae5b89d9d

doctest failure in src/example_nqueens.md:31-185 ```jldoctest label3; output = false using Satisfiability function queens(n::Int) open(Z3()) do solver # Define SAT variables for the column positions of each queen @satvariable(Q[1:n], Int) # Each queen must be in a column within {1, ..., n} val_c = [(1 ≤ Q[i]) ∧ (Q[i] ≤ n) for i in 1:n] # All queens must be in distinct columns col_c = [distinct(Q)] # No two queens can attack each other diagonally diag_c = [] for i in 1:n for j in 1:i-1 push!(diag_c, ite(i == j, true, (Q[i] - Q[j] ≠ i - j) ∧ (Q[i] - Q[j] ≠ j - i))) end end # Add all constraints to the solver for constraint in vcat(val_c, col_c, diag_c) assert!(solver,constraint) end # Solve and print all solutions num_solutions = 0 while true status, assignment = sat!(solver) if status != :SAT break end # Assign values to the variables and print the solution assign!(Q, assignment) solution = [value(Q[i]) for i in 1:n] println(solution) num_solutions += 1 # Add a constraint to exclude the current solution exclusion = or([Q[i] ≠ solution[i] for i in 1:n]...) assert!(solver, exclusion) end println("Total solutions: $num_solutions") end end queens(4) # output [2, 4, 1, 3] [3, 1, 4, 2] Total solutions: 2 queens(8) # output [6, 4, 7, 1, 3, 5, 2, 8] [5, 2, 4, 6, 8, 3, 1, 7] [6, 3, 5, 8, 1, 4, 2, 7] [6, 3, 5, 7, 1, 4, 2, 8] [3, 6, 8, 1, 4, 7, 5, 2] [4, 6, 8, 3, 1, 7, 5, 2] [6, 3, 7, 4, 1, 8, 2, 5] [3, 5, 8, 4, 1, 7, 2, 6] [4, 6, 1, 5, 2, 8, 3, 7] [4, 8, 5, 3, 1, 7, 2, 6] [5, 7, 2, 6, 3, 1, 4, 8] [4, 8, 1, 3, 6, 2, 7, 5] [5, 2, 6, 1, 7, 4, 8, 3] [8, 4, 1, 3, 6, 2, 7, 5] [4, 7, 1, 8, 5, 2, 6, 3] [3, 5, 2, 8, 6, 4, 7, 1] [4, 1, 5, 8, 6, 3, 7, 2] [4, 1, 5, 8, 2, 7, 3, 6] [5, 1, 8, 4, 2, 7, 3, 6] [6, 2, 7, 1, 4, 8, 5, 3] [7, 3, 8, 2, 5, 1, 6, 4] [3, 8, 4, 7, 1, 6, 2, 5] [3, 6, 8, 2, 4, 1, 7, 5] [3, 5, 7, 1, 4, 2, 8, 6] [6, 2, 7, 1, 3, 5, 8, 4] [5, 2, 8, 1, 4, 7, 3, 6] [6, 3, 7, 2, 4, 8, 1, 5] [6, 3, 7, 2, 8, 5, 1, 4] [7, 2, 4, 1, 8, 5, 3, 6] [8, 2, 4, 1, 7, 5, 3, 6] [2, 5, 7, 4, 1, 8, 6, 3] [2, 7, 3, 6, 8, 5, 1, 4] [1, 7, 4, 6, 8, 2, 5, 3] [3, 6, 2, 5, 8, 1, 7, 4] [5, 7, 2, 6, 3, 1, 8, 4] [5, 7, 2, 4, 8, 1, 3, 6] [4, 8, 1, 5, 7, 2, 6, 3] [3, 7, 2, 8, 5, 1, 4, 6] [6, 3, 1, 8, 5, 2, 4, 7] [5, 3, 1, 6, 8, 2, 4, 7] [7, 4, 2, 8, 6, 1, 3, 5] [6, 3, 1, 7, 5, 8, 2, 4] [2, 6, 1, 7, 4, 8, 3, 5] [4, 2, 8, 6, 1, 3, 5, 7] [8, 2, 5, 3, 1, 7, 4, 6] [5, 8, 4, 1, 3, 6, 2, 7] [7, 5, 3, 1, 6, 8, 2, 4] [3, 5, 2, 8, 1, 7, 4, 6] [6, 4, 2, 8, 5, 7, 1, 3] [7, 4, 2, 5, 8, 1, 3, 6] [7, 3, 1, 6, 8, 5, 2, 4] [4, 6, 8, 2, 7, 1, 3, 5] [4, 2, 8, 5, 7, 1, 3, 6] [3, 1, 7, 5, 8, 2, 4, 6] [1, 6, 8, 3, 7, 4, 2, 5] [4, 2, 7, 3, 6, 8, 1, 5] [3, 6, 8, 1, 5, 7, 2, 4] [5, 1, 8, 6, 3, 7, 2, 4] [1, 5, 8, 6, 3, 7, 2, 4] [4, 7, 5, 2, 6, 1, 3, 8] [4, 2, 7, 3, 6, 8, 5, 1] [2, 5, 7, 1, 3, 8, 6, 4] [5, 7, 4, 1, 3, 8, 6, 2] [2, 8, 6, 1, 3, 5, 7, 4] [6, 4, 7, 1, 8, 2, 5, 3] [6, 1, 5, 2, 8, 3, 7, 4] [3, 6, 4, 2, 8, 5, 7, 1] [3, 6, 4, 1, 8, 5, 7, 2] [5, 8, 4, 1, 7, 2, 6, 3] [2, 6, 8, 3, 1, 4, 7, 5] [7, 2, 6, 3, 1, 4, 8, 5] [5, 3, 8, 4, 7, 1, 6, 2] [4, 7, 5, 3, 1, 6, 8, 2] [4, 2, 7, 5, 1, 8, 6, 3] [5, 3, 1, 7, 2, 8, 6, 4] [2, 4, 6, 8, 3, 1, 7, 5] [6, 3, 1, 8, 4, 2, 7, 5] [1, 7, 5, 8, 2, 4, 6, 3] [8, 3, 1, 6, 2, 5, 7, 4] [3, 6, 2, 7, 1, 4, 8, 5] [2, 7, 5, 8, 1, 4, 6, 3] [5, 7, 1, 4, 2, 8, 6, 3] [3, 6, 2, 7, 5, 1, 8, 4] [6, 4, 1, 5, 8, 2, 7, 3] [3, 7, 2, 8, 6, 4, 1, 5] [5, 7, 1, 3, 8, 6, 4, 2] [6, 8, 2, 4, 1, 7, 5, 3] [5, 2, 4, 7, 3, 8, 6, 1] [5, 1, 4, 6, 8, 2, 7, 3] [7, 1, 3, 8, 6, 4, 2, 5] [4, 7, 3, 8, 2, 5, 1, 6] [4, 2, 5, 8, 6, 1, 3, 7] Total solutions: 92 ``` Subexpression: using Satisfiability function queens(n::Int) open(Z3()) do solver # Define SAT variables for the column positions of each queen @sat