Cp-Sat: Channeling constraints

[Peter Bruch]

Hello,

I am using the Cp-Sat solver in order to solve constraints generated from a custom domain-specific language.

With the Dsl arbitrary long pseudo boolean constraints can be written, like:

```

bool0 AND bool1 -> (int0 > 15 AND !(bool3 or bool4))

```.

In the end, I have an expression-tree from my Dsl and want to encode it into a Cp-Sat constraint. Therefore I am using a typical Visitor that walks up the expression tree for each term and creates a corresponding term with the Cp-Model methods.

Since I did not find any other way to channel my constraints I introduce 1 boolean variable for each term of my constraint and reify the term with the variable.

```

protected override IntVar ConvertTerm(Operators op, IntVar left, IntVar right = null)
{
   ReifiedVariable = _model.NewBoolVar(string.Empty);
   switch (op)
   {
    case Operators.And:
       _model.AddBoolAnd(new[] { left, right })
           .OnlyEnforceIf(ReifiedVariable);
       _model.AddBoolOr(new[] { left.Not(), right.Not() })
           .OnlyEnforceIf(ReifiedVariable.Not());
       break;

   case Operators.Or:
      _model.AddBoolOr(new[] { left, right })
          .OnlyEnforceIf(ReifiedVariable);
      _model.AddBoolAnd(new[] { left.Not(), right.Not() })
         .OnlyEnforceIf(ReifiedVariable.Not());

      break;

    case Operators.Implies:
    case Operators.Greater:
...

```

E.g. !( x || y) becomes to b2 <-> !(b1 <-> b0 <-> y || x)

The Problem: I did a lot of Benchmarks with different models but in the end, the Cp-Sat solver is around 10 times slower than the old Constraint solver. 

I suspect my approach with channeling the terms introduces a lot of unnecessary variables and complexity.

For example, a model with 100 Constraints and 186 boolean variables creates 

 1330 Constraints and 863 boolean variables (186 model variables + 677 reified variables) in the CpModel. 

Solving this model costs 263ms with the old constraint solver but 3690ms with the Cp-Sat solver. 

Is there any other idea to  encode arbitrary long constraints in the Cp-Sat solver?

Best regards

Peter

[Laurent Perron]

Do you cache/merge equivalent nodes in the syntax tree ?

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/eaaaaaf9-8238-43d0-b2d1-6db932702142n%40googlegroups.com.