CP sat and solution search dead end

Just wondering what CP SAT does when it selects a branch which does not lead to global optimum? For instance, a code minimizing an objective returns:

Solution 0, time = 1.05 s, objective = 11700
Solution 1, time = 1.59 s, objective = 9200
Solution 2, time = 4.54 s, objective = 9100
Solution 3, time = 5.14 s, objective = 8600
Solution 4, time = 6.44 s, objective = 7600
Solution 5, time = 8.04 s, objective = 7100
Solution 6, time = 8.72 s, objective = 6000
Solution 7, time = 10.44 s, objective = 5900
Solution 8, time = 15.67 s, objective = 1600
Solution 9, time = 16.29 s, objective = 200

I understand it ignores solutions with greater objective value in minimizing context.

Below is the setup.

solver = cp_model.CpSolver()
solver.parameters.max_time_in_seconds = 100
solver.parameters.num_search_workers = 16

Since the code finished in 40 seconds, can one assume it enumerated all solutions? I was unable to use enumerate_all_solutions parameter in combination with num_search_workers.

Answer

Like all solvers, it prunes branches as soon as possible. Note that search in a SAT solver is not a tree search.

After 40s, it proved that the solution is optimal. Luckily, it does not need to enumerate all solutions to do so.

Note: linearization_level = 0 is bizarre. Does it change anything ?

Advertisement

Answer