Proven Infeasible CP SAT

[Iqbal Nur Fauzi]

Currently i work with ortools cp-sat to solve scheduling problem with some constraint. But it says that proven infeasible. How can i know what constraint than could make the cp-sat decided "proven infeasible" ? 

This is the log while creating the model : Thanks.

Parameters: max_time_in_seconds: 3600 log_search_progress: true search_branching: AUTOMATIC_SEARCH num_search_workers: 99

Optimization model '':

#Variables: 4222 (1 in objective)

 - 2119 in [0,1]

 - 14 in [0,894]

 - 1387 in [0,928875]

 - 693 in [1,928875]

 - 9 constants in {1,2,3,4,6,12,13,21,1038}

#kBoolAnd: 21 (#enforced: 21) (#literals: 42)

#kBoolOr: 7 (#enforced: 7) (#literals: 14)

#kCumulative: 8

#kIntDiv: 14

#kIntMax: 1

#kInterval: 1144 (#enforced: 451)

#kLinear1: 1621 (#enforced: 28)

#kLinear2: 112 (#enforced: 84)

#kLinear3: 7

#kLinearN: 28 (#enforced: 28)

*** starting model expansion at 0.01s

*** starting model presolve at 0.01s

Unsat after presolving constraint #1312 (warning, dump might be inconsistent): linear { vars: 2072 coeffs: 1 }

- 21 affine relations were detected.

- 21 variable equivalence relations were detected.

- rule 'bool_or: removed enforcement literal' was applied 14 times.

- rule 'cumulative: convert to no_overlap' was applied 2 times.

- rule 'cumulative: no intervals' was applied 2 times.

- rule 'enforcement literal not used' was applied 2 times.

- rule 'int_div: linearize positive division with a constant divisor' was applied 14 times.

- rule 'int_div: updated domain of target in target = X / cte' was applied 1 time.

- rule 'interval: reduced domains' was applied 693 times.

- rule 'interval: unused, converted to linear' was applied 449 times.

- rule 'linear: divide by GCD' was applied 5 times.

- rule 'linear: negative clause' was applied 7 times.

- rule 'linear: positive equal one' was applied 7 times.

- rule 'linear: reduced variable domains' was applied 7 times.

- rule 'linear: simplified rhs' was applied 70 times.

- rule 'linear: size one' was applied 6 times.

- rule 'presolve: iteration' was applied 1 time.

Satisfaction model '':

#Variables: 0

#kBoolOr: 1 (#literals: 0)

*** starting Search at 0.04s with 99 workers and strategies: [ auto, less encoding, no_lp, max_lp, random, random_1, random_2, random_3, random_4, random_5, random_6, random_7, random_8, random_9, random_10, random_11, random_12, random_13, random_14, random_15, random_16, random_17, random_18, random_19, random_20, random_21, random_22, random_23, random_24, random_25, random_26, random_27, random_28, random_29, random_30, random_31, random_32, random_33, random_34, random_35, random_36, random_37, random_38, random_39, random_40, random_41, random_42, random_43, random_44, random_45, random_46, random_47, random_48, random_49, random_50, random_51, random_52, random_53, random_54, random_55, random_56, random_57, random_58, random_59, random_60, random_61, random_62, random_63, random_64, random_65, random_66, random_67, random_68, random_69, random_70, random_71, random_72, random_73, random_74, random_75, random_76, random_77, random_78, random_79, random_80, random_81, random_82, random_83, random_84, random_85, random_86, random_87, random_88, random_89, random_90, random_91, random_92, random_93, random_94 ]

#Done    0.05s  auto [loading]

#Done    0.05s  less encoding [loading]

CpSolverResponse:

status: INFEASIBLE

objective: NA

best_bound: NA

booleans: 0

conflicts: 0

branches: 0

propagations: 0

integer_propagations: 0

walltime: 0.0549262

usertime: 0.0549268

deterministic_time: 0

2021-11-16 00:43:21,012 model.py 279 Thread-17 INFO

2021-11-16 00:43:21,013 model.py 286 Thread-17 INFO     Time elapsed while creating object solver : 0.054926824000000006 seconds

2021-11-16 00:43:21,014 model.py 299 Thread-17 INFO     ==NOT FOUND !!!==

[christoph...@ksb.com]

To look for constraints causing the infeasibility, see the discussion in this post:  https://github.com/google/or-tools/issues/973