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

Question

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

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

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

Answer 1

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

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

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 个。