3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-06-08 09:26:15 -07:00
parent 08528b3526
commit 2861b10d58

View file

@ -1074,7 +1074,7 @@
"source": [
"# Puzzles\n",
"\n",
"Dog, Cat and Mouse\n",
"## Dog, Cat and Mouse\n",
"\n",
"Consider the following puzzle. Spend exactly 100 dollars and buy exactly 100 animals. Dogs cost 15 dollars, cats cost 1 dollar, and mice cost 25 cents each. You have to buy at least one of each. How many of each should you buy?\n"
]
@ -1108,7 +1108,7 @@
"cell_type": "markdown",
"metadata": {},
"source": [
"# Sodoku\n",
"## Sodoku\n",
"\n",
"<p><a target=\"_blank\" href=\"http://www.dailysudoku.com/sudoku/\">Sudoku</a>is a very popular puzzle. The goal is to insert the numbers in the boxes to satisfy only one condition: each row, column and 3x3 box must contain the digits 1 through 9 exactly once.\n",
" \n",
@ -1213,7 +1213,7 @@
"cell_type": "markdown",
"metadata": {},
"source": [
"# Eight queens\n",
"## Eight queens\n",
"\n",
"\n",
"The eight queens puzzle is the problem of placing eight chess queens on an 8x8 chessboard so that no two queens attack each other. Thus, a solution requires that no two queens share the same row, column, or diagonal.\n",