Skip to content

OR-Tools CP-SAT crashes with UNKNOWN answer #4733

@JulienVion

Description

@JulienVion

What version of OR-Tools and what language are you using?

Version 9.14 for Debian Sid with Minizinc 2.9.3 (fzn-cp-sat)

What did you do?

I try to solve somewhat large timetabling problem. I have been working on this problem for weeks with no issues, then OR-Tools suddenly crashes (UNKNOWN answer) on given instance.
Older version 9.12 works.

Here is the output:

%% Starting CP-SAT solver v9.14.6206
%% Parameters: log_search_progress: true log_to_stdout: false max_domain_size_when_encoding_eq_neq_constraints: 32 num_workers: 10
%% Initial optimization model 'mznfilenTsILS': (model_fingerprint: 0x1a2c4429bdfdde77)
%% #Variables: 305'000 (#ints: 1 in objective) (205'082 primary variables)
%% - 282'226 Booleans in [0,1]
%% - 235 different domains in [-59400,81910508] with a largest complexity of 60.
%% - 11'995 constants in {0,1,2,3,4,5,6,7,8,9,10,11 ... 568,569,571,572,573,574,575,577,578,579,580,581}
%% #kBoolAnd: 1'881 (#enforced: 1'881) (#literals: 5'643)
%% #kBoolOr: 238'225 (#enforced: 1'881) (#literals: 682'420)
%% #kCumulative: 50 (#intervals: 9'469, #fixed_intervals: 5'859)
%% #kElement: 1'782
%% #kIntDiv: 18
%% #kIntProd: 780
%% #kInterval: 1'272 (#fixed: 390)
%% #kLinMax: 198 (#expressions: 3'564)
%% #kLinear1: 349'719 (#enforced: 349'719)
%% #kLinear2: 104'803 (#enforced: 2'376)
%% #kLinear3: 4'129 (#enforced: 99)
%% #kLinearN: 17'370 (#terms: 200'059)
%% #kNoOverlap: 3 (#intervals: 192, #fixed_intervals: 122)
%% Starting presolve at 0.25s
%% The solution hint is incomplete: 882 out of 293005 non fixed variables hinted.
%% 6.80e-02s 0.00e+00d [DetectDominanceRelations]
%% 1.30e+00s 0.00e+00d [PresolveToFixPoint] #num_loops=16 #num_dual_strengthening=2
%% 6.42e-03s 0.00e+00d [ExtractEncodingFromLinear] #potential_supersets=171 #potential_subsets=213
%% 7.73e-03s 0.00e+00d [DetectDuplicateColumns]
%% 1.70e-02s 0.00e+00d [DetectDuplicateConstraints] #duplicates=491
%% [SAT presolve] num removable Booleans: 254 / 41651
%% [SAT presolve] num trivial clauses: 0
%% [SAT presolve] [0s] clauses:42970 literals:126021 vars:23762 one_side_vars:109 simple_definition:11640 singleton_clauses:0
%% [SAT presolve] [0.00928697s] clauses:42837 literals:125316 vars:23762 one_side_vars:112 simple_definition:11661 singleton_clauses:0
%% [SAT presolve] [0.0127427s] clauses:42393 literals:124420 vars:23553 one_side_vars:112 simple_definition:11673 singleton_clauses:0
%% 1.53e-02s 0.00e+00d [DetectDuplicateConstraintsWithDifferentEnforcements] #without_enforcements=2'120
%% 4.07e+00s 1.01e+00d *[Probe] #probed=28'141 #fixed_bools=3'520 #new_bounds=968 #equiv=675 #new_binary_clauses=509'394
%% 3.41e-01s 7.44e-01d [MaxClique] Merged 42'887(90'403 literals) into 31'034(77'341 literals) at_most_ones.
%% 6.25e-02s 0.00e+00d [DetectDominanceRelations]
%% 4.18e-01s 0.00e+00d [PresolveToFixPoint] #num_loops=4 #num_dual_strengthening=2
%% 2.99e-02s 0.00e+00d [ProcessAtMostOneAndLinear] #num_changes=145
%% 9.35e-03s 0.00e+00d [DetectDuplicateConstraints] #duplicates=373
%% 1.01e-02s 0.00e+00d [DetectDuplicateConstraintsWithDifferentEnforcements] #without_enforcements=212
%% 1.07e-02s 1.03e-04d [DetectDominatedLinearConstraints] #relevant_constraints=2'517 #num_inclusions=537 #num_redundant=142
%% 5.55e-03s 0.00e+00d [DetectDifferentVariables]
%% 2.46e-02s 1.39e-03d [ProcessSetPPC] #relevant_constraints=27'140 #num_inclusions=22'858
%% 6.55e-03s 3.58e-06d [FindAlmostIdenticalLinearConstraints] #num_tested_pairs=13 #found=1
%% 1.78e-02s 8.30e-03d [FindBigAtMostOneAndLinearOverlap]
%% 7.07e-03s 3.50e-03d [FindBigVerticalLinearOverlap]
%% 4.55e-03s 7.57e-05d [FindBigHorizontalLinearOverlap] #linears=1'152
%% 1.10e-02s 1.81e-04d [MergeClauses] #num_collisions=52 #num_merges=52 #num_saved_literals=104
%% 6.26e-02s 0.00e+00d [DetectDominanceRelations]
%% 2.65e-01s 0.00e+00d [PresolveToFixPoint] #num_loops=3 #num_dual_strengthening=2
%% 6.30e-02s 0.00e+00d [DetectDominanceRelations]
%% 2.36e-01s 0.00e+00d [PresolveToFixPoint] #num_loops=1 #num_dual_strengthening=1
%% 7.40e-03s 0.00e+00d [DetectDuplicateColumns]
%% 9.31e-03s 0.00e+00d [DetectDuplicateConstraints] #duplicates=1
%% [SAT presolve] num removable Booleans: 4 / 36694
%% [SAT presolve] num trivial clauses: 0
%% [SAT presolve] [0s] clauses:19193 literals:71629 vars:20485 one_side_vars:8529 simple_definition:7264 singleton_clauses:0
%% [SAT presolve] [0.00564241s] clauses:19140 literals:71378 vars:20484 one_side_vars:8535 simple_definition:7284 singleton_clauses:0
%% [SAT presolve] [0.0080213s] clauses:19140 literals:71378 vars:20484 one_side_vars:8535 simple_definition:7284 singleton_clauses:0
%% 8.01e-03s 0.00e+00d [DetectDuplicateConstraintsWithDifferentEnforcements] #without_enforcements=220
%% 4.75e+00s 1.01e+00d *[Probe] #probed=37'020 #fixed_bools=299 #new_bounds=140 #equiv=317 #new_binary_clauses=466'155
%% 3.44e-01s 7.61e-01d [MaxClique] Merged 24'503(63'596 literals) into 21'161(59'863 literals) at_most_ones.
%% 6.20e-02s 0.00e+00d [DetectDominanceRelations]
%% 2.67e-01s 0.00e+00d [PresolveToFixPoint] #num_loops=2 #num_dual_strengthening=1
%% 2.72e-02s 0.00e+00d [ProcessAtMostOneAndLinear] #num_changes=16
%% 9.77e-03s 0.00e+00d [DetectDuplicateConstraints] #duplicates=128
%% 8.65e-03s 0.00e+00d [DetectDuplicateConstraintsWithDifferentEnforcements] #without_enforcements=55
%% 9.93e-03s 6.22e-05d [DetectDominatedLinearConstraints] #relevant_constraints=2'269 #num_inclusions=362
%% 5.41e-03s 0.00e+00d [DetectDifferentVariables]
%% 2.51e-02s 1.18e-03d [ProcessSetPPC] #relevant_constraints=23'543 #num_inclusions=19'121
%% 6.54e-03s 3.27e-06d [FindAlmostIdenticalLinearConstraints] #num_tested_pairs=12
%% 1.76e-02s 8.22e-03d [FindBigAtMostOneAndLinearOverlap]
%% 7.01e-03s 3.40e-03d [FindBigVerticalLinearOverlap]
%% 4.65e-03s 7.29e-05d [FindBigHorizontalLinearOverlap] #linears=1'094
%% 1.09e-02s 1.76e-04d [MergeClauses] #num_collisions=75 #num_merges=75 #num_saved_literals=157
%% 6.24e-02s 0.00e+00d [DetectDominanceRelations]
%% 2.66e-01s 0.00e+00d [PresolveToFixPoint] #num_loops=3 #num_dual_strengthening=2
%% 6.32e-02s 0.00e+00d [DetectDominanceRelations]
%% 2.34e-01s 0.00e+00d [PresolveToFixPoint] #num_loops=1 #num_dual_strengthening=1
%% 7.55e-03s 0.00e+00d [DetectDuplicateColumns]
%% 1.12e-02s 0.00e+00d [DetectDuplicateConstraints] #duplicates=1
%% [SAT presolve] num removable Booleans: 0 / 36073
%% [SAT presolve] num trivial clauses: 0
%% [SAT presolve] [0s] clauses:14314 literals:60679 vars:19896 one_side_vars:11124 simple_definition:5498 singleton_clauses:0
%% [SAT presolve] [0.00339199s] clauses:14314 literals:60675 vars:19896 one_side_vars:11126 simple_definition:5496 singleton_clauses:0
%% [SAT presolve] [0.00553966s] clauses:14314 literals:60675 vars:19896 one_side_vars:11126 simple_definition:5496 singleton_clauses:0
%% 8.01e-03s 0.00e+00d [DetectDuplicateConstraintsWithDifferentEnforcements] #without_enforcements=55
%% 4.79e+00s 1.01e+00d *[Probe] #probed=38'163 #fixed_bools=80 #new_bounds=53 #equiv=47 #new_binary_clauses=453'642
%% 3.63e-01s 7.75e-01d [MaxClique] Merged 20'947(59'035 literals) into 20'302(58'293 literals) at_most_ones.
%% 6.40e-02s 0.00e+00d [DetectDominanceRelations]
%% 2.56e-01s 0.00e+00d [PresolveToFixPoint] #num_loops=2 #num_dual_strengthening=1
%% 2.82e-02s 0.00e+00d [ProcessAtMostOneAndLinear] #num_changes=1
%% 9.97e-03s 0.00e+00d [DetectDuplicateConstraints] #duplicates=18
%% 9.05e-03s 0.00e+00d [DetectDuplicateConstraintsWithDifferentEnforcements] #without_enforcements=32
%% 8.79e-03s 6.18e-05d [DetectDominatedLinearConstraints] #relevant_constraints=2'259 #num_inclusions=361
%% 6.60e-03s 0.00e+00d [DetectDifferentVariables]
%% 2.48e-02s 1.15e-03d [ProcessSetPPC] #relevant_constraints=23'073 #num_inclusions=18'568
%% 6.60e-03s 1.35e-06d [FindAlmostIdenticalLinearConstraints] #num_tested_pairs=5
%% 1.90e-02s 8.24e-03d [FindBigAtMostOneAndLinearOverlap]
%% 8.56e-03s 3.38e-03d [FindBigVerticalLinearOverlap]
%% 5.16e-03s 7.25e-05d [FindBigHorizontalLinearOverlap] #linears=1'091
%% 1.27e-02s 1.76e-04d [MergeClauses] #num_collisions=81 #num_merges=81 #num_saved_literals=169
%% 6.27e-02s 0.00e+00d [DetectDominanceRelations]
%% 2.35e-01s 0.00e+00d [PresolveToFixPoint] #num_loops=1 #num_dual_strengthening=1
%% 1.27e-02s 0.00e+00d [ExpandObjective] #entries=6'753 #tight_variables=268 #tight_constraints=205
%% Presolve summary:
%% - 29256 affine relations were detected.
%% - rule 'TODO dual: make linear1 equiv' was applied 17'228 times.
%% - rule 'TODO dual: only one blocking constraint?' was applied 2'770 times.
%% - rule 'TODO dual: tighten at most one' was applied 30 times.
%% - rule 'TODO duplicate: skipped identical encoding constraints' was applied 68 times.
%% - rule 'TODO int_div: single variable with large domain' was applied 15 times.
%% - rule 'TODO linear2: contains a Boolean.' was applied 407 times.
%% - rule 'TODO no_overlap: only size one !' was applied 18 times.
%% - rule 'affine: new relation' was applied 29'256 times.
%% - rule 'all_diff: expanded' was applied 6 times.
%% - rule 'all_diff: permutation expanded' was applied 1 time.
%% - rule 'all_diff: propagate fixed expressions' was applied 1 time.
%% - rule 'all_diff: remove fixed expressions' was applied 1 time.
%% - rule 'at_most_one: empty or all false' was applied 62 times.
%% - rule 'at_most_one: removed literals' was applied 6'520 times.
%% - rule 'at_most_one: satisfied' was applied 240 times.
%% - rule 'at_most_one: size one' was applied 5'771 times.
%% - rule 'at_most_one: transformed into max clique.' was applied 3 times.
%% - rule 'bool_and: always false' was applied 7'643 times.
%% - rule 'bool_and: merged constraints with same enforcement' was applied 104 times.
%% - rule 'bool_and: non-reified.' was applied 46'376 times.
%% - rule 'bool_and: x => x' was applied 210 times.
%% - rule 'bool_or: always true' was applied 111'570 times.
%% - rule 'bool_or: fixed literals' was applied 4'121 times.
%% - rule 'bool_or: implications' was applied 123'370 times.
%% - rule 'bool_or: only one literal' was applied 143'609 times.
%% - rule 'bool_or: removed enforcement literal' was applied 361 times.
%% - rule 'cumulative: convert to all_different' was applied 8 times.
%% - rule 'cumulative: convert to no_overlap' was applied 39 times.
%% - rule 'cumulative: max profile is always under the min capacity' was applied 4'125 times.
%% - rule 'cumulative: merged demand of identical interval' was applied 1'308 times.
%% - rule 'cumulative: split into disjoint components' was applied 48 times.
%% - rule 'deductions: 104849 stored' was applied 1 time.
%% - rule 'dual: enforced equivalence' was applied 112 times.
%% - rule 'dual: make encoding equiv' was applied 42'526 times.
%% - rule 'dual: reduced domain' was applied 1 time.
%% - rule 'duplicate: identical constraint with implied enforcements' was applied 1'603 times.
%% - rule 'duplicate: merged rhs of linear constraint' was applied 429 times.
%% - rule 'duplicate: remapped duplicate intervals' was applied 1 time.
%% - rule 'duplicate: removed constraint' was applied 1'012 times.
%% - rule 'duplicate: removed enforced constraint' was applied 376 times.
%% - rule 'element: fixed index' was applied 1'782 times.
%% - rule 'enforcement: false literal' was applied 17'504 times.
%% - rule 'enforcement: literal not used' was applied 139 times.
%% - rule 'enforcement: true literal' was applied 90'767 times.
%% - rule 'exactly_one: removed literals' was applied 18 times.
%% - rule 'exactly_one: singleton' was applied 18 times.
%% - rule 'exactly_one: size two' was applied 2 times.
%% - rule 'hint: moved var hint within its domain.' was applied 6 times.
%% - rule 'int_div: always true' was applied 15 times.
%% - rule 'int_div: linearize positive division with a constant divisor' was applied 3 times.
%% - rule 'int_div: target has been fixed by propagating X / cte' was applied 15 times.
%% - rule 'int_prod: boolean affine term' was applied 12 times.
%% - rule 'int_prod: constant product' was applied 559 times.
%% - rule 'int_prod: divide product by constant factor' was applied 35 times.
%% - rule 'int_prod: removed constant expressions.' was applied 1'118 times.
%% - rule 'int_square: reduced target domain.' was applied 941 times.
%% - rule 'intervals: removed unused interval' was applied 385 times.
%% - rule 'lin_max: converted to equality' was applied 194 times.
%% - rule 'lin_max: removed exprs' was applied 400 times.
%% - rule 'lin_max: target domain reduced' was applied 303 times.
%% - rule 'linear + amo: detect hidden AMO' was applied 93 times.
%% - rule 'linear + amo: empty after processing' was applied 21 times.
%% - rule 'linear + amo: extracted enforcement literal' was applied 566 times.
%% - rule 'linear + amo: fixed literal implied by enforcement' was applied 117 times.
%% - rule 'linear + amo: infeasible enforcement' was applied 27 times.
%% - rule 'linear + amo: removed enforcement literal' was applied 5 times.
%% - rule 'linear + amo: simplified enforcement list' was applied 3 times.
%% - rule 'linear + amo: trivial linear constraint' was applied 103 times.
%% - rule 'linear inclusion: redundant included constraint' was applied 15 times.
%% - rule 'linear inclusion: subset + singleton is equality' was applied 127 times.
%% - rule 'linear1: always true' was applied 39 times.
%% - rule 'linear1: canonicalized' was applied 6 times.
%% - rule 'linear1: transformed to implication' was applied 1'505 times.
%% - rule 'linear1: x in domain' was applied 88 times.
%% - rule 'linear2: Boolean with one feasible value.' was applied 102 times.
%% - rule 'linear2: contains a Boolean.' was applied 22 times.
%% - rule 'linear2: implied ax + by = cte has only one solution' was applied 4 times.
%% - rule 'linear: advanced affine relation from 2 constraints.' was applied 1 time.
%% - rule 'linear: always true' was applied 157'250 times.
%% - rule 'linear: coefficient strenghtening.' was applied 2 times.
%% - rule 'linear: divide by GCD' was applied 15'495 times.
%% - rule 'linear: empty' was applied 79'461 times.
%% - rule 'linear: enforcement literal in expression' was applied 66 times.
%% - rule 'linear: extracted at most one (max).' was applied 618 times.
%% - rule 'linear: extracted enforcement literal' was applied 205 times.
%% - rule 'linear: fixed or dup variables' was applied 181'888 times.
%% - rule 'linear: infeasible' was applied 35'264 times.
%% - rule 'linear: negative clause' was applied 888 times.
%% - rule 'linear: negative reified and' was applied 18 times.
%% - rule 'linear: positive at most one' was applied 256 times.
%% - rule 'linear: positive clause' was applied 3 times.
%% - rule 'linear: positive equal one' was applied 4 times.
%% - rule 'linear: positive reified and' was applied 1 time.
%% - rule 'linear: reduced variable domains' was applied 84'011 times.
%% - rule 'linear: reduced variable domains in derived constraint' was applied 158 times.
%% - rule 'linear: remapped using affine relations' was applied 25'074 times.
%% - rule 'linear: remove irrelevant part' was applied 29 times.
%% - rule 'linear: simplified rhs' was applied 52'242 times.
%% - rule 'linear: small Boolean expression' was applied 204 times.
%% - rule 'linear: variable substitution 0' was applied 9 times.
%% - rule 'linear: variable substitution 2' was applied 99 times.
%% - rule 'new_bool: integer encoding' was applied 4'151 times.
%% - rule 'new_bool: var with 2 values' was applied 1'685 times.
%% - rule 'no_overlap: merge constant contiguous intervals' was applied 2 times.
%% - rule 'no_overlap: merged constraints' was applied 1 time.
%% - rule 'no_overlap: split into disjoint components' was applied 5 times.
%% - rule 'presolve: 256697 unused variables removed.' was applied 1 time.
%% - rule 'presolve: iteration' was applied 3 times.
%% - rule 'probing: bool_or reduced to implication' was applied 564 times.
%% - rule 'probing: simplified clauses.' was applied 3'293 times.
%% - rule 'probing: simplified enforcement list.' was applied 5 times.
%% - rule 'setppc: bool_or in at_most_one.' was applied 14 times.
%% - rule 'setppc: removed dominated constraints' was applied 92 times.
%% - rule 'variables with 2 values: create encoding literal' was applied 1'685 times.
%% - rule 'variables with 2 values: merge encoding literals' was applied 5 times.
%% - rule 'variables with 2 values: new affine relation' was applied 1'693 times.
%% - rule 'variables with 2 values: register other encoding' was applied 3 times.
%% - rule 'variables: add encoding constraint' was applied 4'151 times.
%% - rule 'variables: both boolean and its negation fix the same variable' was applied 14 times.
%% - rule 'variables: canonicalize affine domain' was applied 117 times.
%% - rule 'variables: canonicalize domain' was applied 3 times.
%% - rule 'variables: detect fully reified value encoding' was applied 9'206 times.
%% - rule 'variables: detect half reified value encoding' was applied 23'300 times.
%% - rule 'variables: removable enforcement literal' was applied 530 times.
%% Error while validating postsolved model: Interval 48259 in constraint #48241 must appear before in the list of constraints :no_overlap { intervals: 1519 intervals: 1520 intervals: 1521 intervals: 1522 intervals: 1523 intervals: 1524 intervals: 1525 intervals: 48259 intervals: 1805 intervals: 1790 intervals: 1789 intervals: 1685 intervals: 1684 intervals: 1683 intervals: 1631 intervals: 1630 intervals: 1629 intervals: 1628 intervals: 1617 intervals: 1616 intervals: 1615 intervals: 1614 intervals: 1613 intervals: 1582 intervals: 1581 intervals: 1580 intervals: 1579 intervals: 1578 intervals: 1577 intervals: 1576 intervals: 1575 intervals: 1549 intervals: 1548 intervals: 1547 intervals: 1433 intervals: 1419 intervals: 1418 intervals: 1410 intervals: 1382 intervals: 1361 intervals: 1360 intervals: 1359 intervals: 1358 intervals: 1357 intervals: 1356 intervals: 1345 intervals: 1344 intervals: 1343 intervals: 1342 intervals: 1341 intervals: 1340 intervals: 1339 intervals: 1301 intervals: 1258 intervals: 1257 intervals: 1256 intervals: 1255 intervals: 1218 intervals: 1210 intervals: 1209 intervals: 1208 intervals: 1207 intervals: 1206 intervals: 1205 intervals: 1118 intervals: 1117 }
%% Problem closed by presolve.
%% CpSolverResponse summary:
%% status: MODEL_INVALID
%% objective: 0
%% best_bound: 0
%% integers: 0
%% booleans: 0
%% conflicts: 0
%% branches: 0
%% propagations: 0
%% integer_propagations: 0
%% restarts: 0
%% lp_iterations: 0
%% walltime: 19.8862
%% usertime: 19.8862
%% deterministic_time: 5.35744
%% gap_integral: 0
%%
=====UNKNOWN=====

timetable.zip

Metadata

Metadata

Assignees

Type

No type

Projects

No projects

Milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions