Link Search Menu Expand Document
PyCSP3
Documentation Data GitHub XCSP3 About
download ipynb

Finding One, Several or All Solutions

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.

But first, we need first to import the library PyCSP$^3$:

from pycsp3 import *

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?

The model is rather simple:

# the number we look for
x = Var(range(1000))

# a first divider
d1 = Var(range(2, 1000))

# a second divider
d2 = Var(range(2, 1000))

satisfy(
    x == d1 * d2,
    x % 2 != 0,
    x % 3 != 0,
    x % 5 != 0,
    d1 <= d2
);

The solving part of the code is for example:

instance = compile()
ace = solver(ACE)
result = ace.solve(instance)

print("Result:", result)
if result is SAT:
    print("The prime-looking number is: ", value(x))
Result: SAT
The prime-looking number is:  49

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.

Of course, most of the time, we certainly prefer to use a simplified equivalent code:

if solve() is SAT:
    print("The prime-looking number is: ", value(x))
The prime-looking number is:  49

Note that we can also call solution() and get specialized information (field) as shown now:

if solve() is SAT:
    solution = solution()
    print("Solution: ", solution)
    print("Solution Root: ", solution.root)
    print("Solution Variables: ", solution.variables)
    print("Solution Values: ", solution.values)
    print("Pretty Solution: ", solution.pretty_solution)
Solution:  <instantiation id="sol1" type="solution">
  <list> x d1 d2 </list>
  <values> 49 7 7 </values>
</instantiation>
Solution Root:  <Element instantiation at 0x7f27502bcc80>
Solution Variables:  [x, d1, d2]
Solution Values:  [49, 7, 7]
Pretty Solution:  <instantiation id="sol1" type="solution">
  <list> x d1 d2 </list>
  <values> 49 7 7 </values>
</instantiation>

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().

if solve(sols=ALL) is SAT:
    print("Number of solutions: ", n_solutions())
    print("Solutions: ", sorted([value(x, sol=i) for i in range(n_solutions())]))
Number of solutions:  105
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]

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:

if solve(sols=ALL) is SAT:
    t = sorted(set([value(x, sol=i) for i in range(n_solutions())]))
    print("Number of prime looking numbers: ", len(t))
Number of prime looking numbers:  100

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:

if solve(sols=10) is SAT:
    print("Number of solutions: ", n_solutions())
    print("Solutions: ", [value(x, sol=i) for i in range(n_solutions())])
Number of solutions:  10
Solutions:  [49, 77, 91, 119, 133, 161, 203, 217, 259, 287]