Skip to content

Commit

Permalink
Merge pull request #78 from Fe-r-oz/fa/doc-fix
Browse files Browse the repository at this point in the history
fix: correctly use `# output` in script examples
  • Loading branch information
elsoroka authored Dec 28, 2024
2 parents 2333f6f + 6d013f8 commit a1dd52b
Show file tree
Hide file tree
Showing 2 changed files with 16 additions and 1 deletion.
6 changes: 5 additions & 1 deletion docs/src/example_nqueens.md
Original file line number Diff line number Diff line change
Expand Up @@ -77,14 +77,18 @@ function queens(n::Int)
end
end
queens(4)
# output
queens(4)
[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]
Expand Down
11 changes: 11 additions & 0 deletions docs/src/example_sudoku_solver.md
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,8 @@ represent the digits in the grid.
using Satisfiability
# Create a 9x9 matrix of integer variables (for the Sudoku grid)
@satvariable(X[1:9, 1:9], Int);
# output
```

The main constraints for Sudoku are:
Expand All @@ -40,6 +42,8 @@ sq_c = [distinct([X[3*i0 + i, 3*j0 + j] for i in 1:3, j in 1:3]) for i0 in 0:2,
# Combine all constraints into one list
sudoku_c = vcat(cells_c..., rows_c..., cols_c..., sq_c...);
# output
```

For a given Sudoku puzzle, some cells are pre-filled with known values, and others are
Expand All @@ -59,6 +63,8 @@ instance = [
(0, 0, 0, 4, 1, 9, 0, 0, 5),
(0, 0, 0, 0, 8, 0, 0, 7, 9)
];
# output
```

!!! note We have chosen the identical pre-filled values as presented in the
Expand All @@ -71,13 +77,17 @@ Define constraints for the given values (cells with non-zero values) as follows:
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
```

Now, we combine all the constraints (cell, row, column, subgrid, and given values):

```jldoctest label4; output = false

Check failure on line 86 in docs/src/example_sudoku_solver.md

View workflow job for this annotation

GitHub Actions / Documentation

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
# Combine the sudoku constraints and the puzzle instance constraints
constraints = vcat(sudoku_c..., instance_c...);
# output
```

Now that we have set up all the constraints, we can use Z3 to solve the puzzle. The solver
Expand Down Expand Up @@ -117,6 +127,7 @@ open(Z3()) do solver
end
# output
Status: SAT
5 3 4 | 6 7 8 | 9 1 2
6 7 2 | 1 9 5 | 3 4 8
Expand Down

0 comments on commit a1dd52b

Please sign in to comment.