Textdoc
Zipdoc
Writeurl
Loading…
Starting CP-SAT solver v9.3.10497 Parameters: log_search_progress: true Setting number of workers to 8 Initial optimization model '': #Variables: 1004003 (#bools:1000 in objective) - 1002001 in [0,1] - 2000 in [1661198400,1661234400] - 2 constants in {0,1} #kBoolOr: 2000000 (#literals: 4000000) #kCircuit: 1 #kInterval: 1000 (#enforced: 1000) #kLinear1: 2000 (#enforced: 2000) #kLinear3: 1000000 (#enforced: 1000000) #kNoOverlap: 1001 (#intervals: 2000, #optional: 2000) Starting presolve at 0.43s [ExtractEncodingFromLinear] #potential_supersets=0 #potential_subsets=0 #at_most_one_encodings=0 #exactly_one_encodings=0 #unique_terms=0 #multiple_terms=0 #literals=0 time=0.0292221s [Probing] deterministic_time: 1.00018 (limit: 1) wall_time: 1.97208 (Aborted 3663/1003004) [Probing] - new integer bounds: 1000 [Probing] - new binary clause: 5305 [SAT presolve] num removable Booleans: 2 / 1004003 [SAT presolve] num trivial clauses: 0 [SAT presolve] [0s] clauses:2000000 literals:4000000 vars:1001001 one_side_vars:1000001 simple_definition:1000 singleton_clauses:0 [SAT presolve] [0.309976s] clauses:2000000 literals:4000000 vars:1001001 one_side_vars:1000001 simple_definition:1000 singleton_clauses:0 [SAT presolve] [0.346822s] clauses:2000000 literals:4000000 vars:1001001 one_side_vars:1000001 simple_definition:1000 singleton_clauses:0 [DetectDuplicateConstraints] #duplicates=0 time=1.15207s [DetectDominatedLinearConstraints] #relevant_constraints=0 #work_done=0 #num_inclusions=0 #num_redundant=0 time=0.0490809s [DetectOverlappingColumns] #processed_columns=0 #work_done=0 #nz_reduction=0 time=0.250004s [ProcessSetPPC] #relevant_constraints=2000000 #num_inclusions=0 work=12307656 time=1.41487s [Symmetry] Problem too large. Skipping. You can use symmetry_level:3 or more to force it. Presolve summary: - 0 affine relations were detected. - rule 'bool_or: implications' was applied 2000000 times. - rule 'deductions: 1003000 stored' was applied 1 time. - rule 'linear: fixed or dup variables' was applied 1000 times. - rule 'linear: simplified rhs' was applied 1998000 times. - rule 'no_overlap: only one interval' was applied 1000 times. - rule 'presolve: 2 unused variables removed.' was applied 1 time. - rule 'presolve: iteration' was applied 1 time. - rule 'variables: detect half reified value encoding' was applied 2000 times. Presolved optimization model '': #Variables: 1004001 (#bools:1000 in objective) - 1002001 in [0,1] - 1000 in [1661198400,1661234399] - 1000 in [1661198400,1661234400] #kBoolAnd: 2000 (#enforced: 2000) (#literals: 2000000) #kCircuit: 1 #kInterval: 1000 (#enforced: 1000) #kLinear1: 2000 (#enforced: 2000) #kLinear2: 1000000 (#enforced: 1000000) #kNoOverlap: 1 (#intervals: 1000, #optional: 1000) Preloading model. [Symmetry] Problem too large. Skipping. You can use symmetry_level:3 or more to force it. #Bound 37.94s best:-inf next:[-0,1000] initial_domain Starting Search at 39.45s with 8 workers. 6 full subsolvers: [default_lp, fixed, no_lp, max_lp, core, reduced_costs] Interleaved subsolvers: [feasibility_pump, rnd_var_lns_default, rnd_cst_lns_default, graph_var_lns_default, graph_cst_lns_default, scheduling_time_window_lns_default, scheduling_random_lns_default, routing_random_lns_default, routing_path_lns_default, rins_lns_default, rens_lns_default] #1 73.00s best:1000 next:[] core fixed_bools:1/1004001 #Done 73.09s core #Done 73.11s no_lp Process finished with exit code 137 (interrupted by signal 9: SIGKILL)