CP-SAT freezing soon after starting to solve with 8 or more workers

Question

I am experiencing this for all formulations now. Previously I had no issues.

Take this example:

from ortools.sat.python import cp_model
from typing import List, Optional
from ortools.sat.python import cp_model

n = 8  # Board size and number of queens
model = cp_model.CpModel()

# Create variables - queens[i] represents the column position of queen in row i
queens = [model.NewIntVar(0, n - 1, f"queen_{i}") for i in range(n)]

# No two queens in same column
model.AddAllDifferent(queens)

# No two queens in same diagonal
for i in range(n):
    for j in range(i + 1, n):
        model.Add(queens[i] - queens[j] != i - j)
        model.Add(queens[i] - queens[j] != j - i)

# Solve
solver = cp_model.CpSolver()
solver.parameters.max_time_in_seconds = 10
solver.parameters.log_search_progress = True
solver.parameters.num_search_workers = 8
status = solver.Solve(model)

This code freezes indefinitely just after starting to solve. Output:

Starting CP-SAT solver v9.11.4210
Parameters: max_time_in_seconds: 10 log_search_progress: true num_search_workers: 8

Initial satisfaction model '': (model_fingerprint: 0x6856406a4ac1332d)
#Variables: 8
  - 8 in [0,7]
#kAllDiff: 1
#kLinear2: 56 (#complex_domain: 56)

Starting presolve at 0.00s
  1.10e-05s  0.00e+00d  [DetectDominanceRelations] 
  1.49e-04s  0.00e+00d  [PresolveToFixPoint] #num_loops=2 #num_dual_strengthening=1 
  2.00e-06s  0.00e+00d  [ExtractEncodingFromLinear] 
[Symmetry] Graph for symmetry has 552 nodes and 944 arcs.
[Symmetry] Symmetry computation done. time: 0.000165 dtime: 0.00029732
[Symmetry] #generators: 1, average support size: 72
[Symmetry] 36 orbits with sizes: 2,2,2,2,2,2,2,2,2,2,...
[Symmetry] Num fixable by intersecting at_most_one with orbits: 4 largest_orbit: 2
[SAT presolve] num removable Booleans: 0 / 64
[SAT presolve] num trivial clauses: 0
[SAT presolve] [0s] clauses:252 literals:504 vars:60 one_side_vars:60 simple_definition:0 singleton_clauses:0
[SAT presolve] [1.3e-05s] clauses:252 literals:504 vars:60 one_side_vars:60 simple_definition:0 singleton_clauses:0
[SAT presolve] [2e-05s] clauses:252 literals:504 vars:60 one_side_vars:60 simple_definition:0 singleton_clauses:0
...
#2       0.00s default_lp (fixed_bools=0/60)
#3       0.00s quick_restart (fixed_bools=0/60)
#4       0.00s quick_restart_no_lp (fixed_bools=0/60)
#Model   0.11s var:59/60 constraints:114/114

If I update the num search workers to any number below 8 then there are no issues.

Has anyone seen this before?

CP-SAT freezing soon after starting to solve with 8 or more workers

Answers (1)

Related Questions