trying to solve huge mode on CP-Sat

[Josh Friedman]

I am working on a model that probably has 500,000 to 1,000,000 boolean variables. My python script generates the model, it seems to execute the line

 status = solver.SolveWithSolutionCallback(model, solution_printer)

but it doesn't solve anything, just goes to the next line.

When I limit the size of the model, it does solve (or at least attempt find an optimal solution).

Anyone have any suggestion? I can post the full code.

print('Ready to Solve')
    solver = cp_model.CpSolver()
    print('Created Solver')
    solver.parameters.max_time_in_seconds = 10000
    solver.parameters.num_search_workers = 6
#    status = solver.Solve(model)
    solution_printer = cp_model.ObjectiveSolutionPrinter()
    status = solver.SolveWithSolutionCallback(model, solution_printer)
    print('Finished Solving')
    if status == cp_model.OPTIMAL:
        print('found optimal')
        print('Total edges = %i' % solver.ObjectiveValue())

[Laurent Perron]

add solver.parameters.log_search_progress = True

most likely, your problem is infeasible.

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

--
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/96b4b74d-0385-41c4-9c8e-b077e946b37fn%40googlegroups.com.

[Joshua Friedman]

It does say it's infeasible. I am not sure it really is infeasible, but I'll try to track down the issue. Does it create an IIS tree?

Parameters: max_time_in_seconds: 10000 log_search_progress: true num_search_workers: 6
Optimization model '':
#Variables: 89786 (59340 in objective)
 - 89786 in [0,1]
#kBoolOr: 735777 (#literals: 2207331)
#kLinear1: 1942
#kLinear2: 1170
#kLinear3: 1036
#kLinearN: 4532 (#terms: 54287)
*** starting model presolve at 0.14s
Unsat after presolving constraint #8586 (warning, dump might be inconsistent): linear { domain: -9223372036854775808 domain: -12 }
- 1170 affine relations were detected.
- 0 variable equivalence relations were detected.
- rule 'affine: new relation' was applied 1170 times.
- rule 'bool_or: always true' was applied 55886 times.
- rule 'bool_or: implications' was applied 43457 times.
- rule 'bool_or: only one literal' was applied 36 times.
- rule 'linear: empty' was applied 16 times.
- rule 'linear: fixed or dup variables' was applied 16 times.
- rule 'linear: positive equal one' was applied 5223 times.
- rule 'linear: remapped using affine relations' was applied 14 times.
- rule 'linear: simplified rhs' was applied 28 times.
- rule 'linear: size one' was applied 1942 times.
- rule 'presolve: iteration' was applied 1 time.
Satisfaction model '':
#Variables: 0
#kBoolOr: 1 (#literals: 0)
*** starting Search at 1.65s with 6 workers and subsolvers: [ default_lp, less_encoding, no_lp, max_lp, quick_restart, feasibility_pump, rins_lns_default, rens_lns_default ]
#Done    1.65s  no_lp [loading]
#Done    1.65s  no_lp [loading]
#Done    1.65s  default_lp [loading]
#Done    1.65s  default_lp [loading]
#Done    1.65s  quick_restart [loading]
#Done    1.65s  quick_restart [loading]
#Done    1.65s  feasibility_pump [loading]
#Done    1.65s  max_lp [loading]
#Done    1.65s  max_lp [loading]
#Done    1.65s  less_encoding [loading]
#Done    1.65s  less_encoding [loading]
CpSolverResponse:
status: INFEASIBLE
objective: NA
best_bound: NA
booleans: 0
conflicts: 0
branches: 0
propagations: 0
integer_propagations: 0
restarts: 0
lp_iterations: 0
walltime: 1.65059
usertime: 1.65059
deterministic_time: 0
primal_integral: 0
Finished Solving

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

--

Joshua Friedman PhD
Crown...@gmail.com
http://www.math.sunysb.edu/~joshua

[Laurent Perron]

No for the IIS.

You can write the model to file with model.ExportToFile(...)

The run the sat_runner binary with parameters

--input <path to exported model> --logtostderr -v 2

It will log every presolve step. This is where the model is found infeasible.

I hope this helps.

To view this discussion on the web visit https://groups.google.com/d/msgid/or-tools-discuss/CABsGjsr-ORksd4Bw42eNaEVbDVNNDtYpYDTk3mhemeB%2BO5vuTQ%40mail.gmail.com.

--

--Laurent

[Joshua Friedman]

Laurent

Thanks very much. Your advice is much appreciated. I found one mistake in my code that lead to infeasibility.

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

[iga...@gmail.com]

Hi,

I am a bit in the same spot, thought I have developed some automatic functionalities to detect IIS. It seems that when the problem is infeasible (but there is no Unsat after ...) everything goes well and I am able to detect the ISS but with Unsat after... it does not work well.

I am trying to run the sat_runner as mentioned above but it crashes with segmentation fault (raw text file for the model is 6GB and the zipped file about 300MB). Any clues?

Thank you in advance

[Joshua Friedman]

Try increasing swap space. 

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/VjiSYjFFB_4/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/9d478400-1363-4784-9907-b0344dcf7dben%40googlegroups.com.

[Laurent Perron]

There is a 2gb limit on proto size (internal size). 

To view this discussion on the web visit https://groups.google.com/d/msgid/or-tools-discuss/CABsGjso1CEpqUtL%3DzLAaa%2Bq4woZSDsAWhShpfwUBT31iA-KEnQ%40mail.gmail.com.