CP-SAT claims to find optimal solution to a MILP

[Stuart Rogers]

CP-SAT finds a solution to a MILP provided via a MPS file. The objective value is 73,656,558, which CP-SAT claims to be optimal (status: OPTIMAL). However, I know the optimal value is 27,370,900. Below is the CP-SAT console output.

$ solve --solver=sat --logtostderr --linear_solver_enable_verbose_output --input="input.mps" --sol_file="solution.sol" --params="cp_model_presolve:true" --num_threads=4 | tee output.txt

File        : 'input.mps'
Solver      : SAT_INTEGER_PROGRAMMING
Dimension   : 11993312 x 11983760

Running basic LP presolve, initial problem dimensions: 11993312 rows, 11983760 columns, 35940689 entries with magnitude in [1.000000e+00, 1.000000e+00]
glop::FixedVariablePreprocessor                        11993312 rows, 11983760 columns, 35940689 entries with magnitude in [1.000000e+00, 1.000000e+00]
glop::SingletonPreprocessor                            11993283 rows, 11983731 columns, 35940631 entries with magnitude in [1.000000e+00, 1.000000e+00]
glop::ForcingAndImpliedFreeConstraintPreprocessor      11993283 rows, 11983731 columns, 35940631 entries with magnitude in [1.000000e+00, 1.000000e+00]
glop::FreeConstraintPreprocessor                       11993283 rows, 11983731 columns, 35940631 entries with magnitude in [1.000000e+00, 1.000000e+00]
glop::UnconstrainedVariablePreprocessor                11993283 rows, 11983731 columns, 35940631 entries with magnitude in [1.000000e+00, 1.000000e+00]

Scaling to pure integer problem.
Num integers: 11983731/11983731 (implied: 0 in_inequalities: 0 max_scaling: 0) [IP]
Maximum constraint coefficient relative error: 0
Maximum constraint worst-case activity error: 0
Maximum constraint scaling factor: 1

Starting CP-SAT solver v9999.0.0
Parameters: log_search_progress: true cp_model_presolve: true num_search_workers: 4

Initial optimization model 'input.mps':
#Variables: 11983731 (#bools:11978461 in floating point objective)
  - 11983731 Booleans in [0,1]
#kLinear2: 11978468
#kLinear3: 23
#kLinearN: 14792 (#terms: 11983626)

Starting presolve at 2.37s
[Scaling] Floating point objective has 11978461 terms with magnitude in [2, 12732] average = 5309.28
[Scaling] Objective coefficient relative error: 0
[Scaling] Objective worst-case absolute error: 0
[Scaling] Objective scaling factor: 1
[ExtractEncodingFromLinear] #potential_supersets=14814 #potential_subsets=0 #at_most_one_encodings=0 #exactly_one_encodings=0 #unique_terms=0 #multiple_terms=0 #literals=0 time=0.135618s
[Probing] deterministic_time: 1.00039 (limit: 1) wall_time: 3.10116 (Aborted 5109/11983731)
[SAT presolve] num removable Booleans: 0 / 11983731
[SAT presolve] num trivial clauses: 0
[SAT presolve] [0s] clauses:11978468 literals:23956936 vars:11983731 one_side_vars:11983731 simple_definition:0 singleton_clauses:0
[SAT presolve] [1.34621s] clauses:11978468 literals:23956936 vars:11983731 one_side_vars:11983731 simple_definition:0 singleton_clauses:0
[SAT presolve] [1.59267s] clauses:11978468 literals:23956936 vars:11983731 one_side_vars:11983731 simple_definition:0 singleton_clauses:0
[DetectDuplicateConstraints] #duplicates=0 time=9.10448s
[DetectDominatedLinearConstraints] #relevant_constraints=1 #work_done=0 #num_inclusions=0 #num_redundant=0 time=0.225256s
[DetectOverlappingColumns] #processed_columns=0 #work_done=0 #nz_reduction=0 time=0.714752s
[ProcessSetPPC] #relevant_constraints=11993283 #num_inclusions=0 work=100001336 time=8.12962s
[Symmetry] Problem too large. Skipping. You can use symmetry_level:3 or more to force it.
[Probing] deterministic_time: 1.00039 (limit: 1) wall_time: 3.11291 (Aborted 5109/11983731)
[SAT presolve] num removable Booleans: 0 / 11983731
[SAT presolve] num trivial clauses: 0
[SAT presolve] [0s] clauses:11978468 literals:23956936 vars:11983731 one_side_vars:11983731 simple_definition:0 singleton_clauses:0
[SAT presolve] [1.80113s] clauses:11978468 literals:23956936 vars:11983731 one_side_vars:11983731 simple_definition:0 singleton_clauses:0
[SAT presolve] [2.0488s] clauses:11978468 literals:23956936 vars:11983731 one_side_vars:11983731 simple_definition:0 singleton_clauses:0
[DetectDuplicateConstraints] #duplicates=0 time=4.87825s
[DetectDominatedLinearConstraints] #relevant_constraints=1 #work_done=0 #num_inclusions=0 #num_redundant=0 time=0.225531s
[DetectOverlappingColumns] #processed_columns=0 #work_done=0 #nz_reduction=0 time=1.70797s
[ProcessSetPPC] #relevant_constraints=14815 #num_inclusions=0 work=35945804 time=2.49987s
[Symmetry] Problem too large. Skipping. You can use symmetry_level:3 or more to force it.

Presolve summary:
  - 0 affine relations were detected.
  - rule 'TODO linear2: contains a Boolean.' was applied 23956936 times.
  - rule 'bool_or: implications' was applied 11978468 times.
  - rule 'linear: negative clause' was applied 18 times.
  - rule 'linear: positive at most one' was applied 14814 times.
  - rule 'linear: positive clause' was applied 11978450 times.
  - rule 'linear: simplified rhs' was applied 11993282 times.
  - rule 'objective: expanded objective constraint.' was applied 1 time.
  - rule 'presolve: 0 unused variables removed.' was applied 1 time.
  - rule 'presolve: iteration' was applied 2 times.

Presolved optimization model 'input.mps':
#Variables: 11983731 (#bools:11983730 in objective)
  - 11983731 Booleans in [0,1]
#kAtMostOne: 14814 (#literals: 11978414)
#kBoolAnd: 5299 (#enforced: 5299) (#literals: 11978468)
#kLinearN: 1 (#terms: 5281)

Preloading model.
[Symmetry] Graph for symmetry has 35966008 nodes and 59908093 arcs.
[Symmetry] GraphSymmetryFinder error: During the initial refinement.
[Symmetry] Symmetry computation done. time: 10.5518 dtime: 10.2001
#Bound 421.24s best:inf   next:[-6.35216382e+10,75311048] initial_domain

Starting Search at 431.75s with 4 workers.
2 full subsolvers: [default_lp, no_lp]
Interleaved subsolvers: [feasibility_pump, rnd_var_lns_default, rnd_cst_lns_default, graph_var_lns_default, graph_cst_lns_default, rins_lns_default, rens_lns_default]
#Bound 484.17s best:inf   next:[15010363,75311048] default_lp initial_propagation
#1     489.79s best:73656558 next:[15010363,73656557] no_lp fixed_bools:0/11983731
#Done  490.22s no_lp

Solutions found per subsolver:
  'no_lp': 1

Objective bounds found per subsolver:
  'default_lp': 1
  'initial_domain': 1

CpSolverResponse summary:
status: OPTIMAL
objective: 73656558
best_bound: 73656558
booleans: 11983731
conflicts: 0
branches: 23714
propagations: 23074313
integer_propagations: 23105355
restarts: 10219
lp_iterations: 0
walltime: 541.928
usertime: 541.928
deterministic_time: 3.62577
gap_integral: 31.5774

Status      : MPSOLVER_OPTIMAL
Objective   : 7.365655800000000e+07
BestBound   : 7.365655800000000e+07
Iterations  : 0
Nodes       : 0
Time        : 582.5

[Laurent Perron]

Can you send us the mps ?

Which version ?

--
You received this message because you are subscribed to the Google Groups "or-tools-discuss" group.
To unsubscribe from this group and stop receiving emails from it, send an email to or-tools-discu...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/or-tools-discuss/c09c7cba-d69d-44d6-a8ad-75fb68385cf7n%40googlegroups.com.

[Stuart Rogers]

On Sunday, February 5, 2023 at 10:41:23 PM UTC-8 Laurent Perron wrote:

Can you send us the mps ?

The .mps.bz2 file is 179 MB. Where should it be uploaded? 

Which version ?

OR-Tools v9.4 

CP-SAT appears to be working properly, though very slowly, using 2 threads, as per the console output generated so far and shown below.

$ solve --solver=sat --logtostderr --linear_solver_enable_verbose_output --input="input.mps" --sol_file="solution.sol" --params="cp_model_presolve:true" --num_threads=2

File        : 'input.mps'
Solver      : SAT_INTEGER_PROGRAMMING
Dimension   : 11993312 x 11983760

Running basic LP presolve, initial problem dimensions: 11993312 rows, 11983760 columns, 35940689 entries with magnitude in [1.000000e+00, 1.000000e+00]
glop::FixedVariablePreprocessor                        11993312 rows, 11983760 columns, 35940689 entries with magnitude in [1.000000e+00, 1.000000e+00]
glop::SingletonPreprocessor                            11993283 rows, 11983731 columns, 35940631 entries with magnitude in [1.000000e+00, 1.000000e+00]
glop::ForcingAndImpliedFreeConstraintPreprocessor      11993283 rows, 11983731 columns, 35940631 entries with magnitude in [1.000000e+00, 1.000000e+00]
glop::FreeConstraintPreprocessor                       11993283 rows, 11983731 columns, 35940631 entries with magnitude in [1.000000e+00, 1.000000e+00]
glop::UnconstrainedVariablePreprocessor                11993283 rows, 11983731 columns, 35940631 entries with magnitude in [1.000000e+00, 1.000000e+00]

Scaling to pure integer problem.
Num integers: 11983731/11983731 (implied: 0 in_inequalities: 0 max_scaling: 0) [IP]
Maximum constraint coefficient relative error: 0
Maximum constraint worst-case activity error: 0
Maximum constraint scaling factor: 1

Starting CP-SAT solver v9999.0.0

Parameters: log_search_progress: true cp_model_presolve: true num_search_workers: 2

Initial optimization model 'input.mps':
#Variables: 11983731 (#bools:11978461 in floating point objective)
  - 11983731 Booleans in [0,1]
#kLinear2: 11978468
#kLinear3: 23
#kLinearN: 14792 (#terms: 11983626)

Starting presolve at 2.36s

[Scaling] Floating point objective has 11978461 terms with magnitude in [2, 12732] average = 5309.28
[Scaling] Objective coefficient relative error: 0
[Scaling] Objective worst-case absolute error: 0
[Scaling] Objective scaling factor: 1
[ExtractEncodingFromLinear] #potential_supersets=14814 #potential_subsets=0 #at_most_one_encodings=0 #exactly_one_encodings=0 #unique_terms=0 #multiple_terms=0 #literals=0 time=0.134646s

[Probing] deterministic_time: 1.00039 (limit: 1) wall_time: 3.07129 (Aborted 5109/11983731)

[SAT presolve] num removable Booleans: 0 / 11983731
[SAT presolve] num trivial clauses: 0
[SAT presolve] [0s] clauses:11978468 literals:23956936 vars:11983731 one_side_vars:11983731 simple_definition:0 singleton_clauses:0

[SAT presolve] [1.50631s] clauses:11978468 literals:23956936 vars:11983731 one_side_vars:11983731 simple_definition:0 singleton_clauses:0
[SAT presolve] [1.74489s] clauses:11978468 literals:23956936 vars:11983731 one_side_vars:11983731 simple_definition:0 singleton_clauses:0
[DetectDuplicateConstraints] #duplicates=0 time=9.14592s
[DetectDominatedLinearConstraints] #relevant_constraints=1 #work_done=0 #num_inclusions=0 #num_redundant=0 time=0.222703s
[DetectOverlappingColumns] #processed_columns=0 #work_done=0 #nz_reduction=0 time=0.718553s
[ProcessSetPPC] #relevant_constraints=11993283 #num_inclusions=0 work=100001336 time=8.03436s

[Symmetry] Problem too large. Skipping. You can use symmetry_level:3 or more to force it.

[Probing] deterministic_time: 1.00039 (limit: 1) wall_time: 3.09242 (Aborted 5109/11983731)

[SAT presolve] num removable Booleans: 0 / 11983731
[SAT presolve] num trivial clauses: 0
[SAT presolve] [0s] clauses:11978468 literals:23956936 vars:11983731 one_side_vars:11983731 simple_definition:0 singleton_clauses:0

[SAT presolve] [1.8114s] clauses:11978468 literals:23956936 vars:11983731 one_side_vars:11983731 simple_definition:0 singleton_clauses:0
[SAT presolve] [2.05769s] clauses:11978468 literals:23956936 vars:11983731 one_side_vars:11983731 simple_definition:0 singleton_clauses:0
[DetectDuplicateConstraints] #duplicates=0 time=4.91237s
[DetectDominatedLinearConstraints] #relevant_constraints=1 #work_done=0 #num_inclusions=0 #num_redundant=0 time=0.222896s
[DetectOverlappingColumns] #processed_columns=0 #work_done=0 #nz_reduction=0 time=1.70883s
[ProcessSetPPC] #relevant_constraints=14815 #num_inclusions=0 work=35945804 time=2.51836s

[Symmetry] Problem too large. Skipping. You can use symmetry_level:3 or more to force it.

Presolve summary:
  - 0 affine relations were detected.
  - rule 'TODO linear2: contains a Boolean.' was applied 23956936 times.
  - rule 'bool_or: implications' was applied 11978468 times.
  - rule 'linear: negative clause' was applied 18 times.
  - rule 'linear: positive at most one' was applied 14814 times.
  - rule 'linear: positive clause' was applied 11978450 times.
  - rule 'linear: simplified rhs' was applied 11993282 times.
  - rule 'objective: expanded objective constraint.' was applied 1 time.
  - rule 'presolve: 0 unused variables removed.' was applied 1 time.
  - rule 'presolve: iteration' was applied 2 times.

Presolved optimization model 'input.mps':
#Variables: 11983731 (#bools:11983730 in objective)
  - 11983731 Booleans in [0,1]
#kAtMostOne: 14814 (#literals: 11978414)
#kBoolAnd: 5299 (#enforced: 5299) (#literals: 11978468)
#kLinearN: 1 (#terms: 5281)

Preloading model.
[Symmetry] Graph for symmetry has 35966008 nodes and 59908093 arcs.
[Symmetry] GraphSymmetryFinder error: During the initial refinement.

[Symmetry] Symmetry computation done. time: 10.5263 dtime: 10.2001
#Bound 419.91s best:inf   next:[-6.35216382e+10,75311048] initial_domain

Starting Search at 429.87s with 2 workers.
1 full subsolvers: [default_lp]

Interleaved subsolvers: [feasibility_pump, rnd_var_lns_default, rnd_cst_lns_default, graph_var_lns_default, graph_cst_lns_default, rins_lns_default, rens_lns_default]

#Bound 476.25s best:inf   next:[15010363,75311048] default_lp initial_propagation
#1     553.17s best:46721339 next:[15010363,46721338] default_lp fixed_bools:0/11983731
#2     586.90s best:45667554 next:[15010363,45667553] rnd_var_lns_default(d=0.50 s=32 t=0.10 p=0.00)
#3     10356.96s best:42752280 next:[15010363,42752279] default_lp fixed_bools:0/11983731
#4     12961.92s best:42696344 next:[15010363,42696343] rins_lns_default_lp(d=0.50 s=36 t=0.10 p=0.00)
#5     12997.63s best:41436514 next:[15010363,41436513] rnd_var_lns_default(d=0.71 s=37 t=0.10 p=1.00)
#6     14045.10s best:39910566 next:[15010363,39910565] rins_lns_default_lp(d=0.71 s=41 t=0.10 p=1.00)
#7     14083.90s best:38572146 next:[15010363,38572145] rnd_var_lns_default(d=0.81 s=42 t=0.10 p=1.00)
#8     14656.05s best:38514818 next:[15010363,38514817] graph_cst_lns_default(d=0.19 s=45 t=0.10 p=0.00)
#9     14678.48s best:38401740 next:[15010363,38401739] rins_lns_default_lp(d=0.81 s=46 t=0.10 p=1.00)
#10    14718.95s best:38065064 next:[15010363,38065063] rnd_var_lns_default(d=0.88 s=47 t=0.10 p=1.00)
#11    14739.64s best:38060720 next:[15010363,38060719] rnd_cst_lns_default(d=0.12 s=48 t=0.10 p=0.00)
#12    14759.93s best:38041326 next:[15010363,38041325] graph_var_lns_default(d=0.12 s=49 t=0.10 p=0.00)
#13    15385.55s best:37997526 next:[15010363,37997525] rnd_var_lns_default(d=0.91 s=52 t=0.10 p=1.00)
#14    17356.67s best:37996048 next:[15010363,37996047] rins_lns_default_lp(d=0.91 s=56 t=0.10 p=1.00)
#15    33577.80s best:37990316 next:[15010363,37990315] rnd_var_lns_default(d=0.92 s=62 t=0.10 p=0.83)

[Laurent Perron]

If you have a Google drive, send me the link in pm

To view this discussion on the web visit https://groups.google.com/d/msgid/or-tools-discuss/102f41c9-12fa-41ae-8a1a-6d9b88fdd352n%40googlegroups.com.

[Laurent Perron]

For the record, 

Starting search at 488.11s with 24 workers.

13 full problem subsolvers: [default_lp, no_lp, max_lp, core, reduced_costs, pseudo_costs, quick_restart, quick_restart_no_lp, lb_tree_search, objective_lb_search, probing, probing_max_lp, objective_lb_search_max_lp]

8 first solution subsolvers: [random_0, random_quick_restart_0, random_1, random_quick_restart_1, random_2, random_quick_restart_2, random_3, random_quick_restart_3]

7 incomplete subsolvers: [feasibility_pump, rins_lns_default, rens_lns_default, rnd_var_lns_default, rnd_cst_lns_default, graph_var_lns_default, graph_cst_lns_default]

3 helper subsolvers: [synchronization_agent, neighborhood_helper, update_gap_integral]

#1     638.03s best:72906378 next:[-6.35216382e+10,72906377] quick_restart_no_lp fixed_bools:0/11983731

#2     720.24s best:71173910 next:[-6.35216382e+10,71173909] 

#3     724.01s best:70861153 next:[-6.35216382e+10,70861152] 

#Bound 789.03s best:70861153 next:[-6.31759637e+10,70861152] am1_presolve num_literals:11978461 num_am1:70 increase:345674490 work_done:100345259

#4     814.84s best:69830765 next:[-6.31759637e+10,69830764] 

#5     828.21s best:68737464 next:[-6.31759637e+10,68737463] 

#Bound 867.84s best:68737464 next:[-3.99911323e+10,68737463] objective_lb_search_max_lp initial_propagation

#Bound 896.11s best:68737464 next:[-2.33436236e+10,68737463] max_lp initial_propagation

#Bound 944.75s best:68737464 next:[-5.29631876e+09,68737463] max_lp

#Bound 967.08s best:68737464 next:[-3.05983328e+09,68737463] max_lp

#Bound 976.14s best:68737464 next:[-1.02091464e+09,68737463] max_lp

#Bound 987.92s best:68737464 next:[-296630484,68737463] max_lp

takes, according to top 

1351.1g 221.0g   9804 S  1232  87.9 177:24.66 solve 

Laurent Perron | Operations Research | lpe...@google.com | (33) 1 42 68 53 00

To view this discussion on the web visit https://groups.google.com/d/msgid/or-tools-discuss/CAPyyUTvf58%3DfJ3awJukWtKLpLC1Y0yMzgPxe46%3Dt6T_PHbiEaA%40mail.gmail.com.

[Stuart Rogers]

What are your machine specs? My machine has an AMD Ryzen Threadripper 3960X 24-Core Processor (48 logical cores with hyper-threading) and 128 GB RAM and runs Ubuntu 20.04.5 LTS. CP-SAT is killed on my machine when the number of threads is set to 24, regardless of whether presolve is true or false. It's also killed when the number of threads is set to 8.

[Laurent Perron]

On a machine with more memory (512GB) and with 16 workers

Starting search at 496.10s with 16 workers.

10 full problem subsolvers: [default_lp, no_lp, max_lp, core, reduced_costs, pseudo_costs, quick_restart, quick_restart_no_lp, lb_tree_search, probing]

4 first solution subsolvers: [random_0, random_quick_restart_0, random_1, random_quick_restart_1]

7 incomplete subsolvers: [feasibility_pump, rins_lns_default, rens_lns_default, rnd_var_lns_default, rnd_cst_lns_default, graph_var_lns_default, graph_cst_lns_default]

3 helper subsolvers: [synchronization_agent, neighborhood_helper, update_gap_integral]

#Bound 541.12s best:inf   next:[-6.31759637e+10,75311048] am1_presolve num_literals:11978461 num_am1:70 increase:345674490 work_done:100345259

#1     557.03s best:73565894 next:[-6.31759637e+10,73565893] no_lp fixed_bools:0/11983731

#2     557.54s best:72906378 next:[-6.31759637e+10,72906377] quick_restart_no_lp fixed_bools:0/11983731

#3     623.44s best:70975446 next:[-6.31759637e+10,70975445] 

#Bound 625.98s best:70975446 next:[-6.3175951e+10,70975445] bool_core num_cores:1 [core:2 mw:12728 d:0] assumptions:11978454 depth:1 fixed_bools:0/11983802

#Bound 628.61s best:70975446 next:[-6.31759382e+10,70975445] bool_core num_cores:2 [core:2 mw:12728 d:1] assumptions:11978454 depth:1 fixed_bools:0/11983803

#Bound 641.06s best:70975446 next:[-3.99911323e+10,70975445] reduced_costs initial_propagation

#Bound 650.91s best:70975446 next:[-2.33436236e+10,70975445] max_lp initial_propagation

#Bound 666.05s best:70975446 next:[-5.29631876e+09,70975445] max_lp

#Bound 672.67s best:70975446 next:[-3.05983328e+09,70975445] max_lp

#Bound 679.65s best:70975446 next:[-1.02091464e+09,70975445] max_lp

#Bound 685.73s best:70975446 next:[-296630484,70975445] max_lp

#Bound 695.86s best:70975446 next:[-7477247,70975445] max_lp

#Bound 700.25s best:70975446 next:[15009812,70975445] max_lp

#Bound 710.53s best:70975446 next:[15250160,70975445] max_lp

#Bound 714.21s best:70975446 next:[15319564,70975445] max_lp

#Bound 721.93s best:70975446 next:[15401709,70975445] max_lp

#4     723.28s best:69939758 next:[15401709,69939757] core fixed_bools:0/11983818

#Bound 725.07s best:69939758 next:[15428410,69939757] max_lp

#Bound 727.61s best:69939758 next:[15443962,69939757] max_lp

#Bound 732.85s best:69939758 next:[15507446,69939757] max_lp

#Bound 736.41s best:69939758 next:[15594859,69939757] max_lp

#Bound 744.41s best:69939758 next:[15717649,69939757] max_lp

#Bound 747.75s best:69939758 next:[15756700,69939757] max_lp

#Bound 754.43s best:69939758 next:[15781371,69939757] max_lp

#Bound 759.11s best:69939758 next:[15799121,69939757] max_lp

#Bound 766.10s best:69939758 next:[15919042,69939757] max_lp

#Bound 770.06s best:69939758 next:[15980355,69939757] max_lp

#5     770.29s best:45079459 next:[15980355,45079458] default_lp fixed_bools:0/11983731

#Bound 777.44s best:45079459 next:[16030051,45079458] max_lp

#Bound 781.22s best:45079459 next:[16051079,45079458] max_lp

#Bound 784.31s best:45079459 next:[16746088,45079458] lb_tree_search initial_propagation

#6     833.35s best:44443131 next:[16746088,44443130] default_lp fixed_bools:0/11983731

#7     874.45s best:44442811 next:[16746088,44442810] 

#8     917.32s best:44432459 next:[16746088,44432458] 

#9     992.53s best:44423563 next:[16746088,44423562] 

#Bound 999.93s best:44423563 next:[17711971,44423562] lb_tree_search

#10    1064.91s best:36942451 next:[17711971,36942450] default_lp fixed_bools:0/11983731

#11    1098.72s best:36780976 next:[17711971,36780975] default_lp fixed_bools:0/11983731

#12    1127.17s best:33074613 next:[17711971,33074612] default_lp fixed_bools:0/11983731

#13    1198.14s best:32656437 next:[17711971,32656436] rnd_cst_lns_default(d=0.13 s=66 t=0.1

Which would indicate the problem is fixed on the main branch.

Laurent Perron | Operations Research | lpe...@google.com | (33) 1 42 68 53 00

[Laurent Perron]

large amd 

AMD EPYC 7B12

512 GB of mem.

Laurent Perron | Operations Research | lpe...@google.com | (33) 1 42 68 53 00

To view this discussion on the web visit https://groups.google.com/d/msgid/or-tools-discuss/8a5d2301-e7bc-4354-a166-0622fc8e55fdn%40googlegroups.com.

[Stuart Rogers]

Is this problem still running on the large AMD? Did CP-SAT find a better or optimal solution?

[Laurent Perron]

8 workers:

#Bound 822.20s best:44423563 next:[16965891,44423562] max_lp

#Bound 829.15s best:44423563 next:[16992514,44423562] max_lp

...

Laurent Perron | Operations Research | lpe...@google.com | (33) 1 42 68 53 00

To view this discussion on the web visit https://groups.google.com/d/msgid/or-tools-discuss/1d787b90-5c4e-4dcf-b13b-bd486b412404n%40googlegroups.com.

[Laurent Perron]

#Bound 1269.52s best:33038197 next:[18207481,33038196] max_lp

#Bound 1288.34s best:33038197 next:[18218748,33038196] max_lp

Laurent Perron | Operations Research | lpe...@google.com | (33) 1 42 68 53 00

[Stuart Rogers]

I downloaded and installed the main branch version of OR-Tools. Using 4 threads, CP-SAT still claims an optimal solution when it has found a suboptimal solution.

$ ~/or-tools_main_2_7_2023/or-tools/bazel-bin/examples/cpp/solve --solver=sat --logtostderr --linear_solver_enable_verbose_output --input=input.mps --sol_file="cp_sat_red.sol" --params="cp_model_presolve:true" --num_threads=4

.....

total cuts added: 0 (out of 0 calls)
    LP statistics:
      final dimension: 0 rows, 1679 columns, 0 entries with magnitude in [0.000000e+00, 0.000000e+00]
      total number of simplex iterations: 0
      total num cut propagation: 0
      num solves:
      managed constraints: 1
      total cuts added: 0 (out of 0 calls)
    LP statistics:
      final dimension: 0 rows, 2053 columns, 0 entries with magnitude in [0.000000e+00, 0.000000e+00]
      total number of simplex iterations: 0
      total num cut propagation: 0
      num solves:
      managed constraints: 1
      total cuts added: 0 (out of 0 calls)
    LP statistics:
      final dimension: 0 rows, 1949 columns, 0 entries with magnitude in [0.000000e+00, 0.000000e+00]
      total number of simplex iterations: 0
      total num cut propagation: 0
      num solves:
      managed constraints: 1
      total cuts added: 0 (out of 0 calls)
    LP statistics:
      final dimension: 0 rows, 993 columns, 0 entries with magnitude in [0.000000e+00, 0.000000e+00]
      total number of simplex iterations: 0
      total num cut propagation: 0
      num solves:
      managed constraints: 1
      total cuts added: 0 (out of 0 calls)
    LP statistics:
      final dimension: 0 rows, 1939 columns, 0 entries with magnitude in [0.000000e+00, 0.000000e+00]
      total number of simplex iterations: 0
      total num cut propagation: 0
      num solves:
      managed constraints: 1
      total cuts added: 0 (out of 0 calls)
    LP statistics:
      final dimension: 0 rows, 293 columns, 0 entries with magnitude in [0.000000e+00, 0.000000e+00]
      total number of simplex iterations: 0
      total num cut propagation: 0
      num solves:
      managed constraints: 1
      total cuts added: 0 (out of 0 calls)
    Skipping other LPs...
      - 14815 total independent LPs.

Solutions found per subsolver:
  'no_lp': 1

Objective bounds found per subsolver:

  'initial_domain': 1

CpSolverResponse summary:
status: OPTIMAL

objective: 73565894
best_bound: 73565894
booleans: 11983731
conflicts: 0
branches: 10218
propagations: 11104078
integer_propagations: 11114397
restarts: 10218
lp_iterations: 0
walltime: 1182.24
usertime: 1182.24
deterministic_time: 3.27076
gap_integral: 31.5919
solution_fingerprint: 0xb75edbc17143d2a2

Status      : MPSOLVER_OPTIMAL
Objective   : 7.356589400000000e+07
BestBound   : 7.356589400000000e+07
Iterations  : 0
Nodes       : 0
Time        : 1228

[Laurent Perron]

You are right, I used the internal code, which is supposed to the same of the or-tools version. 

I am debugging.

This being said, the model is actually much smaller in the sat world

#Variables: 11983731 (#bools:11978461 in objective)

  - 11983731 Booleans in [0,1]

#kAtMostOne: 14814 (#literals: 11978414)

#kBoolAnd: 5299 (#enforced: 5299) (#literals: 11983767)

#kLinearN: 1 (#terms: 5281)

Laurent Perron | Operations Research | lpe...@google.com | (33) 1 42 68 53 00

To view this discussion on the web visit https://groups.google.com/d/msgid/or-tools-discuss/91e5f159-5f5e-4b7b-90f3-d7ec9663440en%40googlegroups.com.

[Laurent Perron]

To further the plot, it seems to work fine on mac using 1 thread (I do not have the memory to run in parallel).

Laurent Perron | Operations Research | lpe...@google.com | (33) 1 42 68 53 00

[Laurent Perron]

Starting CP-SAT solver v9.5.9999

Parameters: log_search_progress: true cp_model_presolve: false linearization_level: 0 num_workers: 1

Initial optimization model '/data/stuart/gen_MPS_files/p10_fix2_MILP_binary_x.mps': (model_fingerprint: 0xf94700dd262667c6)

#Variables: 11983731 (#bools:11978461 in objective)

  - 11983731 Booleans in [0,1]

#kAtMostOne: 14814 (#literals: 11978414)

#kBoolAnd: 5299 (#enforced: 5299) (#literals: 11983767)

#kLinearN: 1 (#terms: 5281)

Starting presolve at 2.17s

Presolve summary:

  - 0 affine relations were detected.

Presolved optimization model '/data/stuart/gen_MPS_files/p10_fix2_MILP_binary_x.mps': (model_fingerprint: 0xf94700dd262667c6)

#Variables: 11983731 (#bools:11978461 in objective)

  - 11983731 Booleans in [0,1]

#kAtMostOne: 14814 (#literals: 11978414)

#kBoolAnd: 5299 (#enforced: 5299) (#literals: 11983767)

#kLinearN: 1 (#terms: 5281)

Preloading model.

#Bound  17.77s best:inf   next:[-6.35216382e+10,75311048] initial_domain

[Symmetry] Graph for symmetry has 35966008 nodes and 59908093 arcs.

[Symmetry] Graph too large. Skipping. You can use symmetry_level:3 or more to force it.

Starting to load the model at 28.94s

Starting sequential search at 69.48s

#1      79.06s best:73565894 next:[-6.35216382e+10,73565893]  fixed_bools:0/11983731

#2      83.73s best:73554558 next:[-6.35216382e+10,73554557]  fixed_bools:0/11983731

#3     101.25s best:73554552 next:[-6.35216382e+10,73554551]  fixed_bools:0/11983731

#4     106.14s best:46685248 next:[-6.35216382e+10,46685247]  fixed_bools:0/11983731

Laurent Perron | Operations Research | lpe...@google.com | (33) 1 42 68 53 00

[Stuart Rogers]

Is this problem still running on the large AMD?

[Laurent Perron]

No, it got killed

Laurent Perron | Operations Research | lpe...@google.com | (33) 1 42 68 53 00

To view this discussion on the web visit https://groups.google.com/d/msgid/or-tools-discuss/9c450307-8c3e-4a6f-ad81-1eac8481acabn%40googlegroups.com.

[Laurent Perron]

I relaunched it with 4 workers with the following parameters:

--params num_workers:4,subsolvers:\"no_lp\",subsolvers:\"max_lp\"

It will create a solver with 4 workers: no_lp for fast solutions, max_lp for the lb, and 2 LNS workers.

Promising so far (still on our internal code)

Starting search at 27.37s with 4 workers.

2 full problem subsolvers: [no_lp, max_lp]

1 first solution subsolver: [random_0]

7 incomplete subsolvers: [feasibility_pump, rins_lns_default, rens_lns_default, rnd_var_lns_default, rnd_cst_lns_default, graph_var_lns_default, graph_cst_lns_default]

3 helper subsolvers: [synchronization_agent, neighborhood_helper, update_gap_integral]

#1      60.70s best:73565894 next:[-6.35216382e+10,73565893] no_lp fixed_bools:0/11983731

#2      64.20s best:73554558 next:[-6.35216382e+10,73554557] no_lp fixed_bools:0/11983731

#3      76.58s best:73554552 next:[-6.35216382e+10,73554551] no_lp fixed_bools:0/11983731

#4      80.20s best:46685248 next:[-6.35216382e+10,46685247] no_lp fixed_bools:0/11983731

#Bound 103.45s best:46685248 next:[-2.33436236e+10,46685247] max_lp initial_propagation

#Bound 109.58s best:46685248 next:[-5.29631876e+09,46685247] max_lp

#Bound 113.10s best:46685248 next:[-3.05983328e+09,46685247] max_lp

#Bound 116.30s best:46685248 next:[-1.02091464e+09,46685247] max_lp

#Bound 119.09s best:46685248 next:[-296630484,46685247] max_lp

#Bound 124.85s best:46685248 next:[-7477247,46685247] max_lp

#Bound 127.05s best:46685248 next:[15009812,46685247] max_lp

#Bound 133.26s best:46685248 next:[15250160,46685247] max_lp

#Bound 135.33s best:46685248 next:[15319564,46685247] max_lp

#Bound 139.96s best:46685248 next:[15401709,46685247] max_lp

#Bound 142.00s best:46685248 next:[15428410,46685247] max_lp

#Bound 146.59s best:46685248 next:[15455072,46685247] max_lp

#Bound 148.68s best:46685248 next:[15507243,46685247] max_lp

#Bound 155.18s best:46685248 next:[15663396,46685247] max_lp

#Bound 158.31s best:46685248 next:[15718824,46685247] max_lp

#Bound 164.56s best:46685248 next:[15767820,46685247] max_lp

#Bound 167.75s best:46685248 next:[15782197,46685247] max_lp

#Bound 174.47s best:46685248 next:[15827096,46685247] max_lp

#Bound 177.89s best:46685248 next:[15927000,46685247] max_lp

#Bound 184.98s best:46685248 next:[15992456,46685247] max_lp

#Bound 188.24s best:46685248 next:[16028155,46685247] max_lp

#Bound 194.94s best:46685248 next:[16055000,46685247] max_lp

#Bound 198.09s best:46685248 next:[16067539,46685247] max_lp

#Bound 204.70s best:46685248 next:[16141408,46685247] max_lp

#Bound 208.38s best:46685248 next:[16217479,46685247] max_lp

#Bound 215.63s best:46685248 next:[16261396,46685247] max_lp

#Bound 219.08s best:46685248 next:[16285963,46685247] max_lp

#Bound 226.05s best:46685248 next:[16302891,46685247] max_lp

#Bound 229.36s best:46685248 next:[16315349,46685247] max_lp

#Bound 238.45s best:46685248 next:[16365492,46685247] max_lp

#Bound 241.96s best:46685248 next:[16439295,46685247] max_lp

#Bound 248.40s best:46685248 next:[16474834,46685247] max_lp

#Bound 251.93s best:46685248 next:[16494023,46685247] max_lp

#Bound 259.59s best:46685248 next:[16509869,46685247] max_lp

Laurent Perron | Operations Research | lpe...@google.com | (33) 1 42 68 53 00

[Stuart Rogers]

When I use 1 thread, CP-SAT exits without any explanation after generating 6 solutions.

$ ~/or-tools_main_2_7_2023/or-tools/bazel-bin/examples/cpp/solve --solver=sat --logtostderr --linear_solver_enable_verbose_output --input=input.mps --sol_file="cp_sat_red_1_thread.sol" --params="cp_model_presolve:true" --num_threads=1 | tee cp_sat_red_1_thread_output.txt

File        : '/data/stuart/PaPILO_files_MILP_binary_x/p10_fix2_red.mps'

Solver      : SAT_INTEGER_PROGRAMMING
Dimension   : 11993312 x 11983760

Running basic LP presolve, initial problem dimensions: 11993312 rows, 11983760 columns, 35940689 entries with magnitude in [1.000000e+00, 1.000000e+00]
glop::FixedVariablePreprocessor                        11993312 rows, 11983760 columns, 35940689 entries with magnitude in [1.000000e+00, 1.000000e+00]
glop::SingletonPreprocessor                            11993283 rows, 11983731 columns, 35940631 entries with magnitude in [1.000000e+00, 1.000000e+00]
glop::ForcingAndImpliedFreeConstraintPreprocessor      11993283 rows, 11983731 columns, 35940631 entries with magnitude in [1.000000e+00, 1.000000e+00]
glop::FreeConstraintPreprocessor                       11993283 rows, 11983731 columns, 35940631 entries with magnitude in [1.000000e+00, 1.000000e+00]
glop::UnconstrainedVariablePreprocessor                11993283 rows, 11983731 columns, 35940631 entries with magnitude in [1.000000e+00, 1.000000e+00]

Scaling to pure integer problem.
Num integers: 11983731/11983731 (implied: 0 in_inequalities: 0 max_scaling: 0) [IP]
Maximum constraint coefficient relative error: 0
Maximum constraint worst-case activity error: 0
Maximum constraint scaling factor: 1

Starting CP-SAT solver v9.5.9999
Parameters: log_search_progress: true cp_model_presolve: true num_workers: 1

Initial optimization model '/data/stuart/gen_MPS_files/p10_fix2_MILP_binary_x.mps': (model_fingerprint: 0x43e5d1e353c6a5e7)

#Variables: 11983731 (#bools:11978461 in floating point objective)
  - 11983731 Booleans in [0,1]
#kLinear2: 11978468
#kLinear3: 23
#kLinearN: 14792 (#terms: 11983626)

Starting presolve at 2.77s

[Scaling] Floating point objective has 11978461 terms with magnitude in [2, 12732] average = 5309.28
[Scaling] Objective coefficient relative error: 0
[Scaling] Objective worst-case absolute error: 0
[Scaling] Objective scaling factor: 1

[ExtractEncodingFromLinear] #potential_supersets=14814 #potential_subsets=0 #at_most_one_encodings=0 #exactly_one_encodings=0 #unique_terms=0 #multiple_terms=0 #literals=0 time=0.143494s

[Symmetry] Problem too large. Skipping. You can use symmetry_level:3 or more to force it.

[SAT presolve] num removable Booleans: 0 / 11983731
[SAT presolve] num trivial clauses: 0
[SAT presolve] [0s] clauses:11978468 literals:23956936 vars:11983731 one_side_vars:11983731 simple_definition:0 singleton_clauses:0

[SAT presolve] [1.14258s] clauses:11978468 literals:23956936 vars:11983731 one_side_vars:11983731 simple_definition:0 singleton_clauses:0
[SAT presolve] [1.38035s] clauses:11978468 literals:23956936 vars:11983731 one_side_vars:11983731 simple_definition:0 singleton_clauses:0
[Probing] deterministic_time: 1.00039 (limit: 1) wall_time: 3.76081 (Aborted 5109/11983731)
[Probing] implications and bool_or (work_done=20454).
[DetectDuplicateConstraints] #duplicates=0 #without_enforcements=0 time=12.2092s
[DetectDominatedLinearConstraints] #relevant_constraints=1 #work_done=0 #num_inclusions=0 #num_redundant=0 time=0.146523s
[ProcessSetPPC] #relevant_constraints=11993283 #num_inclusions=0 work=100001336 time=8.40579s
[FindBigLinearOverlap] #blocks=0 #saved_nz=0 #linears=1 #work_done=5281/1e+09 time=0.143359s
[MergeClauses] #num_collisions=0 #num_merges=0 #num_saved_literals=0 work=0/100000000 time=0.448455s

[Symmetry] Problem too large. Skipping. You can use symmetry_level:3 or more to force it.

[SAT presolve] num removable Booleans: 0 / 11983731
[SAT presolve] num trivial clauses: 0
[SAT presolve] [0s] clauses:11978468 literals:23956936 vars:11983731 one_side_vars:11983731 simple_definition:0 singleton_clauses:0

[SAT presolve] [1.90428s] clauses:11978468 literals:23956936 vars:11983731 one_side_vars:11983731 simple_definition:0 singleton_clauses:0
[SAT presolve] [2.14565s] clauses:11978468 literals:23956936 vars:11983731 one_side_vars:11983731 simple_definition:0 singleton_clauses:0
[Probing] deterministic_time: 1.00039 (limit: 1) wall_time: 3.87754 (Aborted 5109/11983731)
[Probing] implications and bool_or (work_done=20454).
[DetectDuplicateConstraints] #duplicates=0 #without_enforcements=0 time=13.5186s
[DetectDominatedLinearConstraints] #relevant_constraints=1 #work_done=0 #num_inclusions=0 #num_redundant=0 time=0.236384s
[ProcessSetPPC] #relevant_constraints=11993283 #num_inclusions=0 work=100001336 time=11.4696s
[FindBigLinearOverlap] #blocks=0 #saved_nz=0 #linears=1 #work_done=5281/1e+09 time=0.230207s
[MergeClauses] #num_collisions=0 #num_merges=0 #num_saved_literals=0 work=0/100000000 time=0.876525s
[ExpandObjective] #propagations=0 #entries=0 #tight_variables=0 #tight_constraints=0 #expands=0 #issues=0 time=3.2917s

Presolve summary:
  - 0 affine relations were detected.

  - rule 'TODO dual: only one blocking constraint?' was applied 31686 times.
  - rule 'TODO dual: only one unspecified blocking constraint?' was applied 71870700 times.

  - rule 'TODO linear2: contains a Boolean.' was applied 23956936 times.
  - rule 'bool_or: implications' was applied 11978468 times.
  - rule 'linear: negative clause' was applied 18 times.
  - rule 'linear: positive at most one' was applied 14814 times.
  - rule 'linear: positive clause' was applied 11978450 times.
  - rule 'linear: simplified rhs' was applied 11993282 times.

  - rule 'presolve: 0 unused variables removed.' was applied 1 time.
  - rule 'presolve: iteration' was applied 2 times.

Presolved optimization model '/data/stuart/gen_MPS_files/p10_fix2_MILP_binary_x.mps': (model_fingerprint: 0xf94700dd262667c6)
#Variables: 11983731 (#bools:11978461 in objective)

  - 11983731 Booleans in [0,1]
#kAtMostOne: 14814 (#literals: 11978414)

#kBoolAnd: 5299 (#enforced: 5299) (#literals: 11983767)

#kLinearN: 1 (#terms: 5281)

Preloading model.

#Bound 568.40s best:inf   next:[-6.35216382e+10,75311048] initial_domain

[Symmetry] Graph for symmetry has 35966008 nodes and 59908093 arcs.

[Symmetry] Graph too large. Skipping. You can use symmetry_level:3 or more to force it.

Starting to load the model at 578.82s
#Bound 972.04s best:inf   next:[15010363,75311048]  initial_propagation

Starting sequential search at 973.00s
#1     998.36s best:45079459 next:[15010363,45079458]  fixed_bools:0/11983731
#2     1045.32s best:44443131 next:[15010363,44443130]  fixed_bools:0/11983731
#3     1180.09s best:36942451 next:[15010363,36942450]  fixed_bools:0/11983731
#4     1345.75s best:35208470 next:[15010363,35208469]  fixed_bools:0/11983731
#5     1383.85s best:34955948 next:[15010363,34955947]  fixed_bools:0/11983731
#6     3116.60s best:34955943 next:[15010363,34955942]  fixed_bools:0/11983731

[Laurent Perron]

It exits? Or it does not find improving solutions ?

I have the second behavior.

To view this discussion on the web visit https://groups.google.com/d/msgid/or-tools-discuss/8fa51181-e8d6-461c-8d97-4d8b03899cdan%40googlegroups.com.

[Stuart Rogers]

Does CP-SAT print a statement stating that it could not find improving solutions? Is there a time limit that determines when CP-SAT quits searching for an improved solution? In my experiments, there is no explanation printed to the console about why CP-SAT stopped searching.

[Laurent Perron]

Normally, it prints an exit log with metrics from the search.

To view this discussion on the web visit https://groups.google.com/d/msgid/or-tools-discuss/8f6179df-7122-4676-85db-079af4ac8acdn%40googlegroups.com.

--

--Laurent

[Stuart Rogers]

No exit log is printed to the console. I pasted all the output that was printed to the console by CP-SAT.

[Laurent Perron]

using this command line works on the main branch

--input ~/tmp/p10_fix2_red_presolved_sat.pb.txt.gz --params num_workers:3,min_num_lns_workers:0,subsolvers:\"max_lp\",subsolvers:\"core\",subsolvers:\"default_lp\",cp_model_presolve:false

I am using the CP-SAT presolved model. To get it, run the solve binary with --cp_model_dump_models and use /tmp/presolved_model.pb.txt. This proto is readable by the examples/cpp/sat_runner.cc program.

Laurent Perron | Operations Research | lpe...@google.com | (33) 1 42 68 53 00

To view this discussion on the web visit https://groups.google.com/d/msgid/or-tools-discuss/8b4bd6dd-1805-4f5d-b7b8-3a9d9c0b36f4n%40googlegroups.com.

[Stuart Rogers]

Is there a way for CP-SAT to save the presolved model and exit before trying to solve it. I call CP-SAT like this:

~/or-tools_main_2_7_2023/or-tools/bazel-bin/examples/cpp/solve --solver=sat --input=input.mps --cp_model_dump_models ./tmp/presolved_model.pb.txt --params="cp_model_presolve:true"

Does CP-SAT presolve benefit from multiple threads or is it strictly single-threaded?

"--input ~/tmp/p10_fix2_red_presolved_sat.pb.txt.gz"

I had thought OR-Tools was unable to read .gz and .bz2 files. https://github.com/google/or-tools/issues/3421#issuecomment-1253008571

[Laurent Perron]

just add --cp_model_dump_models on the command line. It will solve multiple problems in /tmp.

No need for the extra presolved_model arguments.

Currently, presolve is parallel. Not sure we can do a better job in parallel with the current architecture.

Laurent Perron | Operations Research | lpe...@google.com | (33) 1 42 68 53 00

To view this discussion on the web visit https://groups.google.com/d/msgid/or-tools-discuss/72a0990e-29d9-4e4e-8f8f-e188ec412595n%40googlegroups.com.

[Stuart Rogers]

"--input ~/tmp/p10_fix2_red_presolved_sat.pb.txt.gz"

I had thought OR-Tools was unable to read .gz and .bz2 files. https://github.com/google/or-tools/issues/3421#issuecomment-1253008571

I am unable to build sat_runner.

$ bazel run -c opt --cxxopt=-std=c++17 examples/cpp:sat_runner
Starting local Bazel server and connecting to it...
INFO: Analyzed target //examples/cpp:sat_runner (76 packages loaded, 1935 targets configured).
INFO: Found 1 target...
INFO: From Compiling examples/cpp/sat_runner.cc:
In file included from examples/cpp/sat_runner.cc:29:
./examples/cpp/opb_reader.h: In static member function 'static std::string operations_research::sat::OpbReader::ExtractProblemName(const string&)':
./examples/cpp/opb_reader.h:64:15: warning: comparison of integer expressions of different signedness: 'const int' and 'const size_type' {aka 'const long unsigned int'} [-Wsign-compare]
   64 |         found != std::string::npos ? filename.substr(found + 1) : filename;
      |         ~~~~~~^~~~~~~~~~~~~~~~~~~~
./examples/cpp/opb_reader.h: In member function 'void operations_research::sat::OpbReader::ProcessNewLine(operations_research::sat::LinearBooleanProblem*, const string&)':
./examples/cpp/opb_reader.h:77:25: warning: comparison of integer expressions of different signedness: 'int' and 'std::vector<std::__cxx11::basic_string<char> >::size_type' {aka 'long unsigned int'} [-Wsign-compare]
   77 |       for (int i = 1; i < words.size(); ++i) {
      |                       ~~^~~~~~~~~~~~~~
./examples/cpp/opb_reader.h:98:23: warning: comparison of integer expressions of different signedness: 'int' and 'std::vector<std::__cxx11::basic_string<char> >::size_type' {aka 'long unsigned int'} [-Wsign-compare]
   98 |     for (int i = 0; i < words.size(); ++i) {
      |                     ~~^~~~~~~~~~~~~~
In file included from examples/cpp/sat_runner.cc:30:
./examples/cpp/sat_cnf_reader.h: In static member function 'static std::string operations_research::sat::SatCnfReader::ExtractProblemName(const string&)':
./examples/cpp/sat_cnf_reader.h:193:15: warning: comparison of integer expressions of different signedness: 'const int' and 'const size_type' {aka 'const long unsigned int'} [-Wsign-compare]
  193 |         found != std::string::npos ? filename.substr(found + 1) : filename;
      |         ~~~~~~^~~~~~~~~~~~~~~~~~~~
In file included from ./ortools/sat/pb_constraint.h:33,
                 from ./ortools/sat/boolean_problem.h:26,
                 from examples/cpp/sat_runner.cc:41:
./ortools/sat/sat_base.h: In member function 'std::vector<operations_research::sat::Literal>* operations_research::sat::Trail::GetEmptyVectorToStoreReason(int) const':
./ortools/sat/sat_base.h:331:21: warning: comparison of integer expressions of different signedness: 'int' and 'std::deque<std::vector<operations_research::sat::Literal> >::size_type' {aka 'long unsigned int'} [-Wsign-compare]
  331 |     if (trail_index >= reasons_repository_.size()) {
      |         ~~~~~~~~~~~~^~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In file included from ./ortools/sat/sat_solver.h:39,
                 from ./ortools/sat/boolean_problem.h:28,
                 from examples/cpp/sat_runner.cc:41:
./ortools/sat/clause.h: In member function 'operations_research::sat::SatClause* operations_research::sat::LiteralWatchers::NextClauseToMinimize()':
./ortools/sat/clause.h:250:31: warning: comparison of integer expressions of different signedness: 'int' and 'std::vector<operations_research::sat::SatClause*>::size_type' {aka 'long unsigned int'} [-Wsign-compare]
  250 |     for (; to_minimize_index_ < clauses_.size(); ++to_minimize_index_) {
      |            ~~~~~~~~~~~~~~~~~~~^~~~~~~~~~~~~~~~~
In file included from ./ortools/sat/boolean_problem.h:28,
                 from examples/cpp/sat_runner.cc:41:
./ortools/sat/sat_solver.h: In lambda function:
./ortools/sat/sat_solver.h:909:23: warning: comparison of integer expressions of different signedness: 'int' and 'std::vector<operations_research::sat::Literal>::size_type' {aka 'long unsigned int'} [-Wsign-compare]
  909 |     for (int i = 0; i < literals.size(); ++i) {
      |                     ~~^~~~~~~~~~~~~~~~~
In file included from ./ortools/sat/boolean_problem.h:29,
                 from examples/cpp/sat_runner.cc:41:
./ortools/sat/simplification.h: In member function 'std::vector<operations_research::sat::Literal> operations_research::sat::SatPostsolver::Clause(int) const':
./ortools/sat/simplification.h:92:27: warning: comparison of integer expressions of different signedness: 'int' and 'std::vector<int>::size_type' {aka 'long unsigned int'} [-Wsign-compare]
   92 |     const int end = i + 1 < clauses_start_.size() ? clauses_start_[i + 1]
      |                     ~~~~~~^~~~~~~~~~~~~~~~~~~~~~~
./ortools/sat/simplification.h:96:23: warning: comparison of integer expressions of different signedness: 'int' and 'std::vector<operations_research::sat::Literal>::size_type' {aka 'long unsigned int'} [-Wsign-compare]
   96 |     for (int j = 0; j < result.size(); ++j) {
      |                     ~~^~~~~~~~~~~~~~~
In file included from ./ortools/sat/cp_model_mapping.h:29,
                 from ./ortools/sat/optimization.h:22,
                 from examples/cpp/sat_runner.cc:47:
./ortools/sat/integer.h: In member function 'bool operations_research::sat::IntegerTrail::VariableLowerBoundIsFromLevelZero(operations_research::sat::IntegerVariable) const':
./ortools/sat/integer.h:973:43: warning: comparison of integer expressions of different signedness: 'const int' and 'absl::StrongVector<operations_research::StrongIndex<operations_research::sat::IntegerVariable_index_tag_>, operations_research::sat::IntegerTrail::VarInfo>::size_type' {aka 'long unsigned int'} [-Wsign-compare]
  973 |     return vars_[var].current_trail_index < vars_.size();
./ortools/sat/integer.h: In member function 'void operations_research::sat::GenericLiteralWatcher::WatchLowerBound(operations_research::sat::IntegerVariable, int, int)':
./ortools/sat/integer.h:1616:19: warning: comparison of integer expressions of different signedness: 'int' and 'absl::StrongVector<operations_research::StrongIndex<operations_research::sat::IntegerVariable_index_tag_>, std::vector<operations_research::sat::GenericLiteralWatcher::WatchData> >::size_type' {aka 'long unsigned int'} [-Wsign-compare]
 1616 |   if (var.value() >= var_to_watcher_.size()) {
      |       ~~~~~~~~~~~~^~~~~~~~~~~~~~~~~~~~~~~~~
In file included from ./ortools/sat/intervals.h:29,
                 from ./ortools/sat/cp_model_mapping.h:30,
                 from ./ortools/sat/optimization.h:22,
                 from examples/cpp/sat_runner.cc:47:
./ortools/sat/cp_constraints.h: In function 'std::vector<operations_research::StrongInt64<operations_research::sat::IntegerValue_integer_tag_>, std::allocator<operations_research::StrongInt64<operations_research::sat::IntegerValue_integer_tag_> > > operations_research::sat::ToIntegerValueVector(const std::vector<long int>&)':
./ortools/sat/cp_constraints.h:106:21: warning: comparison of integer expressions of different signedness: 'int' and 'std::vector<long int>::size_type' {aka 'long unsigned int'} [-Wsign-compare]
  106 |   for (int i = 0; i < input.size(); ++i) {
      |                   ~~^~~~~~~~~~~~~~
In file included from ./ortools/sat/integer_expr.h:31,
                 from ./ortools/sat/intervals.h:31,
                 from ./ortools/sat/cp_model_mapping.h:30,
                 from ./ortools/sat/optimization.h:22,
                 from examples/cpp/sat_runner.cc:47:
./ortools/sat/linear_constraint.h: In member function 'std::string operations_research::sat::LinearConstraint::DebugString() const':
./ortools/sat/linear_constraint.h:70:23: warning: comparison of integer expressions of different signedness: 'int' and 'std::vector<operations_research::StrongIndex<operations_research::sat::IntegerVariable_index_tag_> >::size_type' {aka 'long unsigned int'} [-Wsign-compare]
   70 |     for (int i = 0; i < vars.size(); ++i) {
      |                     ~~^~~~~~~~~~~~~
In file included from ./ortools/sat/intervals.h:31,
                 from ./ortools/sat/cp_model_mapping.h:30,
                 from ./ortools/sat/optimization.h:22,
                 from examples/cpp/sat_runner.cc:47:
./ortools/sat/integer_expr.h: In lambda function:
./ortools/sat/integer_expr.h:766:23: warning: comparison of integer expressions of different signedness: 'int' and 'std::vector<operations_research::StrongIndex<operations_research::sat::IntegerVariable_index_tag_> >::size_type' {aka 'long unsigned int'} [-Wsign-compare]
  766 |     for (int i = 0; i < new_vars.size(); ++i) {
      |                     ~~^~~~~~~~~~~~~~~~~
In file included from ./ortools/sat/optimization.h:22,
                 from examples/cpp/sat_runner.cc:47:
./ortools/sat/cp_model_mapping.h: In member function 'int operations_research::sat::CpModelMapping::GetProtoVariableFromBooleanVariable(operations_research::sat::BooleanVariable) const':
./ortools/sat/cp_model_mapping.h:158:21: warning: comparison of integer expressions of different signedness: 'int' and 'absl::StrongVector<operations_research::StrongIndex<operations_research::sat::BooleanVariable_index_tag_>, int>::size_type' {aka 'long unsigned int'} [-Wsign-compare]
  158 |     if (var.value() >= reverse_boolean_map_.size()) return -1;
      |         ~~~~~~~~~~~~^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
./ortools/sat/cp_model_mapping.h: In member function 'int operations_research::sat::CpModelMapping::GetProtoVariableFromIntegerVariable(operations_research::sat::IntegerVariable) const':
./ortools/sat/cp_model_mapping.h:162:21: warning: comparison of integer expressions of different signedness: 'int' and 'absl::StrongVector<operations_research::StrongIndex<operations_research::sat::IntegerVariable_index_tag_>, int>::size_type' {aka 'long unsigned int'} [-Wsign-compare]
  162 |     if (var.value() >= reverse_integer_map_.size()) return -1;
      |         ~~~~~~~~~~~~^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In file included from ./ortools/glop/basis_representation.h:23,
                 from ./ortools/glop/revised_simplex.h:101,
                 from ./ortools/sat/linear_programming_constraint.h:27,
                 from ./ortools/sat/integer_search.h:37,
                 from ./ortools/sat/optimization.h:24,
                 from examples/cpp/sat_runner.cc:47:
./ortools/glop/rank_one_update.h: In member function 'void operations_research::glop::RankOneUpdateFactorization::RightSolve(operations_research::glop::DenseColumn*) const':
./ortools/glop/rank_one_update.h:195:23: warning: comparison of integer expressions of different signedness: 'int' and 'const size_t' {aka 'const long unsigned int'} [-Wsign-compare]
  195 |     for (int i = 0; i < end; ++i) {
      |                     ~~^~~~~
./ortools/glop/rank_one_update.h: In member function 'void operations_research::glop::RankOneUpdateFactorization::RightSolveWithNonZeros(operations_research::glop::ScatteredColumn*) const':
./ortools/glop/rank_one_update.h:215:23: warning: comparison of integer expressions of different signedness: 'int' and 'const size_t' {aka 'const long unsigned int'} [-Wsign-compare]
  215 |     for (int i = 0; i < end; ++i) {
      |                     ~~^~~~~
examples/cpp/sat_runner.cc: In function 'int operations_research::sat::{anonymous}::Run()':
examples/cpp/sat_runner.cc:313:23: warning: comparison of integer expressions of different signedness: 'int' and 'std::vector<std::unique_ptr<operations_research::SparsePermutation> >::size_type' {aka 'long unsigned int'} [-Wsign-compare]
  313 |     for (int i = 0; i < generators.size(); ++i) {
      |                     ~~^~~~~~~~~~~~~~~~~~~
In file included from external/com_google_absl/absl/flags/flag.h:37,
                 from examples/cpp/sat_runner.cc:21:
external/com_google_absl/absl/log/internal/check_op.h: In instantiation of 'constexpr std::string* absl::lts_20230125::log_internal::Check_LTImpl(const T1&, const T2&, const char*) [with T1 = int; T2 = long unsigned int; std::string = std::__cxx11::basic_string<char>]':
./examples/cpp/opb_reader.h:102:9:   required from here
external/com_google_absl/absl/log/internal/check_op.h:339:43: warning: comparison of integer expressions of different signedness: 'const int' and 'const long unsigned int' [-Wsign-compare]
  339 | ABSL_LOG_INTERNAL_CHECK_OP_IMPL(Check_LT, <)
external/com_google_absl/absl/base/optimization.h:178:58: note: in definition of macro 'ABSL_PREDICT_TRUE'
  178 | #define ABSL_PREDICT_TRUE(x) (__builtin_expect(false || (x), true))
      |                                                          ^
external/com_google_absl/absl/log/internal/check_op.h:339:1: note: in expansion of macro 'ABSL_LOG_INTERNAL_CHECK_OP_IMPL'
  339 | ABSL_LOG_INTERNAL_CHECK_OP_IMPL(Check_LT, <)
      | ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
external/com_google_absl/absl/log/internal/check_op.h: In instantiation of 'constexpr std::string* absl::lts_20230125::log_internal::Check_LTImpl(const T1&, const T2&, const char*) [with T1 = long unsigned int; T2 = int; std::string = std::__cxx11::basic_string<char>]':
./ortools/sat/sat_base.h:576:3:   required from here
external/com_google_absl/absl/log/internal/check_op.h:339:43: warning: comparison of integer expressions of different signedness: 'const long unsigned int' and 'const int' [-Wsign-compare]
  339 | ABSL_LOG_INTERNAL_CHECK_OP_IMPL(Check_LT, <)
external/com_google_absl/absl/base/optimization.h:178:58: note: in definition of macro 'ABSL_PREDICT_TRUE'
  178 | #define ABSL_PREDICT_TRUE(x) (__builtin_expect(false || (x), true))
      |                                                          ^
external/com_google_absl/absl/log/internal/check_op.h:339:1: note: in expansion of macro 'ABSL_LOG_INTERNAL_CHECK_OP_IMPL'
  339 | ABSL_LOG_INTERNAL_CHECK_OP_IMPL(Check_LT, <)
      | ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In file included from ./ortools/util/time_limit.h:33,
                 from ./ortools/sat/util.h:38,
                 from ./ortools/sat/clause.h:41,
                 from ./ortools/sat/sat_solver.h:39,
                 from ./ortools/sat/boolean_problem.h:28,
                 from examples/cpp/sat_runner.cc:41:
./ortools/util/running_stat.h: In instantiation of 'void operations_research::RunningMax<Number>::Add(Number) [with Number = long int]':
./ortools/util/time_limit.h:569:70:   required from here
./ortools/util/running_stat.h:148:43: warning: comparison of integer expressions of different signedness: 'size_t' {aka 'long unsigned int'} and 'const int' [-Wsign-compare]
  148 |   if (static_cast<size_t>(values_.size()) < window_size_) {
      |       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~^~~~~~~~~~~~~~
In file included from ./ortools/sat/intervals.h:31,
                 from ./ortools/sat/cp_model_mapping.h:30,
                 from ./ortools/sat/optimization.h:22,
                 from examples/cpp/sat_runner.cc:47:
./ortools/sat/integer_expr.h: In instantiation of 'std::function<void(operations_research::sat::Model*)> operations_research::sat::ConditionalWeightedSumLowerOrEqual(const std::vector<operations_research::sat::Literal>&, const std::vector<operations_research::StrongIndex<operations_research::sat::IntegerVariable_index_tag_> >&, const VectorInt&, int64_t) [with VectorInt = std::vector<long int>; int64_t = long int]':
./ortools/sat/integer_expr.h:697:71:   required from here
./ortools/sat/integer_expr.h:568:23: warning: comparison of integer expressions of different signedness: 'int' and 'std::vector<operations_research::StrongIndex<operations_research::sat::IntegerVariable_index_tag_> >::size_type' {aka 'long unsigned int'} [-Wsign-compare]
  568 |     for (int i = 0; i < vars.size(); ++i) {
      |                     ~~^~~~~~~~~~~~~
./ortools/sat/integer_expr.h:579:25: warning: comparison of integer expressions of different signedness: 'int' and 'std::vector<operations_research::StrongIndex<operations_research::sat::IntegerVariable_index_tag_> >::size_type' {aka 'long unsigned int'} [-Wsign-compare]
  579 |       for (int i = 0; i < vars.size(); ++i) {
      |                       ~~^~~~~~~~~~~~~
In file included from examples/cpp/sat_runner.cc:30:
./examples/cpp/sat_cnf_reader.h: In instantiation of 'void operations_research::sat::SatCnfReader::ProcessNewLine(const string&, Problem*) [with Problem = operations_research::sat::LinearBooleanProblemWrapper; std::string = std::__cxx11::basic_string<char>]':
./examples/cpp/sat_cnf_reader.h:161:7:   required from 'bool operations_research::sat::SatCnfReader::LoadInternal(const string&, Problem*) [with Problem = operations_research::sat::LinearBooleanProblemWrapper; std::string = std::__cxx11::basic_string<char>]'
./examples/cpp/sat_cnf_reader.h:136:43:   required from here
./examples/cpp/sat_cnf_reader.h:303:33: warning: comparison of integer expressions of different signedness: 'int' and 'std::vector<int>::size_type' {aka 'long unsigned int'} [-Wsign-compare]
  303 |           for (int i = 0; i + 1 < tmp_clause_.size(); ++i) {
      |                           ~~~~~~^~~~~~~~~~~~~~~~~~~~
./examples/cpp/sat_cnf_reader.h: In instantiation of 'void operations_research::sat::SatCnfReader::ProcessNewLine(const string&, Problem*) [with Problem = operations_research::sat::CpModelProtoWrapper; std::string = std::__cxx11::basic_string<char>]':
./examples/cpp/sat_cnf_reader.h:161:7:   required from 'bool operations_research::sat::SatCnfReader::LoadInternal(const string&, Problem*) [with Problem = operations_research::sat::CpModelProtoWrapper; std::string = std::__cxx11::basic_string<char>]'
./examples/cpp/sat_cnf_reader.h:142:43:   required from here
./examples/cpp/sat_cnf_reader.h:303:33: warning: comparison of integer expressions of different signedness: 'int' and 'std::vector<int>::size_type' {aka 'long unsigned int'} [-Wsign-compare]
In file included from external/com_google_absl/absl/flags/flag.h:37,
                 from examples/cpp/sat_runner.cc:21:
external/com_google_absl/absl/log/internal/check_op.h: In instantiation of 'constexpr std::string* absl::lts_20230125::log_internal::Check_GEImpl(const T1&, const T2&, const char*) [with T1 = long unsigned int; T2 = int; std::string = std::__cxx11::basic_string<char>]':
./ortools/sat/integer_expr.h:373:3:   required from 'std::function<void(operations_research::sat::Model*)> operations_research::sat::WeightedSumLowerOrEqual(const std::vector<operations_research::StrongIndex<operations_research::sat::IntegerVariable_index_tag_> >&, const VectorInt&, int64_t) [with VectorInt = std::vector<long int>; int64_t = long int]'
./ortools/sat/integer_expr.h:670:75:   required from here
external/com_google_absl/absl/log/internal/check_op.h:340:43: warning: comparison of integer expressions of different signedness: 'const long unsigned int' and 'const int' [-Wsign-compare]
  340 | ABSL_LOG_INTERNAL_CHECK_OP_IMPL(Check_GE, >=)
external/com_google_absl/absl/base/optimization.h:178:58: note: in definition of macro 'ABSL_PREDICT_TRUE'
  178 | #define ABSL_PREDICT_TRUE(x) (__builtin_expect(false || (x), true))
      |                                                          ^
external/com_google_absl/absl/log/internal/check_op.h:340:1: note: in expansion of macro 'ABSL_LOG_INTERNAL_CHECK_OP_IMPL'
  340 | ABSL_LOG_INTERNAL_CHECK_OP_IMPL(Check_GE, >=)
      | ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Target //examples/cpp:sat_runner up-to-date:
  bazel-bin/examples/cpp/sat_runner
INFO: Elapsed time: 9.256s, Critical Path: 6.35s
INFO: 6 processes: 4 internal, 2 linux-sandbox.
INFO: Build completed successfully, 6 total actions
INFO: Build completed successfully, 6 total actions
F0209 11:10:01.780756  257379 sat_runner.cc:200] Please supply a data file with --input=
*** Check failure stack trace: ***
    @     0x559218b763f2  absl::lts_20230125::log_internal::LogMessage::Flush()
    @     0x559218b7651d  absl::lts_20230125::log_internal::LogMessageFatal::~LogMessageFatal()
    @     0x55921873bb7a  operations_research::sat::(anonymous namespace)::Run()
    @     0x559218780a90  main
    @     0x7f0a2a1a3083  __libc_start_main
Aborted (core dumped)

[Laurent Perron]

On linux, I use 

bazel run -c opt --cxxopt=-std=c++17 --cxxopt=-Wno-sign-compare

Laurent Perron | Operations Research | lpe...@google.com | (33) 1 42 68 53 00

To view this discussion on the web visit https://groups.google.com/d/msgid/or-tools-discuss/a7304998-5220-49d5-9129-f980e37c8c87n%40googlegroups.com.

[Stuart Rogers]

The solve binary with --cp_model_dump_models generates several .pb.txt files in /tmp. Did you use presolved_model.pb.txt?

-rw-rw-r--  1 stuart  stuart  3.3G Feb  9 11:35 model.pb.txt
-rw-rw-r--  1 stuart  stuart  1.3G Feb  9 11:44 presolved_model.pb.txt
-rw-rw-r--  1 stuart  stuart  2.9G Feb  9 11:45 presolved.mp_model.pb.txt

During presolve, based on htop, it looks like only 1 or maybe 2 threads are used even though I specify --num_threads=24.

You received this message because you are subscribed to a topic in the Google Groups "or-tools-discuss" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/or-tools-discuss/4fcAuWiIUFA/unsubscribe.
To unsubscribe from this group and all its topics, send an email to or-tools-discu...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/or-tools-discuss/CABcmEebgFa22Ftc2-HuP9mPwGRwgbYO3%2BuowX-KvURvG8eWZbg%40mail.gmail.com.

[Laurent Perron]

Yes

To view this discussion on the web visit https://groups.google.com/d/msgid/or-tools-discuss/CAO6iSeAU1L1P4D%3DaNgWsnnM8BGpcYu9MxsNyi7Mc6LASB6aHXQ%40mail.gmail.com.

[Stuart Rogers]

How long did it take you to solve the CP-SAT presolved model with sat_runner?

#Bound 2082.41s best:34955948 next:[19607947,34955947] max_lp
#Bound 2101.72s best:34955948 next:[19612478,34955947] max_lp
#Bound 2134.65s best:34955948 next:[19621784,34955947] max_lp

Is there a document explaining the different CP-SAT subsolvers?

subsolvers:\"max_lp\",subsolvers:\"core\",subsolvers:\"default_lp\"

[Stuart Rogers]

sat_runner was killed.

$ ~/or-tools_main_2_7_2023/or-tools/bazel-bin/examples/cpp/sat_runner --input /tmp/presolved_model.pb.txt.gz --params num_workers:3,min_num_lns_workers:0,subsolvers:\"max_lp\",subsolvers:\"core\",subsolvers:\"default_lp\",cp_model_presolve:false

....

#Bound 2733.66s best:34955948 next:[19971599,34955947] max_lp
#Bound 2748.94s best:34955948 next:[19981999,34955947] max_lp
#Bound 2762.66s best:34955948 next:[20002799,34955947] max_lp
#Bound 2774.23s best:34955948 next:[20007190,34955947] max_lp
#Bound 2787.69s best:34955948 next:[20027336,34955947] max_lp
#Bound 2798.11s best:34955948 next:[20038894,34955947] max_lp
Killed

[Laurent Perron]

OOM.

To view this discussion on the web visit https://groups.google.com/d/msgid/or-tools-discuss/1612dcd5-e3b0-401a-ba91-5ead29267a87n%40googlegroups.com.

--

--Laurent

[Stuart Rogers]

In your example where the CP-SAT presolved model is fed into CP-SAT via the proto using sat_runner, does CP-SAT return the solution w.r.t. the CP-SAT presolved model or w.r.t. the orignal (before CP-SAT presolving) model?

[Laurent Perron]

It returns a solution to the presolved model. The code should be the same. The variables could be different.

I only used that to avoid the 100s of seconds of running the presolve.

Laurent Perron | Operations Research | lpe...@google.com | (33) 1 42 68 53 00

To view this discussion on the web visit https://groups.google.com/d/msgid/or-tools-discuss/837d8e05-f94e-4b27-b55f-690ad0e13f07n%40googlegroups.com.

[Stuart Rogers]

Eventually, I would want the solution to the original model. Is model.pb.txt the proto for the original model? I got a seg fault when I tried:

$ ~/or-tools_main_2_7_2023/or-tools/bazel-bin/examples/cpp/sat_runner --input /tmp/model.pb.txt.gz --params num_workers:3,min_num_lns_workers:0,subsolvers:\"max_lp\",subsolvers:\"core\",subsolvers:\"default_lp\",cp_model_presolve:true

Segmentation fault (core dumped)

You received this message because you are subscribed to a topic in the Google Groups "or-tools-discuss" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/or-tools-discuss/4fcAuWiIUFA/unsubscribe.
To unsubscribe from this group and all its topics, send an email to or-tools-discu...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/or-tools-discuss/CABcmEeaa3_YaVgS_K2%2BZTxzktnRwEpQvQu_HCVPhnBQLyr8uuQ%40mail.gmail.com.

[Laurent Perron]

it is bigger than 2GB. Protos have a limit of 2GB when serializing. 

I just did the code to enable writing the proto in binary format (which makes it less than 2GB), but it is not yet out in OR-Tools.

your problem is just too big :-)

Laurent Perron | Operations Research | lpe...@google.com | (33) 1 42 68 53 00

To view this discussion on the web visit https://groups.google.com/d/msgid/or-tools-discuss/CAO6iSeD-UyFVQUHTQbW2%2BiHccPj%3DZCgSn1qdF1oc3acht%2BetyA%40mail.gmail.com.

[Stuart Rogers]

Can you show the final results? How long did it take to find the optimal solution?

You received this message because you are subscribed to a topic in the Google Groups "or-tools-discuss" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/or-tools-discuss/4fcAuWiIUFA/unsubscribe.
To unsubscribe from this group and all its topics, send an email to or-tools-discu...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/or-tools-discuss/CABcmEebgFa22Ftc2-HuP9mPwGRwgbYO3%2BuowX-KvURvG8eWZbg%40mail.gmail.com.

[Laurent Perron]

It did not.

This is around the best I got:

#Bound 36470.51s best:33038197 next:[24974735,33038196] max_lp

Laurent Perron | Operations Research | lpe...@google.com | (33) 1 42 68 53 00

To view this discussion on the web visit https://groups.google.com/d/msgid/or-tools-discuss/CAO6iSeAiQ7KKc6LJqdX0sG24NR%3DMADtaBhz%3D%2BWMZ%2BKZHMaThhA%40mail.gmail.com.

[Stuart Rogers]

You had obtained a better feasible solution (32656437) before using 16 workers on the large AMD in just 20 minutes.

[Laurent Perron]

with 16 workers. This was done with 3 or 4 workers.

Laurent Perron | Operations Research | lpe...@google.com | (33) 1 42 68 53 00

To view this discussion on the web visit https://groups.google.com/d/msgid/or-tools-discuss/2cb71ab3-3cb0-4dd6-be76-b3545b992fe6n%40googlegroups.com.

[Laurent Perron]

I just pushed the code to save protos in binary format.

--cp_model_dump_text_proto=false

It should be readable from sat_runner.

Laurent Perron | Operations Research | lpe...@google.com | (33) 1 42 68 53 00

[Stuart Rogers]

Did you push the new code to the main branch? https://github.com/google/or-tools/commit/7277ccc140010f0ad5464496c397585333115eb4

[Laurent Perron]

yes.

Laurent Perron | Operations Research | lpe...@google.com | (33) 1 42 68 53 00

To view this discussion on the web visit https://groups.google.com/d/msgid/or-tools-discuss/9bec8aa7-218a-41ed-b405-bcf3622c7d23n%40googlegroups.com.

[Stuart Rogers]

Where are the binary protos written to?

$ ~/or-tools_main_2_9_2023/or-tools/bazel-bin/examples/cpp/solve --solver=sat --input=input.mps --cp_model_dump_models=false --params="cp_model_presolve:true" --num_threads=24

[Stuart Rogers]

Nevermined, the solve command below writes the binary protos to /tmp:

$ ~/or-tools_main_2_9_2023/or-tools/bazel-bin/examples/cpp/solve --solver=sat --input=input.mps --cp_model_dump_models --cp_model_dump_text_proto=false --params="cp_model_presolve:true" --num_threads=24

[Stuart Rogers]

sat_runner is able to process the binary protos now.

$ ~/or-tools_main_2_7_2023/or-tools/bazel-bin/examples/cpp/sat_runner --input /tmp/model.bin.gz --params num_workers:3,min_num_lns_workers:0,subsolvers:\"max_lp\",subsolvers:\"core\",subsolvers:\"default_lp\",cp_model_presolve:true

Starting CP-SAT solver v9.5.9999
Parameters: log_search_progress: true cp_model_presolve: true num_workers: 3 subsolvers: "max_lp" subsolvers: "core" subsolvers: "default_lp" min_num_lns_workers: 0

Initial optimization model '/data/stuart/gen_MPS_files/p10_fix2_MILP_binary_x.mps': (model_fingerprint: 0x43e5d1e353c6a5e7)
#Variables: 11983731 (#bools:11978461 in floating point objective)
  - 11983731 Booleans in [0,1]
#kLinear2: 11978468
#kLinear3: 23
#kLinearN: 14792 (#terms: 11983626)

Starting presolve at 2.77s
[Scaling] Floating point objective has 11978461 terms with magnitude in [2, 12732] average = 5309.28
[Scaling] Objective coefficient relative error: 0
[Scaling] Objective worst-case absolute error: 0
[Scaling] Objective scaling factor: 1

[ExtractEncodingFromLinear] #potential_supersets=14814 #potential_subsets=0 #at_most_one_encodings=0 #exactly_one_encodings=0 #unique_terms=0 #multiple_terms=0 #literals=0 time=0.143832s

[Symmetry] Problem too large. Skipping. You can use symmetry_level:3 or more to force it.
[SAT presolve] num removable Booleans: 0 / 11983731
[SAT presolve] num trivial clauses: 0
[SAT presolve] [0s] clauses:11978468 literals:23956936 vars:11983731 one_side_vars:11983731 simple_definition:0 singleton_clauses:0

[SAT presolve] [1.13709s] clauses:11978468 literals:23956936 vars:11983731 one_side_vars:11983731 simple_definition:0 singleton_clauses:0
[SAT presolve] [1.37354s] clauses:11978468 literals:23956936 vars:11983731 one_side_vars:11983731 simple_definition:0 singleton_clauses:0
[Probing] deterministic_time: 1.00039 (limit: 1) wall_time: 3.72454 (Aborted 5109/11983731)

[Probing] implications and bool_or (work_done=20454).

[DetectDuplicateConstraints] #duplicates=0 #without_enforcements=0 time=12.6355s
[DetectDominatedLinearConstraints] #relevant_constraints=1 #work_done=0 #num_inclusions=0 #num_redundant=0 time=0.18585s
[ProcessSetPPC] #relevant_constraints=11993283 #num_inclusions=0 work=100001336 time=9.24954s
[FindBigLinearOverlap] #blocks=0 #saved_nz=0 #linears=1 #work_done=5281/1e+09 time=0.169773s
[MergeClauses] #num_collisions=0 #num_merges=0 #num_saved_literals=0 work=0/100000000 time=0.493487s

[Symmetry] Problem too large. Skipping. You can use symmetry_level:3 or more to force it.
[SAT presolve] num removable Booleans: 0 / 11983731
[SAT presolve] num trivial clauses: 0
[SAT presolve] [0s] clauses:11978468 literals:23956936 vars:11983731 one_side_vars:11983731 simple_definition:0 singleton_clauses:0

[SAT presolve] [2.08458s] clauses:11978468 literals:23956936 vars:11983731 one_side_vars:11983731 simple_definition:0 singleton_clauses:0
[SAT presolve] [2.35118s] clauses:11978468 literals:23956936 vars:11983731 one_side_vars:11983731 simple_definition:0 singleton_clauses:0
[Probing] deterministic_time: 1.00039 (limit: 1) wall_time: 4.03032 (Aborted 5109/11983731)

[Probing] implications and bool_or (work_done=20454).

[Stuart Rogers]

OR-Tools can read .gz but not .bz2 compressed files.

$ ~/or-tools_main_2_7_2023/or-tools/bazel-bin/examples/cpp/sat_runner --input /tmp/model.bin.bz2 --params num_workers:3,min_num_lns_workers:0,subsolvers:\"max_lp\",subsolvers:\"core\",subsolvers:\"default_lp\",cp_model_presolve:true
[libprotobuf ERROR external/com_google_protobuf/src/google/protobuf/text_format.cc:337] Error parsing text-format operations_research.sat.CpModelProto: 1:8: Message type "operations_research.sat.CpModelProto" has no field named "BZh91AY".
F0209 18:23:37.729901  278480 file_util.h:45] Check failed: ReadFileToProto(filename, &proto) with file: '/tmp/model.bin.bz2'

*** Check failure stack trace: ***

    @     0x55d4dd5b43f2  absl::lts_20230125::log_internal::LogMessage::Flush()
    @     0x55d4dd5b451d  absl::lts_20230125::log_internal::LogMessageFatal::~LogMessageFatal()
    @     0x55d4dd179600  operations_research::sat::(anonymous namespace)::Run()
    @     0x55d4dd1bea90  main
    @     0x7f9c846cc083  __libc_start_main
Aborted (core dumped)

[Laurent Perron]

indeed.

Laurent Perron | Operations Research | lpe...@google.com | (33) 1 42 68 53 00

To view this discussion on the web visit https://groups.google.com/d/msgid/or-tools-discuss/5bbdb9a8-c019-45a4-81b1-425701999466n%40googlegroups.com.

[Stuart Rogers]

Did this run of 16 workers on the large AMD run out of memory?

On Monday, February 6, 2023 at 1:06:22 PM UTC-8 Laurent Perron wrote:

On a machine with more memory (512GB) and with 16 workers

Starting search at 496.10s with 16 workers.

10 full problem subsolvers: [default_lp, no_lp, max_lp, core, reduced_costs, pseudo_costs, quick_restart, quick_restart_no_lp, lb_tree_search, probing]

4 first solution subsolvers: [random_0, random_quick_restart_0, random_1, random_quick_restart_1]

7 incomplete subsolvers: [feasibility_pump, rins_lns_default, rens_lns_default, rnd_var_lns_default, rnd_cst_lns_default, graph_var_lns_default, graph_cst_lns_default]

3 helper subsolvers: [synchronization_agent, neighborhood_helper, update_gap_integral]

#Bound 541.12s best:inf   next:[-6.31759637e+10,75311048] am1_presolve num_literals:11978461 num_am1:70 increase:345674490 work_done:100345259

#1     557.03s best:73565894 next:[-6.31759637e+10,73565893] no_lp fixed_bools:0/11983731

#2     557.54s best:72906378 next:[-6.31759637e+10,72906377] quick_restart_no_lp fixed_bools:0/11983731

#3     623.44s best:70975446 next:[-6.31759637e+10,70975445] 

#Bound 625.98s best:70975446 next:[-6.3175951e+10,70975445] bool_core num_cores:1 [core:2 mw:12728 d:0] assumptions:11978454 depth:1 fixed_bools:0/11983802

#Bound 628.61s best:70975446 next:[-6.31759382e+10,70975445] bool_core num_cores:2 [core:2 mw:12728 d:1] assumptions:11978454 depth:1 fixed_bools:0/11983803

#Bound 641.06s best:70975446 next:[-3.99911323e+10,70975445] reduced_costs initial_propagation

#Bound 650.91s best:70975446 next:[-2.33436236e+10,70975445] max_lp initial_propagation

#Bound 666.05s best:70975446 next:[-5.29631876e+09,70975445] max_lp

#Bound 672.67s best:70975446 next:[-3.05983328e+09,70975445] max_lp

#Bound 679.65s best:70975446 next:[-1.02091464e+09,70975445] max_lp

#Bound 685.73s best:70975446 next:[-296630484,70975445] max_lp

#Bound 695.86s best:70975446 next:[-7477247,70975445] max_lp

#Bound 700.25s best:70975446 next:[15009812,70975445] max_lp

#Bound 710.53s best:70975446 next:[15250160,70975445] max_lp

#Bound 714.21s best:70975446 next:[15319564,70975445] max_lp

#Bound 721.93s best:70975446 next:[15401709,70975445] max_lp

#4     723.28s best:69939758 next:[15401709,69939757] core fixed_bools:0/11983818

#Bound 725.07s best:69939758 next:[15428410,69939757] max_lp

#Bound 727.61s best:69939758 next:[15443962,69939757] max_lp

#Bound 732.85s best:69939758 next:[15507446,69939757] max_lp

#Bound 736.41s best:69939758 next:[15594859,69939757] max_lp

#Bound 744.41s best:69939758 next:[15717649,69939757] max_lp

#Bound 747.75s best:69939758 next:[15756700,69939757] max_lp

#Bound 754.43s best:69939758 next:[15781371,69939757] max_lp

#Bound 759.11s best:69939758 next:[15799121,69939757] max_lp

#Bound 766.10s best:69939758 next:[15919042,69939757] max_lp

#Bound 770.06s best:69939758 next:[15980355,69939757] max_lp

#5     770.29s best:45079459 next:[15980355,45079458] default_lp fixed_bools:0/11983731

#Bound 777.44s best:45079459 next:[16030051,45079458] max_lp

#Bound 781.22s best:45079459 next:[16051079,45079458] max_lp

#Bound 784.31s best:45079459 next:[16746088,45079458] lb_tree_search initial_propagation

#6     833.35s best:44443131 next:[16746088,44443130] default_lp fixed_bools:0/11983731

#7     874.45s best:44442811 next:[16746088,44442810] 

#8     917.32s best:44432459 next:[16746088,44432458] 

#9     992.53s best:44423563 next:[16746088,44423562] 

#Bound 999.93s best:44423563 next:[17711971,44423562] lb_tree_search

#10    1064.91s best:36942451 next:[17711971,36942450] default_lp fixed_bools:0/11983731

#11    1098.72s best:36780976 next:[17711971,36780975] default_lp fixed_bools:0/11983731

#12    1127.17s best:33074613 next:[17711971,33074612] default_lp fixed_bools:0/11983731

#13    1198.14s best:32656437 next:[17711971,32656436] rnd_cst_lns_default(d=0.13 s=66 t=0.1

Which would indicate the problem is fixed on the main branch.

[Laurent Perron]

Yes, eventually.

Laurent Perron | Operations Research | lpe...@google.com | (33) 1 42 68 53 00

To view this discussion on the web visit https://groups.google.com/d/msgid/or-tools-discuss/55be7a41-f8f5-4f2d-8679-fc298fe20a85n%40googlegroups.com.

[Stuart Rogers]

Did you record the best solution found and the time?

[Laurent Perron]

I only once beat the 33M mark.

Lower bound was a bit more that 25M

Laurent Perron | Operations Research | lpe...@google.com | (33) 1 42 68 53 00

To view this discussion on the web visit https://groups.google.com/d/msgid/or-tools-discuss/a7ebf9ff-a4b0-476a-94b0-6b27597ee3f4n%40googlegroups.com.

[Laurent Perron]

With 20 workers, this is the last output before it was killed

#Bound 1682.06s best:29599718 next:[19480557,29599717]

Laurent Perron | Operations Research | lpe...@google.com | (33) 1 42 68 53 00

[Laurent Perron]

Ok, back at it.

We pushed some memory optimization.

Now, I can run 5 workers for some time. Memory is still creeping up slowly.

Here are the parameters:

num_workers:5,min_num_lns_workers:1,subsolvers:\"max_lp\",subsolvers:\"core\",subsolvers:\"

default_lp\",subsolvers:\"objective_lb_search\",cp_model_presolve:false

With these parameters, I get this

#Bound 18628.74s best:31320327 next:[23962004,31320326] max_lp

#Bound 18695.13s best:31320327 next:[23965265,31320326] max_lp

#Bound 18742.67s best:31320327 next:[23967694,31320326] max_lp

#Bound 18827.29s best:31320327 next:[23972185,31320326] max_lp

#Bound 18883.30s best:31320327 next:[23976257,31320326] max_lp

Still not close to the optimal, but getting there.

Laurent Perron | Operations Research | lpe...@google.com | (33) 1 42 68 53 00

[Laurent Perron]

I just pushed the fix for the search stopping early.

Thank you so much for the bug report.

Now we can continue working on the performance/memory of the solver.

--Laurent

Laurent Perron | Operations Research | lpe...@google.com | (33) 1 42 68 53 00

[Stuart Rogers]

solve.cc and sat_runner.cc seem to be missing from examples/cpp in the current main branch.

$ git clone -b main https://github.com/google/or-tools
Cloning into 'or-tools'...
remote: Enumerating objects: 369429, done.
remote: Counting objects: 100% (1844/1844), done.
remote: Compressing objects: 100% (818/818), done.
remote: Total 369429 (delta 1131), reused 1698 (delta 1020), pack-reused 367585
Receiving objects: 100% (369429/369429), 1.21 GiB | 10.19 MiB/s, done.
Resolving deltas: 100% (282409/282409), done.

$ cd or-tools/

$ bazel run -c opt --cxxopt=-std=c++17 examples/cpp:solve
Starting local Bazel server and connecting to it...
DEBUG: Rule 'bazel_skylib' indicated that a canonical reproducible form can be obtained by modifying arguments commit = "141432789c92e9db2402ef0be58e2a2d2c4dd1fd", shallow_since = "1675958592 -0500" and dropping ["tag"]
DEBUG: Repository bazel_skylib instantiated at:
  /home/stuart/or-tools_main_2_17_2023/or-tools/WORKSPACE:20:15: in <toplevel>
Repository rule git_repository defined at:
  /home/stuart/.cache/bazel/_bazel_stuart/cd565eb284281b9ca0a53dec3e3bb874/external/bazel_tools/tools/build_defs/repo/git.bzl:199:33: in <toplevel>
DEBUG: Rule 'com_google_protobuf' indicated that a canonical reproducible form can be obtained by modifying arguments commit = "f0dc78d7e6e331b8c6bb2d5283e06aa26883ca7c", shallow_since = "1670889792 -0800" and dropping ["tag"]
DEBUG: Repository com_google_protobuf instantiated at:
  /home/stuart/or-tools_main_2_17_2023/or-tools/WORKSPACE:43:15: in <toplevel>
Repository rule git_repository defined at:
  /home/stuart/.cache/bazel/_bazel_stuart/cd565eb284281b9ca0a53dec3e3bb874/external/bazel_tools/tools/build_defs/repo/git.bzl:199:33: in <toplevel>
DEBUG: Rule 'rules_python' indicated that a canonical reproducible form can be obtained by modifying arguments commit = "70cce26432187a60b4e950118791385e6fb3c26f", shallow_since = "1673388051 +1100" and dropping ["tag"]
DEBUG: Repository rules_python instantiated at:
  /home/stuart/or-tools_main_2_17_2023/or-tools/WORKSPACE:122:15: in <toplevel>
Repository rule git_repository defined at:
  /home/stuart/.cache/bazel/_bazel_stuart/cd565eb284281b9ca0a53dec3e3bb874/external/bazel_tools/tools/build_defs/repo/git.bzl:199:33: in <toplevel>
DEBUG: Rule 'pybind11_bazel' indicated that a canonical reproducible form can be obtained by modifying arguments shallow_since = "1667406693 -0700"
DEBUG: Repository pybind11_bazel instantiated at:
  /home/stuart/or-tools_main_2_17_2023/or-tools/WORKSPACE:150:15: in <toplevel>
Repository rule git_repository defined at:
  /home/stuart/.cache/bazel/_bazel_stuart/cd565eb284281b9ca0a53dec3e3bb874/external/bazel_tools/tools/build_defs/repo/git.bzl:199:33: in <toplevel>
DEBUG: Rule 'contrib_rules_jvm' indicated that a canonical reproducible form can be obtained by modifying arguments commit = "06311c6bade29e7d3957d4d34792208acd5ee563", shallow_since = "1666868678 +0100" and dropping ["tag"]
DEBUG: Repository contrib_rules_jvm instantiated at:
  /home/stuart/or-tools_main_2_17_2023/or-tools/WORKSPACE:229:15: in <toplevel>
Repository rule git_repository defined at:
  /home/stuart/.cache/bazel/_bazel_stuart/cd565eb284281b9ca0a53dec3e3bb874/external/bazel_tools/tools/build_defs/repo/git.bzl:199:33: in <toplevel>
ERROR: Skipping 'examples/cpp:solve': no such target '//examples/cpp:solve': target 'solve' not declared in package 'examples/cpp' defined by /home/stuart/or-tools_main_2_17_2023/or-tools/examples/cpp/BUILD.bazel
WARNING: Target pattern parsing failed.
ERROR: no such target '//examples/cpp:solve': target 'solve' not declared in package 'examples/cpp' defined by /home/stuart/or-tools_main_2_17_2023/or-tools/examples/cpp/BUILD.bazel
INFO: Elapsed time: 12.453s
INFO: 0 processes.
FAILED: Build did NOT complete successfully (1 packages loaded)
FAILED: Build did NOT complete successfully (1 packages loaded)

[Laurent Perron]

Moved to or-tools/sat and or-tools/linear_solver

To view this discussion on the web visit https://groups.google.com/d/msgid/or-tools-discuss/f8b9e5d5-e447-4e53-ad62-2cfa49c7ace8n%40googlegroups.com.

[Laurent Perron]

Sorry, ortools/sat and ortools/linear_solver

To view this discussion on the web visit https://groups.google.com/d/msgid/or-tools-discuss/CAPyyUTsbLrSNDJGgydCt%3D%2BDmbJ8TB2N6-Uh02grz17Nmhn0zLw%40mail.gmail.com.

[Stuart Rogers]

With your fix, CP-SAT seems to be working properly now with 4 threads.

$ ~/or-tools_main_2_17_2023/or-tools/bazel-bin/ortools/linear_solver/solve --solver=sat --linear_solver_enable_verbose_output --input="/data/stuart/PaPILO_files_MILP_binary_x/p10_fix2_red.mps" --sol_file="solution_4_threads.sol" --params="cp_model_presolve:true" --num_threads=4 | tee output_4_threads.txt
File        : '/data/stuart/PaPILO_files_MILP_binary_x/p10_fix2_red.mps'
Solver      : SAT_INTEGER_PROGRAMMING
Parameters  : cp_model_presolve:true

Dimension   : 11993312 x 11983760

Running basic LP presolve, initial problem dimensions: 11993312 rows, 11983760 columns, 35940689 entries with magnitude in [1.000000e+00, 1.000000e+00]
glop::FixedVariablePreprocessor                        11993312 rows, 11983760 columns, 35940689 entries with magnitude in [1.000000e+00, 1.000000e+00]
glop::SingletonPreprocessor                            11993283 rows, 11983731 columns, 35940631 entries with magnitude in [1.000000e+00, 1.000000e+00]
glop::ForcingAndImpliedFreeConstraintPreprocessor      11993283 rows, 11983731 columns, 35940631 entries with magnitude in [1.000000e+00, 1.000000e+00]
glop::FreeConstraintPreprocessor                       11993283 rows, 11983731 columns, 35940631 entries with magnitude in [1.000000e+00, 1.000000e+00]
glop::UnconstrainedVariablePreprocessor                11993283 rows, 11983731 columns, 35940631 entries with magnitude in [1.000000e+00, 1.000000e+00]

Scaling to pure integer problem.
Num integers: 11983731/11983731 (implied: 0 in_inequalities: 0 max_scaling: 0) [IP]
Maximum constraint coefficient relative error: 0
Maximum constraint worst-case activity error: 0
Maximum constraint scaling factor: 1

Starting CP-SAT solver v9.5.9999
Parameters: log_search_progress: true cp_model_presolve: true num_workers: 4

Initial optimization model '/data/stuart/gen_MPS_files/p10_fix2_MILP_binary_x.mps': (model_fingerprint: 0x43e5d1e353c6a5e7)

#Variables: 11983731 (#bools:11978461 in floating point objective)
  - 11983731 Booleans in [0,1]
#kLinear2: 11978468
#kLinear3: 23
#kLinearN: 14792 (#terms: 11983626)

Starting presolve at 3.66s

[Scaling] Floating point objective has 11978461 terms with magnitude in [2, 12732] average = 5309.28
[Scaling] Objective coefficient relative error: 0
[Scaling] Objective worst-case absolute error: 0
[Scaling] Objective scaling factor: 1

[ExtractEncodingFromLinear] #potential_supersets=14814 #potential_subsets=0 #at_most_one_encodings=0 #exactly_one_encodings=0 #unique_terms=0 #multiple_terms=0 #literals=0 time=0.203729s

[Symmetry] Problem too large. Skipping. You can use symmetry_level:3 or more to force it.

[SAT presolve] num removable Booleans: 0 / 11983731
[SAT presolve] num trivial clauses: 0
[SAT presolve] [0s] clauses:11978468 literals:23956936 vars:11983731 one_side_vars:11983731 simple_definition:0 singleton_clauses:0

[SAT presolve] [1.50242s] clauses:11978468 literals:23956936 vars:11983731 one_side_vars:11983731 simple_definition:0 singleton_clauses:0
[SAT presolve] [1.78885s] clauses:11978468 literals:23956936 vars:11983731 one_side_vars:11983731 simple_definition:0 singleton_clauses:0
[Probing] deterministic_time: 1.00039 (limit: 1) wall_time: 8.35194 (Aborted 5109/11983731)

[Probing] implications and bool_or (work_done=20454).

[DetectDuplicateConstraints] #duplicates=0 #without_enforcements=0 time=16.7122s
[DetectDominatedLinearConstraints] #relevant_constraints=1 #work_done=0 #num_inclusions=0 #num_redundant=0 time=0.262433s
[ProcessSetPPC] #relevant_constraints=11993283 #num_inclusions=0 work=100001336 time=12.3353s
[FindBigLinearOverlap] #blocks=0 #saved_nz=0 #linears=1 #work_done=5281/1e+09 time=0.249346s
[MergeClauses] #num_collisions=0 #num_merges=0 #num_saved_literals=0 work=0/100000000 time=0.949961s

[Symmetry] Problem too large. Skipping. You can use symmetry_level:3 or more to force it.

[SAT presolve] num removable Booleans: 0 / 11983731
[SAT presolve] num trivial clauses: 0
[SAT presolve] [0s] clauses:11978468 literals:23956936 vars:11983731 one_side_vars:11983731 simple_definition:0 singleton_clauses:0

[SAT presolve] [2.64669s] clauses:11978468 literals:23956936 vars:11983731 one_side_vars:11983731 simple_definition:0 singleton_clauses:0
[SAT presolve] [2.92504s] clauses:11978468 literals:23956936 vars:11983731 one_side_vars:11983731 simple_definition:0 singleton_clauses:0
[Probing] deterministic_time: 1.00039 (limit: 1) wall_time: 6.56327 (Aborted 5109/11983731)

[Probing] implications and bool_or (work_done=20454).

[DetectDuplicateConstraints] #duplicates=0 #without_enforcements=0 time=16.4544s
[DetectDominatedLinearConstraints] #relevant_constraints=1 #work_done=0 #num_inclusions=0 #num_redundant=0 time=0.391907s
[ProcessSetPPC] #relevant_constraints=11993283 #num_inclusions=0 work=100001336 time=16.065s
[FindBigLinearOverlap] #blocks=0 #saved_nz=0 #linears=1 #work_done=5281/1e+09 time=0.392021s
[MergeClauses] #num_collisions=0 #num_merges=0 #num_saved_literals=0 work=0/100000000 time=1.22138s
[ExpandObjective] #propagations=0 #entries=0 #tight_variables=0 #tight_constraints=0 #expands=0 #issues=0 time=4.12869s

Presolve summary:
  - 0 affine relations were detected.

  - rule 'TODO dual: only one blocking constraint?' was applied 31686 times.
  - rule 'TODO dual: only one unspecified blocking constraint?' was applied 71870700 times.

  - rule 'TODO linear2: contains a Boolean.' was applied 23956936 times.
  - rule 'bool_or: implications' was applied 11978468 times.
  - rule 'linear: negative clause' was applied 18 times.
  - rule 'linear: positive at most one' was applied 14814 times.
  - rule 'linear: positive clause' was applied 11978450 times.
  - rule 'linear: simplified rhs' was applied 11993282 times.

  - rule 'presolve: 0 unused variables removed.' was applied 1 time.
  - rule 'presolve: iteration' was applied 2 times.

Presolved optimization model '/data/stuart/gen_MPS_files/p10_fix2_MILP_binary_x.mps': (model_fingerprint: 0xf94700dd262667c6)
#Variables: 11983731 (#bools:11978461 in objective)

  - 11983731 Booleans in [0,1]
#kAtMostOne: 14814 (#literals: 11978414)

#kBoolAnd: 5299 (#enforced: 5299) (#literals: 11983767)

#kLinearN: 1 (#terms: 5281)

Preloading model.

#Bound 685.87s best:inf   next:[-6.35216382e+10,75311048] initial_domain

[Symmetry] Graph for symmetry has 35966008 nodes and 59908093 arcs.

[Symmetry] Graph too large. Skipping. You can use symmetry_level:3 or more to force it.
#Model 712.61s var:11983731/11983731 constraints:20114/20114

Starting search at 712.61s with 4 workers.
2 full problem subsolvers: [default_lp, no_lp]

1 first solution subsolver: [random_0]

7 incomplete subsolvers: [feasibility_pump, rins_lns_default, rens_lns_default, rnd_var_lns_default, rnd_cst_lns_default, graph_var_lns_default, graph_cst_lns_default]
3 helper subsolvers: [synchronization_agent, neighborhood_helper, update_gap_integral]

#1     758.03s best:73565894 next:[-6.35216382e+10,73565893] no_lp fixed_bools:0/11983731
#2     762.35s best:73554558 next:[-6.35216382e+10,73554557] no_lp fixed_bools:0/11983731
#3     775.17s best:73554552 next:[-6.35216382e+10,73554551] no_lp fixed_bools:0/11983731
#4     779.35s best:46685248 next:[-6.35216382e+10,46685247] no_lp fixed_bools:0/11983731
#5     1323.98s best:45488662 next:[-6.35216382e+10,45488661] rnd_var_lns_default(d=0.71 s=10 t=0.10 p=1.00) [presolve]
#Bound 1332.02s best:45488662 next:[15010363,45488661] default_lp initial_propagation
#6     1347.66s best:45325648 next:[15010363,45325647] rnd_cst_lns_default(d=0.29 s=11 t=0.10 p=0.00) [presolve]
#7     1351.99s best:45291556 next:[15010363,45291555] graph_var_lns_default(d=0.29 s=12 t=0.10 p=0.00) [presolve]
#8     1363.64s best:45079459 next:[15010363,45079458] default_lp fixed_bools:0/11983731

#9     1392.45s best:44746366 next:[15010363,44746365] rnd_var_lns_default(d=0.81 s=16 t=0.10 p=1.00) [presolve]

#10    1413.55s best:44443131 next:[15010363,44443130] default_lp fixed_bools:0/11983731