Constraints violation

[arrrdent]

Hello!
I'm having some trouble with formulating constraints. It seems that the constraints for CP-SAT are soft, and I couldn't find a way to make them hard.
The method AddLinearConstraint(SatLinearExpr.Sum(sequence), 0, 1) produces a sequence with a sum of 2, but it should be bounded within [0,1].

Here's a complete example (C# Google.OrTools 9.9.3963 .NET wrapper):

using System;
using System.Collections.Generic;
using Google.OrTools.Sat;
using SatIntVar = Google.OrTools.Sat.IntVar;
using SatLinearExpr = Google.OrTools.Sat.LinearExpr;

class Program
{
    static void Main(string[] args)
    {
        Program program = new Program();
        program.ConstraintsTest();
    }

    private void ConstraintsTest()
    {
        /*
            TASK DEFINITION

            We need to get the next 2D (0,1) assignment to minimize the maximum absolute difference between each element in the targetSum array and the sum of the corresponding column variables. 
            !!! And we also require a constraint to enforce a minimum distance and maximum distance between ones in a row. In other words, we need to ensure there are at least 3 zeros and at most 3 zeros between each pair of consecutive ones in each row !!!

            targetSum
            1, 2, 3, 0, 1, 2, 3, 0, 1 

            columns sum
            1  2  3  0  1  2  3  0  1

            variables with optimal values that we need
            1  0  0  0  1  0  0  0  1
            0  1  0  0  0  1  0  0  0
            0  1  0  0  0  1  0  0  0
            0  0  1  0  0  0  1  0  0
            0  0  1  0  0  0  1  0  0
            0  0  1  0  0  0  1  0  0

            max abs diff (of targetSum and column sum) = 0 

            to formulate this case as an LP problem let's introduce constraints for row sequences:
            maxZeroSeqLen = 3
                (the sum of every sequence of length (maxZeroSeqLen + 1 = 4) in a row must be in [0,1])
            and minNonZeroSeqLen = 4
                (the sum of every sequence of length 4 in row must be >= 1, for example in [1,4])

            P.S. In this specific case we can use a single constraint where the sum of 4 consecutive elements must be equal to 1, but let's use more common definition, cause min and max value can differ.
         */

        int[] targetSum = new[] { 1, 2, 3, 0, 1, 2, 3, 0, 1 };

        int colsNum = targetSum.Length;
        int maxZeroSeqLen = 3;
        int minNonZeroSeqLen = 4;
        int rowsNum = 6;

        CpModel model = new CpModel();

        // create variables
        Google.OrTools.Sat.IntVar[][] assignments = new Google.OrTools.Sat.IntVar[colsNum][];
        for (int col = 0; col < colsNum; col++)
        {
            assignments[col] = new SatIntVar[rowsNum];
            for (int row = 0; row < rowsNum; row++)
            {
                assignments[col][row] = model.NewIntVar(0, 1, $"assignment_{col}_{row}");
            }
        }


        // create constraints
        for (int row = 0; row < rowsNum; row++)
        {
            for (int col = 0; col < colsNum - (maxZeroSeqLen + 1); col++)
            {
                List<SatIntVar> seq1 = new List<SatIntVar>();
                for (int i = 0; i < maxZeroSeqLen + 1; i++)
                {
                    seq1.Add(assignments[col + i][row]);
                }

                model.AddLinearConstraint(SatLinearExpr.Sum(seq1), 0, 1);
            }

            for (int col = 0; col < colsNum - minNonZeroSeqLen; col++)
            {
                List<SatIntVar> seq2 = new List<SatIntVar>();
                for (int i = 0; i < minNonZeroSeqLen; i++)
                {
                    seq2.Add(assignments[col + i][row]);
                }

                model.AddLinearConstraint(SatLinearExpr.Sum(seq2), 1, minNonZeroSeqLen);
            }
        }

        // create target
        SatLinearExpr[] absDiff = new SatLinearExpr[colsNum];
        SatLinearExpr[] sumOnColumns = new SatLinearExpr[colsNum];
        for (int col = 0; col < colsNum; col++)
        {
            sumOnColumns[col] = SatLinearExpr.Sum(assignments[col]);
            absDiff[col] = model.NewIntVar(0, Int32.MaxValue, $"AbsDiffDemand_day_{col}");
            model.AddAbsEquality(absDiff[col], sumOnColumns[col] - targetSum[col]);
        }

        SatLinearExpr maxDifference = model.NewIntVar(0, Int32.MaxValue, "MaxDifference");
        model.AddMaxEquality(maxDifference, absDiff);
        model.Minimize(maxDifference);

        // create the solver
        CpSolver solver = new CpSolver();

        // solve
        CpSolverStatus status = solver.Solve(model);


        // print results
        Console.WriteLine();
        Console.WriteLine($"--- Solve end --- status {status} ---");
        if (status == CpSolverStatus.Feasible || status == CpSolverStatus.Optimal)
        {
            Console.WriteLine($"Best Solution:");
            Console.WriteLine($"{solver.Response.BestObjectiveBound}");

            Console.WriteLine(
                $"maxDifference: {solver.Value(maxDifference)}");

            // get result and print solution
            for (int row = 0; row < rowsNum; row++)
            {
                for (int col = 0; col < colsNum; col++)
                {
                    int res = (int)solver.Value(assignments[col][row]);
                    Console.Write($"{res} ");
                }

                Console.WriteLine();
            }

            Console.WriteLine();
        }
    }
}

And result is

--- Solve end --- status Optimal ---
Best Solution:
0
maxDifference: 0
0 0 1 0 0 0 1 0 1
0 0 1 0 0 0 1 0 0
0 0 1 0 0 0 1 0 0
0 1 0 0 0 1 0 0 0
0 1 0 0 0 1 0 0 0
1 0 0 0 1 0 0 0 0

In the first row, we have an incorrect last sequence with 1 at the end. This value of 1 must be in the last row to avoid violating constraints.

Any advice, suggestions, or examples would be greatly appreciated.
Thank you in advance for your help!

[lperron]

are you including all variables ?

Note that we check all solutions against the model.
So the model is wrong. Either your code, of the LinearExpr.Sum().