Reification in CP-SAT solver python

[Gergő Rozner]

Hi!

I just started to get familiar with eht CP-SAT API, and was thinking to solve smaller problems to learn the basics.

I'm tryign to solve the "magic series" / "magic sequence" problem based on the following pseudo-code:

int n = 5
range D = 0..n-1
var{int} series[D] in D;
solve {
  forall(k in D)
    series[k] = sum(i in D) (series[i]=k)

I spent the last 2 days to implement the reified constraints, and I think I went through all the availabe materials that are available on the internet. Also found an example which solves it with the old solver: https://github.com/google/or-tools/blob/master/examples/python/magic_sequence_distribute.py . I didn't find any material on the distribute function and whether it is available in the new solver or not.

Anyway my goal is to find out how can I sum literal sonditions. I tried several versions with different type of constarints. I got at least to a version which doesn't throw error, but it says the problem is infeasable.

from ortools.sat.python import cp_model

model = cp_model.CpModel()

n = 5

values = range(n)

my_vars = [model.NewIntVar(0,n-1, 'x%i' % i) for i in values]

for k in values:

  tmp_array = []

    for i in values:

      tmp_var = model.NewBoolVar("")

      model.Add((my_vars[i] == k)).OnlyEnforceIf(tmp_var)

      tmp_array.append(tmp_var)

    model.Add(sum(tmp_array) == k)

    

#model.Add(my_vars[k] == sum((my_vars[i] == k) for i in values))

#model.AddSumConstraint([my_vars[i] == k for i in values], k, k)

solver = cp_model.CpSolver()

solution_printer = SolutionPrinter(my_vars)

status = solver.SearchForAllSolutions(model, solution_printer)

Can someone help how to implement reified constarints?

Thank you!

[Laurent Perron]

mostly good.

Please add:

  model.Add(my_vars[i] != k).OnlyEnforceIf(tmp_var.Not())

to have an equivalence between tmp_var and my_vars[i] == 4. Currently you only an implication. 

and change the sum constraint to:

  model.Add(sum(tmp_array) == my_vars[k])

as this is the correct one.

Please note that

  model.Add(sum(my_vars) == n) 

will help.

And finally, your code does not have a solution printer. So add one, or do not call it.

I attach a working code.

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.
For more options, visit https://groups.google.com/d/optout.

[Gergő Rozner]

Oh, thank you very much. Yeah, I have the solution printer, just didn't include it here to have shorter post.

Such a nice community:) I hope shortly I will be useful here and be able to help others :)

[Gergő Rozner]

One question actually. 

Why is it important to call cp_model.CpSolverSolutionCallback.__init__(self) in the solution printer constructor? 

I used solution printer in other task without this and it worked also.

On Friday, September 14, 2018 at 3:06:52 PM UTC+2, Laurent Perron wrote:

[Laurent Perron]

cp_model.CpSolverSolutionCallback inherits from pywrapsat.SolutionCallback which is a director class in SWIG.

I believe you need to make sure the super of that class is called to setup up the cross language magic.

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

[Gergő Rozner]

Well, that makes sense. Thank you for your help!