{
"cells": [
{
"cell_type": "markdown",
"id": "8115ad2d",
"metadata": {},
"source": [
"# Finding One, Several or All Solutions"
]
},
{
"cell_type": "markdown",
"id": "42c71fc1",
"metadata": {},
"source": [
"The easiest and most efficient way of getting several (and even, all) solutions of a CSP instance is to ask the underlying solver to provide them. We give an illustration with the Prime Looking Problem."
]
},
{
"cell_type": "markdown",
"id": "9f54634a",
"metadata": {},
"source": [
"But first, we need first to import the library PyCSP$^3$:"
]
},
{
"cell_type": "code",
"execution_count": 1,
"id": "66e3c136",
"metadata": {},
"outputs": [],
"source": [
"from pycsp3 import *"
]
},
{
"cell_type": "markdown",
"id": "390662e3",
"metadata": {},
"source": [
"The prime-looking problem is from Martin Gardner: a number is said to be *prime-looking* if it is composite but not divisible by 2, 3 or 5. We know that the three smallest prime-looking numbers are 49, 77 and 91. Can you find the prime-looking numbers less than 1000?"
]
},
{
"cell_type": "markdown",
"id": "2bc6bbcf",
"metadata": {},
"source": [
"The model is rather simple:"
]
},
{
"cell_type": "code",
"execution_count": 2,
"id": "a94e2ebd",
"metadata": {},
"outputs": [],
"source": [
"# the number we look for\n",
"x = Var(range(1000))\n",
"\n",
"# a first divider\n",
"d1 = Var(range(2, 1000))\n",
"\n",
"# a second divider\n",
"d2 = Var(range(2, 1000))\n",
"\n",
"satisfy(\n",
" x == d1 * d2,\n",
" x % 2 != 0,\n",
" x % 3 != 0,\n",
" x % 5 != 0,\n",
" d1 <= d2\n",
");"
]
},
{
"cell_type": "markdown",
"id": "bf39c316",
"metadata": {},
"source": [
"The solving part of the code is for example: "
]
},
{
"cell_type": "code",
"execution_count": 3,
"id": "ecd86c3c",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Result: SAT\n",
"The prime-looking number is: 49\n"
]
}
],
"source": [
"instance = compile()\n",
"ace = solver(ACE)\n",
"result = ace.solve(instance)\n",
"\n",
"print(\"Result:\", result)\n",
"if result is SAT:\n",
" print(\"The prime-looking number is: \", value(x))"
]
},
{
"cell_type": "markdown",
"id": "60c8ed17",
"metadata": {},
"source": [
"For the moment, we only get and display the first found solution. Note how we can decide to compile, choose the solver and run the solver in separate statements."
]
},
{
"cell_type": "markdown",
"id": "038e3e7b",
"metadata": {},
"source": [
"Of course, most of the time, we certainly prefer to use a simplified equivalent code:"
]
},
{
"cell_type": "code",
"execution_count": 4,
"id": "2d2d595d",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"The prime-looking number is: 49\n"
]
}
],
"source": [
"if solve() is SAT:\n",
" print(\"The prime-looking number is: \", value(x))"
]
},
{
"cell_type": "markdown",
"id": "ba757e37",
"metadata": {},
"source": [
"Note that we can also call *solution()* and get specialized information (field) as shown now: "
]
},
{
"cell_type": "code",
"execution_count": 5,
"id": "4670dfe7",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Solution: \n",
" x d1 d2
\n",
" 49 7 7 \n",
"\n",
"Solution Root: \n",
"Solution Variables: [x, d1, d2]\n",
"Solution Values: [49, 7, 7]\n",
"Pretty Solution: \n",
" x d1 d2
\n",
" 49 7 7 \n",
"\n"
]
}
],
"source": [
"if solve() is SAT:\n",
" solution = solution()\n",
" print(\"Solution: \", solution)\n",
" print(\"Solution Root: \", solution.root)\n",
" print(\"Solution Variables: \", solution.variables)\n",
" print(\"Solution Values: \", solution.values)\n",
" print(\"Pretty Solution: \", solution.pretty_solution)"
]
},
{
"cell_type": "markdown",
"id": "07a3beab",
"metadata": {},
"source": [
"Now, if we want to get and display all solutions, we need to set ALL as value of the named parameter *sols* of the function *solve()*. After solving, we can get the number of found solutions by calling *n_solutions()*, and, interestingly, we can use the name parameter *sol* to indicate the index of a solution when calling the functions *values()* and *value()*."
]
},
{
"cell_type": "code",
"execution_count": 6,
"id": "5ab3d69a",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Number of solutions: 105\n",
"Solutions: [49, 77, 91, 119, 121, 133, 143, 161, 169, 187, 203, 209, 217, 221, 247, 253, 259, 287, 289, 299, 301, 319, 323, 329, 341, 343, 361, 371, 377, 391, 403, 407, 413, 427, 437, 451, 469, 473, 481, 493, 497, 511, 517, 527, 529, 533, 539, 539, 551, 553, 559, 581, 583, 589, 611, 623, 629, 637, 637, 649, 667, 671, 679, 689, 697, 703, 707, 713, 721, 731, 737, 749, 763, 767, 779, 781, 791, 793, 799, 803, 817, 833, 833, 841, 847, 847, 851, 869, 871, 889, 893, 899, 901, 913, 917, 923, 931, 931, 943, 949, 959, 961, 973, 979, 989]\n"
]
}
],
"source": [
"if solve(sols=ALL) is SAT:\n",
" print(\"Number of solutions: \", n_solutions())\n",
" print(\"Solutions: \", sorted([value(x, sol=i) for i in range(n_solutions())]))"
]
},
{
"cell_type": "markdown",
"id": "779dfadd",
"metadata": {},
"source": [
"Actually, it is known that there are 100 prime-looking numbers less than 1000. To check this, we can use a Python set to remove identical solutions: "
]
},
{
"cell_type": "code",
"execution_count": 7,
"id": "1ac5bcc8",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Number of prime looking numbers: 100\n"
]
}
],
"source": [
"if solve(sols=ALL) is SAT:\n",
" t = sorted(set([value(x, sol=i) for i in range(n_solutions())]))\n",
" print(\"Number of prime looking numbers: \", len(t))"
]
},
{
"cell_type": "markdown",
"id": "410b942c",
"metadata": {},
"source": [
"We can also choose to only find the first $k$ solutions. We need $k$ to be a positive integer set as value of the named parameter *sols* of the function *solve()*. For example, for $k=10$, we have:"
]
},
{
"cell_type": "code",
"execution_count": 8,
"id": "9578cffa",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Number of solutions: 10\n",
"Solutions: [49, 77, 91, 119, 133, 161, 203, 217, 259, 287]\n"
]
}
],
"source": [
"if solve(sols=10) is SAT:\n",
" print(\"Number of solutions: \", n_solutions())\n",
" print(\"Solutions: \", [value(x, sol=i) for i in range(n_solutions())])"
]
}
],
"metadata": {
"kernelspec": {
"display_name": "Python 3 (ipykernel)",
"language": "python",
"name": "python3"
},
"language_info": {
"codemirror_mode": {
"name": "ipython",
"version": 3
},
"file_extension": ".py",
"mimetype": "text/x-python",
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.7.12"
}
},
"nbformat": 4,
"nbformat_minor": 5
}