Boolean constraints over integer expressions in CP-SAT Solver

[Gottfried]

Hi,

For the SAT based CP-SAT python solver is there a more concise way to express boolean constraints of integer expressions than using reification?

x = model.NewIntVar(1,3,"x")

y = model.NewIntVar(1,3,"y")

# Example constraint: x=2 or y=2

# Does not work: model.AddBoolOr([(x==2),(y==2)])

# version with reification (OnlyEnforceIf)

xIs2 = model.NewBoolVar("xis2")

yIs2 = model.NewBoolVar("yis2")

model.Add((x==2)).OnlyEnforceIf(xIs2);

model.Add((x!=2)).OnlyEnforceIf(xIs2.Not());

model.Add((y==2)).OnlyEnforceIf(yIs2);

model.Add((y!=2)).OnlyEnforceIf(yIs2.Not());

model.AddBoolOr([xIs2,yIs2])

KR

  Gottfried

[christoph...@ksb.com]

Hi,

I'm working in c#, not python, but that was the only way I found to do it.  You may have seen the thread  https://groups.google.com/forum/#!topic/or-tools-discuss/8wGnC4V7HdE.

In my project, I plan to create a class MyIntVar which internally maintains a reference to the model and an IntVar, and in which all the operators ==, !=, & and | have been overloaded to allow for easy combination. The overloaded operators will create a new IntVar and post the necessary implication constraints, returning an object with the new reference.

[Laurent Perron]

The second version is the official one. I prefer not to include the expanded version has it does too many hidden things.

For instance, if you create x == 1 and x == 2 booleans. You should add at_most_one on them.

If the domain is fully covered, the you also need a at least one (clause).

then you need to add implications 

x == 1 imply x >= 0 and so on...

That is our current reasoning.

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.