Segfault when solving a CP model with 9.15 utilizing many cores #5025
Description
Version: 9.15.6755
Language: Python
The model is part of a larger scheduling suite we are developing for a major german railway company. The model uses the CP-SAT solver and is built with python. We employ the tool for several years now and this error did not occur with previous versions.
What did you do?
Solve my model as usual with 30 cores.
What did you expect to see
Model solves or proves infeasibility
What did you see instead?
segfault
I'm solving a model with CP-SAT solver.
Running in a docker image (python:3.13) on a AWS EC2 machine r6a.8xlarge (32 CPUs, 256GB RAM) with AWSLinux 2023.
After testing a bit I tried to use less cores and with 8 cores there is no problem.
Here is the log with 30 cores:
Starting CP-SAT solver v9.15.6755
Parameters: random_seed: 1337 max_time_in_seconds: 300 max_memory_in_mb: 2048 log_search_progress: true num_search_workers: 30 repair_hint: true
Setting number of shared tree workers to 7
Initial optimization model '': (model_fingerprint: 0xe3be1f6b16b381b8)
#Variables: 1'928 (#bools: 701 in objective) (964 primary variables)
- 1'928 Booleans in [0,1]
#kLinear1: 4
#kLinear2: 1'560
Starting presolve at 0.02s
The solution hint is incomplete: 482 out of 1928 non fixed variables hinted.
3.08e-04s 0.00e+00d [DetectDominanceRelations]
7.81e-03s 0.00e+00d [PresolveToFixPoint] #num_loops=1 #num_dual_strengthening=1
9.57e-06s 0.00e+00d [ExtractEncodingFromLinear]
7.65e-06s 0.00e+00d [DetectDuplicateColumns]
8.17e-06s 0.00e+00d [DetectDuplicateConstraints]
[Symmetry] Graph for symmetry has 1'928 nodes and 0 arcs.
[Symmetry] Symmetry computation done. time: 0.000125457 dtime: 0.00011568
6.83e-06s 0.00e+00d [DetectDuplicateConstraintsWithDifferentEnforcements]
7.57e-03s 2.69e-04d [Probe] #probed=2'876
5.71e-06s 0.00e+00d [MaxClique]
9.46e-06s 0.00e+00d [PresolveToFixPoint]
5.64e-06s 0.00e+00d [ProcessAtMostOneAndLinear]
6.22e-06s 0.00e+00d [DetectDuplicateConstraints]
2.99e-06s 0.00e+00d [DetectDuplicateConstraintsWithDifferentEnforcements]
4.10e-06s 0.00e+00d [DetectDominatedLinearConstraints]
4.14e-06s 0.00e+00d [DetectDifferentVariables]
5.50e-06s 0.00e+00d [ProcessSetPPC]
2.20e-04s 0.00e+00d [TransformClausesToExactlyOne]
3.86e-06s 0.00e+00d [DetectEncodedComplexDomains]
7.42e-06s 0.00e+00d [FindAlmostIdenticalLinearConstraints]
4.89e-06s 0.00e+00d [FindBigAtMostOneAndLinearOverlap]
7.80e-06s 4.00e-08d [FindBigVerticalLinearOverlap]
4.83e-06s 0.00e+00d [FindBigHorizontalLinearOverlap]
5.39e-06s 0.00e+00d [MergeClauses]
8.15e-06s 0.00e+00d [PresolveToFixPoint]
7.60e-06s 0.00e+00d [PresolveToFixPoint]
4.49e-06s 0.00e+00d [DetectDuplicateColumns]
3.55e-06s 0.00e+00d [DetectDuplicateConstraints]
[Symmetry] Graph for symmetry has 1'928 nodes and 0 arcs.
[Symmetry] Symmetry computation done. time: 9.1655e-05 dtime: 0.00011568
5.62e-06s 0.00e+00d [DetectDuplicateConstraintsWithDifferentEnforcements]
3.60e-03s 2.69e-04d [Probe] #probed=2'876
3.75e-06s 0.00e+00d [MaxClique]
9.15e-06s 0.00e+00d [PresolveToFixPoint]
4.83e-06s 0.00e+00d [ProcessAtMostOneAndLinear]
4.68e-06s 0.00e+00d [DetectDuplicateConstraints]
2.68e-06s 0.00e+00d [DetectDuplicateConstraintsWithDifferentEnforcements]
3.69e-06s 0.00e+00d [DetectDominatedLinearConstraints]
4.00e-06s 0.00e+00d [DetectDifferentVariables]
5.01e-06s 0.00e+00d [ProcessSetPPC]
2.18e-04s 0.00e+00d [TransformClausesToExactlyOne]
4.05e-06s 0.00e+00d [DetectEncodedComplexDomains]
7.14e-06s 0.00e+00d [FindAlmostIdenticalLinearConstraints]
4.76e-06s 0.00e+00d [FindBigAtMostOneAndLinearOverlap]
7.67e-06s 4.00e-08d [FindBigVerticalLinearOverlap]
4.50e-06s 0.00e+00d [FindBigHorizontalLinearOverlap]
4.77e-06s 0.00e+00d [MergeClauses]
7.54e-06s 0.00e+00d [PresolveToFixPoint]
1.49e-05s 0.00e+00d [MergeNoOverlap]
3.49e-06s 0.00e+00d [MergeNoOverlap2D]
4.15e-05s 0.00e+00d [ExpandObjective]
Presolve summary:
- 960 affine relations were detected.
- rule 'affine: new relation' was applied 960 times.
- rule 'linear1: x in domain' was applied 4 times.
- rule 'linear: always true' was applied 1 time.
- rule 'linear: empty' was applied 599 times.
- rule 'linear: fixed or dup variables' was applied 604 times.
- rule 'linear: reduced variable domains' was applied 4 times.
- rule 'linear: remapped using affine relations' was applied 960 times.
- rule 'objective: variable not used elsewhere' was applied 478 times.
- rule 'presolve: 972 unused variables removed.' was applied 1 time.
- rule 'presolve: iteration' was applied 2 times.
Presolved optimization model '': (model_fingerprint: 0x8fa9deebc7ce54b4)
#Variables: 0 ( in objective) (0 primary variables)
[Symmetry] Graph for symmetry has 0 nodes and 0 arcs.
Preloading model.
#Bound 0.07s best:inf next:[4059914,4059914] initial_domain
The solution hint is complete and is feasible. Its objective value is 4059914.
#Model 0.07s var:0/0 constraints:0/0
Starting search at 0.07s with 30 workers.
22 full problem subsolvers: [default_lp(11), max_lp, no_lp, quick_restart, quick_restart_no_lp, shared_tree(7)]
8 first solution subsolvers: [fj(3), fj_lin, fs_random, fs_random_no_lp, fs_random_quick_restart, fs_random_quick_restart_no_lp]
6 interleaved subsolvers: [feasibility_pump, ls(2), ls_lin, rins/rens, variables_shaving]
2 helper subsolvers: [neighborhood_helper, synchronization_agent]
#1 0.08s best:4059914 next:[] shared_tree [repaired]
Check failed: heuristics.fixed_search != nullptr
*** Check failure stack trace: ***
log for run with 8 cores:
Starting CP-SAT solver v9.15.6755
Parameters: random_seed: 1337 max_time_in_seconds: 300 max_memory_in_mb: 2048 log_search_progress: true num_search_workers: 8 repair_hint: true
Initial optimization model '': (model_fingerprint: 0xe3be1f6b16b381b8)
#Variables: 1'928 (#bools: 701 in objective) (964 primary variables)
- 1'928 Booleans in [0,1]
#kLinear1: 4
#kLinear2: 1'560
Starting presolve at 0.02s
The solution hint is incomplete: 482 out of 1928 non fixed variables hinted.
1.82e-04s 0.00e+00d [DetectDominanceRelations]
5.96e-03s 0.00e+00d [PresolveToFixPoint] #num_loops=1 #num_dual_strengthening=1
7.24e-06s 0.00e+00d [ExtractEncodingFromLinear]
5.88e-06s 0.00e+00d [DetectDuplicateColumns]
6.81e-06s 0.00e+00d [DetectDuplicateConstraints]
[Symmetry] Graph for symmetry has 1'928 nodes and 0 arcs.
[Symmetry] Symmetry computation done. time: 8.1362e-05 dtime: 0.00011568
6.75e-06s 0.00e+00d [DetectDuplicateConstraintsWithDifferentEnforcements]
5.91e-03s 2.69e-04d [Probe] #probed=2'876
4.96e-06s 0.00e+00d [MaxClique]
1.13e-05s 0.00e+00d [PresolveToFixPoint]
5.80e-06s 0.00e+00d [ProcessAtMostOneAndLinear]
6.22e-06s 0.00e+00d [DetectDuplicateConstraints]
2.39e-06s 0.00e+00d [DetectDuplicateConstraintsWithDifferentEnforcements]
3.07e-06s 0.00e+00d [DetectDominatedLinearConstraints]
3.36e-06s 0.00e+00d [DetectDifferentVariables]
4.25e-06s 0.00e+00d [ProcessSetPPC]
1.51e-04s 0.00e+00d [TransformClausesToExactlyOne]
4.83e-06s 0.00e+00d [DetectEncodedComplexDomains]
5.65e-06s 0.00e+00d [FindAlmostIdenticalLinearConstraints]
3.57e-06s 0.00e+00d [FindBigAtMostOneAndLinearOverlap]
9.08e-06s 4.00e-08d [FindBigVerticalLinearOverlap]
3.69e-06s 0.00e+00d [FindBigHorizontalLinearOverlap]
4.35e-06s 0.00e+00d [MergeClauses]
6.59e-06s 0.00e+00d [PresolveToFixPoint]
7.07e-06s 0.00e+00d [PresolveToFixPoint]
3.66e-06s 0.00e+00d [DetectDuplicateColumns]
3.03e-06s 0.00e+00d [DetectDuplicateConstraints]
[Symmetry] Graph for symmetry has 1'928 nodes and 0 arcs.
[Symmetry] Symmetry computation done. time: 6.7391e-05 dtime: 0.00011568
5.07e-06s 0.00e+00d [DetectDuplicateConstraintsWithDifferentEnforcements]
1.95e-03s 2.69e-04d [Probe] #probed=2'876
2.70e-06s 0.00e+00d [MaxClique]
6.74e-06s 0.00e+00d [PresolveToFixPoint]
4.82e-06s 0.00e+00d [ProcessAtMostOneAndLinear]
3.92e-06s 0.00e+00d [DetectDuplicateConstraints]
1.80e-06s 0.00e+00d [DetectDuplicateConstraintsWithDifferentEnforcements]
2.23e-06s 0.00e+00d [DetectDominatedLinearConstraints]
2.54e-06s 0.00e+00d [DetectDifferentVariables]
3.49e-06s 0.00e+00d [ProcessSetPPC]
1.19e-04s 0.00e+00d [TransformClausesToExactlyOne]
3.30e-06s 0.00e+00d [DetectEncodedComplexDomains]
4.83e-06s 0.00e+00d [FindAlmostIdenticalLinearConstraints]
2.97e-06s 0.00e+00d [FindBigAtMostOneAndLinearOverlap]
7.00e-06s 4.00e-08d [FindBigVerticalLinearOverlap]
3.82e-06s 0.00e+00d [FindBigHorizontalLinearOverlap]
3.34e-06s 0.00e+00d [MergeClauses]
5.60e-06s 0.00e+00d [PresolveToFixPoint]
1.57e-05s 0.00e+00d [MergeNoOverlap]
3.21e-06s 0.00e+00d [MergeNoOverlap2D]
3.21e-05s 0.00e+00d [ExpandObjective]
Presolve summary:
- 960 affine relations were detected.
- rule 'affine: new relation' was applied 960 times.
- rule 'linear1: x in domain' was applied 4 times.
- rule 'linear: always true' was applied 1 time.
- rule 'linear: empty' was applied 599 times.
- rule 'linear: fixed or dup variables' was applied 604 times.
- rule 'linear: reduced variable domains' was applied 4 times.
- rule 'linear: remapped using affine relations' was applied 960 times.
- rule 'objective: variable not used elsewhere' was applied 478 times.
- rule 'presolve: 972 unused variables removed.' was applied 1 time.
- rule 'presolve: iteration' was applied 2 times.
Presolved optimization model '': (model_fingerprint: 0x8fa9deebc7ce54b4)
#Variables: 0 ( in objective) (0 primary variables)
[Symmetry] Graph for symmetry has 0 nodes and 0 arcs.
Preloading model.
#Bound 0.06s best:inf next:[4059914,4059914] initial_domain
The solution hint is complete and is feasible. Its objective value is 4059914.
#Model 0.06s var:0/0 constraints:0/0
Starting search at 0.06s with 8 workers.
6 full problem subsolvers: [default_lp(2), max_lp, no_lp, quick_restart, quick_restart_no_lp]
2 first solution subsolvers: [fj, fs_random_no_lp]
3 interleaved subsolvers: [feasibility_pump, ls, rins/rens]
2 helper subsolvers: [neighborhood_helper, synchronization_agent]
#1 0.07s best:4059914 next:[] fj_restart_obj(batch:1 lin{mvs:0 evals:0} #w_updates:0 #perturb:0)
Task timing n [ min, max] avg dev time n [ min, max] avg dev dtime
'default_lp': 1 [ 3.53ms, 3.53ms] 3.53ms 0.00ns 3.53ms 1 [ 10.00ns, 10.00ns] 10.00ns 0.00ns 10.00ns
'default_lp': 1 [ 4.16ms, 4.16ms] 4.16ms 0.00ns 4.16ms 1 [ 10.00ns, 10.00ns] 10.00ns 0.00ns 10.00ns
'feasibility_pump': 1 [ 2.81ms, 2.81ms] 2.81ms 0.00ns 2.81ms 0 [ 0.00ns, 0.00ns] 0.00ns 0.00ns 0.00ns
'fj': 1 [126.01us, 126.01us] 126.01us 0.00ns 126.01us 0 [ 0.00ns, 0.00ns] 0.00ns 0.00ns 0.00ns
'fs_random_no_lp': 1 [ 3.53ms, 3.53ms] 3.53ms 0.00ns 3.53ms 1 [ 10.00ns, 10.00ns] 10.00ns 0.00ns 10.00ns
'ls': 0 [ 0.00ns, 0.00ns] 0.00ns 0.00ns 0.00ns 0 [ 0.00ns, 0.00ns] 0.00ns 0.00ns 0.00ns
'max_lp': 1 [ 3.91ms, 3.91ms] 3.91ms 0.00ns 3.91ms 1 [ 10.00ns, 10.00ns] 10.00ns 0.00ns 10.00ns
'no_lp': 1 [ 4.17ms, 4.17ms] 4.17ms 0.00ns 4.17ms 1 [ 10.00ns, 10.00ns] 10.00ns 0.00ns 10.00ns
'quick_restart': 1 [ 3.76ms, 3.76ms] 3.76ms 0.00ns 3.76ms 1 [ 10.00ns, 10.00ns] 10.00ns 0.00ns 10.00ns
'quick_restart_no_lp': 1 [ 3.77ms, 3.77ms] 3.77ms 0.00ns 3.77ms 1 [ 10.00ns, 10.00ns] 10.00ns 0.00ns 10.00ns
'rins/rens': 0 [ 0.00ns, 0.00ns] 0.00ns 0.00ns 0.00ns 0 [ 0.00ns, 0.00ns] 0.00ns 0.00ns 0.00ns
Search stats Bools Conflicts Branches Restarts BacktrackToRoot Backtrack BoolPropag IntegerPropag
'default_lp': 0 0 0 0 0 0 0 0
'default_lp': 0 0 0 0 0 0 0 0
'fs_random_no_lp': 0 0 0 0 0 0 0 0
'max_lp': 0 0 0 0 0 0 0 0
'no_lp': 0 0 0 0 0 0 0 0
'quick_restart': 0 0 0 0 0 0 0 0
'quick_restart_no_lp': 0 0 0 0 0 0 0 0
SAT formula Fixed Equiv Total VarLeft BinaryClauses PermanentClauses TemporaryClauses
'default_lp': 0 0 0 0 0 0 0
'default_lp': 0 0 0 0 0 0 0
'fs_random_no_lp': 0 0 0 0 0 0 0
'max_lp': 0 0 0 0 0 0 0
'no_lp': 0 0 0 0 0 0 0
'quick_restart': 0 0 0 0 0 0 0
'quick_restart_no_lp': 0 0 0 0 0 0 0
SAT stats ClassicMinim LitRemoved LitRemovedBinary LitLearned LitForgotten Subsumed
'default_lp': 0 0 0 0 0 0
'default_lp': 0 0 0 0 0 0
'fs_random_no_lp': 0 0 0 0 0 0
'max_lp': 0 0 0 0 0 0
'no_lp': 0 0 0 0 0 0
'quick_restart': 0 0 0 0 0 0
'quick_restart_no_lp': 0 0 0 0 0 0
Vivification Clauses Decisions LitTrue Subsumed LitRemoved DecisionReused Conflicts
'default_lp': 0 0 0 0 0 0 0
'default_lp': 0 0 0 0 0 0 0
'fs_random_no_lp': 0 0 0 0 0 0 0
'max_lp': 0 0 0 0 0 0 0
'no_lp': 0 0 0 0 0 0 0
'quick_restart': 0 0 0 0 0 0 0
'quick_restart_no_lp': 0 0 0 0 0 0 0
Clause deletion at_true l_and_not(l) to_binary sub_conflict sub_extra sub_decisions sub_eager sub_vivify sub_probing sub_inpro blocked eliminated forgotten promoted conflicts
'default_lp': 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
'default_lp': 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
'fs_random_no_lp': 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
'max_lp': 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
'no_lp': 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
'quick_restart': 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
'quick_restart_no_lp': 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
LNS stats Improv/Calls Closed Difficulty TimeLimit
'rins/rens': 0/0 0% 5.00e-01 0.10
LS stats Batches Restarts/Perturbs LinMoves GenMoves CompoundMoves Bactracks WeightUpdates ScoreComputed
'fj_restart_obj': 1 1 0 0 0 0 0 0
Solutions (1) Num Rank
'fj_restart_obj': 2 [0,1]
Objective bounds Num
'initial_domain': 1
Solution repositories Added Queried Synchro
'alternative_path': 0 0 0
'best_solutions': 1 0 1
'fj solution hints': 0 0 0
'lp solutions': 0 0 0
'pump': 0 0
Clauses shared #Exported #Imported #BinaryRead #BinaryTotal
'default_lp': 0 0 0 0
'default_lp': 0 0 0 0
'fs_random_no_lp': 0 0 0 0
'max_lp': 0 0 0 0
'no_lp': 0 0 0 0
'quick_restart': 0 0 0 0
'quick_restart_no_lp': 0 0 0 0
LRAT_status: NA
CpSolverResponse summary:
status: OPTIMAL
objective: 4059914
best_bound: 4059914
integers: 1
booleans: 0
conflicts: 0
branches: 0
propagations: 0
integer_propagations: 0
restarts: 0
lp_iterations: 0
walltime: 0.0675319
usertime: 0.067532
deterministic_time: 0.00053871
gap_integral: 0
solution_fingerprint: 0x9551a020a00a044c