doctest failure in src/example_sudoku_solver.md:84-182 ```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 9×9 Matrix{BoolExpr}: eq_dcf604d979b7fa47 | X_1_1 | const_5 = 5 eq_308eaa2cff143be9 | X_1_2 | const_3 = 3 … eq_2d017e8e50553990 | X_1_9 | X_1_9 eq_bbe7cfe32f2c86ce | X_2_1 | const_6 = 6 eq_9ce5ecacfb3d4995 | X_2_2 | X_2_2 eq_ebc64589fcc890cc | X_2_9 | X_2_9 eq_db84c42bcfacc50e | X_3_1 | X_3_1 eq_58318b31d4f50cfb | X_3_2 | const_9 = 9 eq_95f73805835f69cb | X_3_9 | X_3_9 eq_d941bd305d656f1f | X_4_1 | const_8 = 8 eq_9b6cfb74f3852d3e | X_4_2 | X_4_2 eq_290cc45b1804d9df | X_4_9 | const_3 = 3 eq_a9de797a69e79898 | X_5_1 | const_4 = 4 eq_39cc02fe88292601 | X_5_2 | X_5_2 eq_8ae5b89d9de60fb9 | X_5_9 | const_1 = 1 eq_36cfe09d42965739 | X_6_1 | const_7 = 7 eq_e4cfdba84463e114 | X_6_2 | X_6_2 … eq_1187474addf2ab2e | X_6_9 | const_6 = 6 eq_4fbdfd428c370ae | X_7_1 | X_7_1 eq_b8bf46366043ab6d | X_7_2 | const_6 = 6 eq_147e360d5715143b | X_7_9 | X_7_9 eq_7e608dc16ec3aa85 | X_8_1 | X_8_1 eq_c37b9f4b2b896e52 | X_8_2 | X_8_2 eq_40e977cc36265ac6 | X_8_9 | const_5 = 5 eq_350c35e834afcd83 | X_9_1 | X_9_1 eq_39f8fa1801dc42df | X_9_2 | X_9_2 eq_29b7b29789ac23ed | X_9_9 | const_9 = 9 ``` 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: 9×9 Matrix{BoolExpr}: eq_dcf604d979b7fa47 | X_1_1 | const_5 = 5 eq_308eaa2cff143be9 | X_1_2 | const_3 = 3 … eq_2d017e8e50553990 | X_1_9 | X_1_9 eq_bbe7cfe32f2c86ce | X_2_1 | const_6 = 6 eq_9ce5ecacfb3d4995 | X_2_2 | X_2_2 eq_ebc64589fcc890cc | X_2_9 | X_2_9 eq_db84c42bcfacc50e | X_3_1 | X_3_1 eq_58318b31d4f50cfb | X_3_2 | const_9 = 9 eq_95f73805835f69cb | X_3_9 | X_3_9 eq_d941bd305d656f1f | X_4_1 | const_8 = 8 eq_9b6cfb74f3852d3e | X_4_2 | X_4_2 eq_290cc45b1804d9df | X_4_9 | const_3 = 3 eq_a9de797a69e79898 | X_5_1 | const_4 = 4 eq_39cc02fe88292601 | X_5_2 | X_5_2 eq_8ae5b89d9de60fb9 | X_5_9 | const_1 = 1 eq_36cfe09d42965739 | X_6_1 | const_7 = 7 eq_e4cfdba84463e114 | X_6_2 | X_6_2 … eq_1187474addf2ab2e | X_6_9 | const_6 = 6 eq_4fbdfd428c370ae | X_7_1 | X_7_1 eq_b8bf46366043ab6d | X_7_2 | const_6 = 6 eq_147e360d5715143b | X_7_9 | X_7_9 eq_7e608dc16ec3aa85 | X_8_1 | X_8_1 eq_c37b9f4b2b896e52 | X_8_2 | X_8_2 eq_40e977cc36265ac6 | X_8_9 | const_5 = 5 eq_350c35e834afcd83 | X_9_1 | X_9_1 eq_39f8fa1801dc42df | X_9_2 | X_9_2 eq_29b7b29789ac23ed | X_9_9 | const_9 = 9 diff = Warning: Diff output requires color. 9×9 Matrix{BoolExpr}: eq_dcf604d979b7fa47 | X_1_1 | const_5 = 5 eq_308eaa2cff143be9

doctest failure in src/example_sudoku_solver.md:186-417 ```jldoctest label4; output = false # Combine the sudoku constraints and the puzzle instance constraints constraints = vcat(sudoku_c..., instance_c...); # 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 and_5b10f81379a5789f | leq_1db81797fbf16ca5 | | X_2_2 | | const_9 = 9 | leq_5c7fc875b1d46fe3 | | const_1 = 1 | | X_2_2 and_cb393ffe746cf345 | leq_58318b31d4f50cfb | | X_3_2 | | const_9 = 9 | leq_620d2c7d86f06f95 | | const_1 = 1 | | X_3_2 and_dd7b3bf37f25acbe | leq_25f4212a99015bbe | | X_4_2 | | const_9 = 9 | leq_f0bd5fbae9ec0d70 | | const_1 = 1 | | X_4_2 and_d035128e1f0f3bdd | leq_2ad9ea94c8cbd695 | | X_5_2 | | const_9 = 9 | leq_accb06f57e2ba0d7 | | const_1 = 1 | | X_5_2 and_f40d10db42ad3f6e | leq_8d5c6994f89b20c8 | | X_6_2 | | const_9 = 9 | leq_a72d623d359fb293 | | const_1 = 1 | | X_6_2 and_cce3b8e80f7941d3 | leq_762f8c5e45b68735 | | const_1 = 1 | | X_7_2 | leq_facefc358841f567 | | X_7_2 | | const_9 = 9 and_6ea6ad8a62ea52c9 | leq_2d79e65d2e87bf8e | | X_8_2 | | const_9 = 9 | leq_3aa43210f504d10 | | const_1 = 1 | | X_8_2 and_ca24cbd3e601ab98 | leq_49caf6b17fdb2237 | | X_9_2 | | const_9 = 9 | leq_e77e5d38f9939a25 | | const_1 = 1 | | X_9_2 and_fc4519dd76487a52 | leq_4fdb0d673d4b8877 | | X_1_3 | | const_9 = 9 | leq_b4749515cda17f3e | | const_1 = 1 | | X_1_3 ⋮ eq_52962a4723ffe178 | X_1_8 | X_1_8 eq_7631ad5a4db0ba8a | X_2_8 | X_2_8 eq_e3e3099959242eee | X_3_8 | const_6 = 6 eq_3f8b46db4ca8e04a | X_4_8 | X_4_8 eq_1d2bc36a587f8cce | X_5_8 | X_5_8 eq_5e486f2e84bdacdb | X_6_8 | X_6_8 eq_cefeb88a10768a1f | X_7_8 | const_8 = 8 eq_d1be9198106bf284 | X_8_8 | X_8_8 eq_f84a5762fb991b6c | X_9_8 | const_7 = 7 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 ``` 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_6526

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