在 ORTOOLS CP-SAT 中设置变量可能唯一值的数量

Question

希望设置/限制 ortools cp-sat 生成的唯一变量的数量。 我目前有 13 个变量的列表，即 x1、x2、x3 ...... 我希望能够确保在这 13 个变量中只给出 5 个唯一值。 我知道我必须为每个变量分配一个布尔变量，但不确定如何执行此操作。 这是另一个得到回答的类似问题，但是当我输入该代码时，我收到一条错误消息，根据他的回答，AddImplication 需要一个布尔值，我的变量应该在其中输入..

How to define a constraint in Ortools to set a limit of distinct values

提前谢谢大家希望有人知道一些事情:)

Answer 1

除了您的变量之外，您还需要为其域 (b1, b2, b3...) 中的每个可能值创建一个新的布尔变量。您将在https://stackoverflow.com/posts/60448315/revisions 中提到的约束中使用这些布尔变量。

然后您需要为每个变量/值添加隐含约束：

x1 == 1 => b1 == 1
x2 == 1 => b1 == 1
...
xn == 1 => b1 == 1

x1 == 2 => b2 == 1
x2 == 2 => b2 == 1
...
xn == 2 => b2 == 1
etc.

然后添加https://stackoverflow.com/posts/60448315/revisions中提到的约束。

这是一个 c# 中的工作示例：

using System;
using System.Collections.Generic;
using System.IO;
using System.Linq;
using System.Text;
using Google.OrTools.Sat;

namespace SO68801590v2
{
    class Program
    {
        static void Main(string[] args)
        {
            try
            {
                Google.OrTools.Sat.CpModel model = new CpModel();
                ORModel myModel = new ORModel();
                myModel.initModel(model);
                IntVar[] decisionVariables = myModel.decisionVariables;

                // Creates a solver and solves the model.
                CpSolver solver = new CpSolver();
                VarArraySolutionPrinter solutionPrinter = new VarArraySolutionPrinter(decisionVariables);
                solver.SearchAllSolutions(model, solutionPrinter);
                Console.WriteLine(String.Format("Number of solutions found: {0}",
                    solutionPrinter.SolutionCount()));
            }
            catch (Exception e)
            {
                Console.WriteLine(e.Message);
                Console.WriteLine(e.StackTrace);
                throw;
            }

            Console.WriteLine("OK");
            Console.ReadKey();
        }
    }

    class ORModel
    {
        const int nVars = 13;
        const int valMin = 28;
        const int valMax = 40;
        const int nValues = valMax - valMin + 1;
        const int maxDifferentValues = 5;
        IntVar[] x = new IntVar[13];
        IntVar[,] b = new IntVar[nVars, nValues];
        IntVar[] b_any = new IntVar[nValues];

        public IntVar[] decisionVariables
        {
            get
            {
                return x;
            }
        }

        public void initModel(CpModel model)
        {

            for (int i = 0; i < nVars; i++)
            {
                // The variables.
                x[i] = model.NewIntVar(valMin, valMax, string.Format("X{0,3:D3}", i + 1));
                for (int j = 0; j < nValues; j++)
                {
                    int value = j + valMin;
                    // A boolean equivalent to "Xi == value j"
                    b[i, j] = model.NewBoolVar(string.Format("X{0,3:D3}_{1,3:D3}", i + 1, value));
                    model.Add(x[i] == value).OnlyEnforceIf(b[i, j]);
                    model.Add(x[i] != value).OnlyEnforceIf(b[i, j].Not());
                }
            }
            // Booleans equivalent to "some value X == value j"
            for (int j = 0; j < nValues; j++)
            {
                List<IntVar> list = new List<IntVar>();
                for (int i = 0; i < nVars; i++)
                {
                    list.Add(b[i, j]);
                }
                int value = j + valMin;
                b_any[j] = model.NewBoolVar(string.Format("Value{0,3:D3}IsPresent", value));
                model.AddMaxEquality(b_any[j], list);
            }
            // Now make sure we respect the limit of distinct values
            model.Add(new SumArray(b_any) <= maxDifferentValues);
        }
    }

    public class VarArraySolutionPrinter : CpSolverSolutionCallback
    {
        private int solution_count_;
        private IntVar[] variables;

        public VarArraySolutionPrinter(IntVar[] variables)
        {
            this.variables = variables;
        }
        public override void OnSolutionCallback()
        {
            // using (StreamWriter sw = new StreamWriter(@"C:\temp\GoogleSATSolverExperiments.txt", true, Encoding.UTF8))
            using (TextWriter sw = Console.Out)
            {
                sw.Write(String.Format("Solution #{0}: time = {1:F2} s;",
                solution_count_, WallTime()));
                foreach (IntVar v in variables)
                {
                    sw.Write(
                    String.Format(" {0} =; {1};\r\n", v.ShortString(), Value(v)));
                }
                solution_count_++;
                sw.WriteLine();
            }
            if (solution_count_ >= 10)
            {
                StopSearch();
            }
        }
        public int SolutionCount()
        {
            return solution_count_;
        }

    }
}

由于有很多有效的解决方案，我将打印输出限制为 10 个。

Answer 2

在考虑了更多之后，我提出了另一个需要更少变量的建议。

除了名义变量本身

IntVar[] x;

我们可以列出给定解决方案中最多五个值的列表

IntVar[] values;

然后使用 AddElement 约束来确保每个变量都等于这些值之一。我们定义了一组索引并使用

IntVar[] indices;
for (int i = 0; i < nVars; i++)
{
    model.AddElement(indices[i], values, x[i]);
}

AddElement 约束确保x[i] == values[indices[i]]

例如：如果values[1] = 29 和indices[3] = 1，那么x[3] 必须是values[indices[3]] = values[1] = 29

值和索引根本不需要限制，它们可以合法地取其域中的任何元素，之后变量 x 都是固定的。为了避免在 x 变量中得到太多重复的解，我们可以将数组中的值限制为完全不同，作为一种对称性破坏。

这是一个演示该想法的有效 C# 代码：

using Google.OrTools.Sat;
using System;
using System.Collections.Generic;
using System.IO;
using System.Linq;
using System.Text;

namespace SO68801590v3
{
    class Program
    {
        static void Main(string[] args)
        {
            try
            {
                Google.OrTools.Sat.CpModel model = new CpModel();
                ORModel myModel = new ORModel();
                myModel.initModel(model);
                IntVar[] decisionVariables = myModel.decisionVariables;

                // Creates a solver and solves the model.
                CpSolver solver = new CpSolver();
                VarArraySolutionPrinter solutionPrinter = new VarArraySolutionPrinter(myModel.variablesToPrintOut);
                solver.SearchAllSolutions(model, solutionPrinter);
                Console.WriteLine(String.Format("Number of solutions found: {0}",
                    solutionPrinter.SolutionCount()));
            }
            catch (Exception e)
            {
                Console.WriteLine(e.Message);
                Console.WriteLine(e.StackTrace);
                throw;
            }

            Console.WriteLine("OK");
            Console.ReadKey();
        }
    }

    class ORModel
    {
        const int nVars = 13;
        const int valMin = 28;
        const int valMax = 40;
        const int nValues = valMax - valMin + 1;
        const int maxDifferentValues = 5;
        IntVar[] x = new IntVar[nVars];
        IntVar[] values = new IntVar[maxDifferentValues];
        IntVar[] indices = new IntVar[nVars];

        public IntVar[] decisionVariables
        {
            get
            {
                return x;
            }
        }

        public IntVar[] variablesToPrintOut
        {
            get
            {
                IntVar[] variablesToPrintOut_ = new IntVar[2 * nVars + maxDifferentValues];
                int ix = 0;
                for (int i = 0; i < nVars; i++)
                {
                    variablesToPrintOut_[ix] = x[i];
                    ix++;
                }
                for (int i = 0; i < nVars; i++)
                {
                    variablesToPrintOut_[ix] = indices[i];
                    ix++;
                }
                for (int j = 0; j < maxDifferentValues; j++)
                {
                    variablesToPrintOut_[ix] = values[j];
                    ix++;
                }
                return variablesToPrintOut_;
            }
        }

        public void initModel(CpModel model)
        {
            // Make variables and indices
            for (int i = 0; i < nVars; i++)
            {
                x[i] = model.NewIntVar(valMin, valMax, string.Format("X{0,3:D3}", i + 1));
                indices[i] = model.NewIntVar(0, maxDifferentValues - 1, string.Format("Index{0,3:D3}", i + 1));
            }
            // Make the list of different values
            for (int j = 0; j < maxDifferentValues; j++)
            {
                values[j] = model.NewIntVar(valMin, valMax, string.Format("Value{0,3:D3}", j + 1));
            }
            // Each variable has to be one of the defined values
            // We'll use the AddElement constraint for this
            // AddElement adds the element constraint: variables[index] == target
            for (int i = 0; i < nVars; i++)
            {
                model.AddElement(indices[i], values, x[i]);
            }
            // As a kind of "symmetry breaking" we'll also make sure that the values are
            // all different to avoid returning too many duplicate solutions
            model.AddAllDifferent(values);
        }
    }

    public class VarArraySolutionPrinter : CpSolverSolutionCallback
    {
        private int solution_count_;
        private IntVar[] variables;

        public VarArraySolutionPrinter(IntVar[] variables)
        {
            this.variables = variables;
        }
        public override void OnSolutionCallback()
        {
            // using (StreamWriter sw = new StreamWriter(@"C:\temp\GoogleSATSolverExperiments.txt", true, Encoding.UTF8))
            using (TextWriter sw = Console.Out)
            {
                sw.WriteLine(String.Format("Solution #{0}: time = {1:F2} s;",
                solution_count_, WallTime()));
                foreach (IntVar v in variables)
                {
                    sw.Write(
                    String.Format(" {0} = {1}\r\n", v.ShortString(), Value(v)));
                }
                solution_count_++;
                sw.WriteLine();
            }
            if (solution_count_ >= 10)
            {
                StopSearch();
            }
        }
        public int SolutionCount()
        {
            return solution_count_;
        }
    }
}