Constructing complicated Boolean expressions for SAT solver

[christoph...@ksb.com]

I would like to use a more complex boolean expression similar to the following as the condition in OnlyEnforceIf() for a constraint:

((A == 1) || (A == 2)) && ((B == 0) || (B ==1) || (B == 5)) && (! C)

This is not possible directly in a single step because

 - OnlyEnforceIf() takes an ILiteral (e.g. an IntVar) as its argument, and (A == 1) etc. are BoundIntegerExpressions

 - There is no && or || operator which can be used with BoundIntegerExpressions

 - The expressions like (A == 1) etc. cannot be added directly to the model because then they will constrain the solution.

I found an example of linking an IntVar to the value of an equality comparison (a BoundIntegerExpression) in

https://github.com/google/or-tools/blob/master/ortools/sat/doc/channeling.md: namely

// Implement b == (x >= 5).

model.Add(x >= 5).OnlyEnforceIf(b);

model.Add(x < 5).OnlyEnforceIf(b.Not());

This seems to be the only way to do it although it seems awkward.

Elaborating on this for a more complicated expression such as the one above, I've developed this example.

using Google.OrTools.Sat;


namespace GoogleSATMinimalExample
{
    class BooleanExpressionExample
    {
        CpModel model;


        public void InitModel() {
            model = new CpModel();
            IntVar A = model.NewIntVar(-1, 3, "A");
            IntVar B = model.NewIntVar(-1, 8, "B");
            IntVar C = model.NewBoolVar("C");


            // Link a boolan variable to the expression A == 1
            IntVar Ais1 = model.NewBoolVar("Ais1");
            model.Add(A == 1).OnlyEnforceIf(Ais1);
            model.Add(A != 1).OnlyEnforceIf(Ais1.Not());


            // Proceed similarly for the other variables
            IntVar Ais2 = model.NewBoolVar("Ais2");
            model.Add(A == 2).OnlyEnforceIf(Ais2);
            model.Add(A != 2).OnlyEnforceIf(Ais2.Not());


            IntVar Bis0 = model.NewBoolVar("Bis0");
            model.Add(B == 0).OnlyEnforceIf(Bis0);
            model.Add(B != 0).OnlyEnforceIf(Bis0.Not());


            IntVar Bis1 = model.NewBoolVar("Bis1");
            model.Add(B == 1).OnlyEnforceIf(Bis1);
            model.Add(B != 1).OnlyEnforceIf(Bis1.Not());


            IntVar Bis5 = model.NewBoolVar("Bis5");
            model.Add(B == 5).OnlyEnforceIf(Bis5);
            model.Add(B != 5).OnlyEnforceIf(Bis5.Not());


            // Since no && or || operators are available for BoundIntegerExpressions we need to construct
            // IntVars equivalent to the partial expressions
            IntVar Ais1or2 = model.NewBoolVar("Ais1or2");  // to become equivalent to ((A ==1) || (A == 2))
            model.AddImplication(Ais1or2.Not(), Ais1.Not());
            model.AddImplication(Ais1or2.Not(), Ais2.Not());


            IntVar Bis0or1or5 = model.NewBoolVar("Bis0or1or5"); // to become equivalent to ((B == 0) || (B == 1) || (B == 5))
            model.AddImplication(Bis0or1or5.Not(), Bis0.Not());
            model.AddImplication(Bis0or1or5.Not(), Bis1.Not());
            model.AddImplication(Bis0or1or5.Not(), Bis5.Not());


            // !C can be represented directly as C.Not()


            // Now the complete expression ((A == 1) || (A == 2)) && ((B == 0) || (B ==1) || (B == 5)) && (! C)
            IntVar expr = model.NewBoolVar("expr");
            model.AddImplication(Ais1or2.Not(), expr.Not());
            model.AddImplication(Bis0or1or5.Not(), expr.Not());
            model.AddImplication(C, expr.Not());


            // Now I can use expr as argument to OnlyEnforceIf()
            IntVar D = model.NewIntVar(-1, 5, "D");
            model.Add(D == 1).OnlyEnforceIf(expr);
        }
    }
}

Is this type of construction the best or only way to proceed, or is there a simpler way?

Thanks for any help.

[christoph...@ksb.com]

 Sorry I should have explicitly mentioned I'm using c#.

[Laurent Perron]

You are aware that this model is much more complex than needed:

            // Link a boolan variable to the expression A == 1
            IntVar Ais1 = model.NewBoolVar("Ais1");
            model.Add(A == 1).OnlyEnforceIf(Ais1);
            model.Add(A != 1).OnlyEnforceIf(Ais1.Not());

this is 

    model.Add(a == Ais1)

Furthermore, 

           IntVar Ais1or2 = model.NewBoolVar("Ais1or2");  // to become equivalent to ((A ==1) || (A == 2))
            model.AddImplication(Ais1or2.Not(), Ais1.Not());
            model.AddImplication(Ais1or2.Not(), Ais2.Not());

is not enough.

You need

    model.AddBoolOr(new ILiteral[] {ais1.Not(), Ais2.Not(), Ais1or2});

Finally, 

            // Now the complete expression ((A == 1) || (A == 2)) && ((B == 0) || (B ==1) || (B == 5)) && (! C)
            IntVar expr = model.NewBoolVar("expr");
            model.AddImplication(Ais1or2.Not(), expr.Not());
            model.AddImplication(Bis0or1or5.Not(), expr.Not());
            model.AddImplication(C, expr.Not());

Why not:

    model.AddBoolAnd(new ILiteral() {Ais1or2, Bis0or1or5, C.Not()});

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

Le dim. 4 nov. 2018 à 12:47, <christoph...@ksb.com> a écrit :

 Sorry I should have explicitly mentioned I'm using c#.

--
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.

[christoph...@ksb.com]

Hello, thank you for the quick reply. 

>You are aware that this model is much more complex than needed:

Yes, my post was intended to be an illustrative example only; what I really need is a general way to make an IntVar A equivalent to another expression like (IntVar B == long val), together with boolan and/or operations on the result. In case val == 1 it can be accomplished by using model.Add(A == B) but in the general case of val not known in advance the construction with 

            IntVar AisVal = model.NewBoolVar("AisVal");
            model.Add(A == val).OnlyEnforceIf(AisVal );
            model.Add(A != val).OnlyEnforceIf(AisVal .Not());

is the only way I've found to do it.

Furthermore, 

           IntVar Ais1or2 = model.NewBoolVar("Ais1or2");  // to become equivalent to ((A ==1) || (A == 2))
            model.AddImplication(Ais1or2.Not(), Ais1.Not());
            model.AddImplication(Ais1or2.Not(), Ais2.Not());

is not enough.

You need

    model.AddBoolOr(new ILiteral[] {ais1.Not(), Ais2.Not(), Ais1or2});

Thank you I hadn't noticed that Ais1or2 could be 1 and both Ais1 and Ais2 be 0 unless an additional constraint is added.

 

Finally, 

            // Now the complete expression ((A == 1) || (A == 2)) && ((B == 0) || (B ==1) || (B == 5)) && (! C)
            IntVar expr = model.NewBoolVar("expr");
            model.AddImplication(Ais1or2.Not(), expr.Not());
            model.AddImplication(Bis0or1or5.Not(), expr.Not());
            model.AddImplication(C, expr.Not());

> Why not:

>

>    model.AddBoolAnd(new ILiteral() {Ais1or2, Bis0or1or5, C.Not()});

The above will enforce enforce the condition to be true in the solutions, won't it? I want to use the expression as a condition in OnlyEnforceIf() on a Constraint. The expression could be both true or false in a valid solution.

From your comments I have also inferred that there is no substantially simpler way to create these expressions.

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.

Thanks again for your help.

[Laurent Perron]

Yes, if you create a lot of these, please cache them.

The presolve is not yet good enough to merge all equivalent Boolean variables. 

Good luck with your code.

--

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.

--

--Laurent