Wrap CP-SAT assumptions

makefiles/Makefile.cpp.mk

@@ -431,6 +431,7 @@ test_cc_constraint_solver_samples: \
 .PHONY: test_cc_sat_samples # Build and Run all C++ Sat Samples (located in ortools/sat/samples)
 test_cc_sat_samples: \
  rcc_assignment_sat \
+ rcc_assumptions_sample_sat \
  rcc_binpacking_problem_sat \
  rcc_bool_or_sample_sat \
  rcc_channeling_sample_sat \

makefiles/Makefile.dotnet.mk

@@ -576,6 +576,7 @@ test_dotnet_linear_solver_samples:
 .PHONY: test_dotnet_sat_samples # Build and Run all .Net SAT Samples (located in ortools/sat/samples)
 test_dotnet_sat_samples:
 	$(MAKE) run SOURCE=ortools/sat/samples/AssignmentSat.cs
+	$(MAKE) run SOURCE=ortools/sat/samples/AssumptionsSampleSat.cs
 	$(MAKE) run SOURCE=ortools/sat/samples/BinPackingProblemSat.cs
 	$(MAKE) run SOURCE=ortools/sat/samples/BoolOrSampleSat.cs
 	$(MAKE) run SOURCE=ortools/sat/samples/ChannelingSampleSat.cs

makefiles/Makefile.java.mk

@@ -657,6 +657,7 @@ test_java_linear_solver_samples: \
 .PHONY: test_java_sat_samples # Build and Run all Java SAT Samples (located in ortools/sat/samples)
 test_java_sat_samples: \
  rjava_AssignmentSat \
+ rjava_AssumptionsSampleSat \
  rjava_BinPackingProblemSat \
  rjava_BoolOrSampleSat \
  rjava_ChannelingSampleSat \

makefiles/Makefile.python.mk

@@ -586,6 +586,7 @@ test_python_linear_solver_samples: \
 .PHONY: test_python_sat_samples # Run all Python Sat Samples (located in ortools/sat/samples)
 test_python_sat_samples: \
  rpy_assignment_sat \
+ rpy_assumptions_sample_sat \
  rpy_binpacking_problem_sat \
  rpy_bool_or_sample_sat \
  rpy_channeling_sample_sat \

ortools/java/com/google/ortools/sat/CpModel.java

@@ -966,6 +966,18 @@ public final class CpModel {
     modelBuilder.getSolutionHintBuilder().addValues(value);
   }
 
+  /** Adds variable as assumption */
+  public void addAssumption(Literal lit) {
+    modelBuilder.addAssumptions(lit.getIndex());
+  }
+
+  /** Adds multiple variables to the assumptions */
+  public void addAssumptions(Literal[] literals) {
+    for (Literal lit : literals) {
+      addAssumption(lit);
+    }
+  }
+
   // Objective.
 
   /** Adds a minimization objective of a linear expression. */

ortools/java/com/google/ortools/sat/CpSolver.java

@@ -115,6 +115,10 @@ public final class CpSolver {
     return solveResponse.getUserTime();
   }
 
+  public java.util.List<Integer> sufficientAssumptionsForInfeasibility() {
+    return solveResponse.getSufficientAssumptionsForInfeasibilityList();
+  }
+
   /** Returns the builder of the parameters of the SAT solver for modification. */
   public SatParameters.Builder getParameters() {
     return solveParameters;

ortools/sat/cp_model.cc

@@ -796,6 +796,16 @@ void CpModelBuilder::AddHint(IntVar var, int64 value) {
   cp_model_.mutable_solution_hint()->add_values(value);
 }
 
+void CpModelBuilder::AddAssumption(BoolVar lit) {
+  cp_model_.mutable_assumptions()->Add(lit.index_);
+}
+
+void CpModelBuilder::AddAssumptions(absl::Span<const BoolVar> literals) {
+  for (const BoolVar& lit : literals) {
+    cp_model_.mutable_assumptions()->Add(lit.index_);
+  }
+}
+
 int64 SolutionIntegerValue(const CpSolverResponse& r, const LinearExpr& expr) {
   int64 result = expr.constant();
   for (int i = 0; i < expr.variables().size(); ++i) {

ortools/sat/cp_model.h

@@ -859,6 +859,12 @@ class CpModelBuilder {
   /// Adds hinting to a variable.
   void AddHint(IntVar var, int64 value);
 
+  /// Adds a variable to the assumptions.
+  void AddAssumption(BoolVar lit);
+
+  /// Adds multiple variables to the assumptions.
+  void AddAssumptions(absl::Span<const BoolVar> literals);
+
   // TODO(user) : add MapDomain?
 
   const CpModelProto& Build() const { return Proto(); }

ortools/sat/csharp/CpModel.cs

@@ -615,6 +615,19 @@ namespace Google.OrTools.Sat
             model_.SolutionHint.Values.Add(value);
         }
 
+        public void AddAssumption(ILiteral lit)
+        {
+            model_.Assumptions.Add(lit.GetIndex());
+        }
+
+        public void AddAssumptions(IEnumerable<ILiteral> literals)
+        {
+            foreach (ILiteral lit in literals)
+            {
+                AddAssumption(lit);
+            }
+        }
+
         // Internal methods.
 
         void SetObjective(LinearExpr obj, bool minimize)

ortools/sat/csharp/CpSolver.cs

@@ -185,6 +185,11 @@ namespace Google.OrTools.Sat
             return response_.WallTime;
         }
 
+        public IList<int> SufficientAssumptionsForInfeasibility()
+        {
+            return response_.SufficientAssumptionsForInfeasibility;
+        }
+
         private CpModelProto model_;
         private CpSolverResponse response_;
         string string_parameters_;

ortools/sat/python/cp_model.py

@@ -1544,8 +1544,17 @@ class CpModel(object):
         self.__model.solution_hint.values.append(value)
 
     def ClearHints(self):
-        del self.__model.solution_hint.vars[:]
-        del self.__model.solution_hint.values[:]
+        self.__model.ClearField("solution_hint")
+
+    def AddAssumption(self, lit):
+        self.__model.assumptions.append(self.GetOrMakeBooleanIndex(lit))
+
+    def AddAssumptions(self, literals):
+        for lit in literals:
+            self.AddAssumption(lit)
+
+    def ClearAssumptions(self):
+        self.__model.ClearField("assumptions")
 
 
 def EvaluateLinearExpr(expression, solution):
@@ -1708,6 +1717,10 @@ class CpSolver(object):
         """Returns the response object."""
         return self.__solution
 
+    def SufficientAssumptionsForInfeasibility(self):
+        """Returns the indices of the infeasible assumptions."""
+        return self.__solution.sufficient_assumptions_for_infeasibility
+
 
 class CpSolverSolutionCallback(pywrapsat.SolutionCallback):
     """Solution callback.

ortools/sat/samples/AssumptionsSampleSat.cs

@@ -0,0 +1,52 @@
+// Copyright 2021 Xiang Chen
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// [START program]
+using System;
+using Google.OrTools.Sat;
+
+public class AssumptionsSampleSat
+{
+    static void Main()
+    {
+        // Creates the model.
+        // [START model]
+        CpModel model = new CpModel();
+        // [END model]
+
+        // Creates the variables.
+        // [START variables]
+        IntVar x = model.NewIntVar(0, 10, "x");
+        IntVar y = model.NewIntVar(0, 10, "y");
+        IntVar a = model.NewBoolVar("a");
+        IntVar b = model.NewBoolVar("b");
+        // [END variables]
+
+        // Creates the constraints.
+        // [START constraints]
+        model.Add(x > 10).OnlyEnforceIf(a);
+        model.Add(y <= 10).OnlyEnforceIf(b);
+        // [END constraints]
+
+        // Add assumptions
+        model.AddAssumptions(new ILiteral[] { a, b });
+
+        // Creates a solver and solves the model.
+        // [START solve]
+        CpSolver solver = new CpSolver();
+        CpSolverStatus status = solver.Solve(model);
+        Console.WriteLine(solver.SufficientAssumptionsForInfeasibility());
+        // [END solve]
+    }
+}
+// [END program]

ortools/sat/samples/AssumptionsSampleSat.csproj

@@ -0,0 +1,24 @@
+<Project Sdk="Microsoft.NET.Sdk">
+  <PropertyGroup>
+    <OutputType>Exe</OutputType>
+    <LangVersion>7.3</LangVersion>
+    <TargetFramework>netcoreapp2.1</TargetFramework>
+    <EnableDefaultItems>false</EnableDefaultItems>
+    <!-- see https://github.com/dotnet/docs/issues/12237 -->
+    <RollForward>LatestMajor</RollForward>
+    <RestoreSources>../../../packages;$(RestoreSources);https://api.nuget.org/v3/index.json</RestoreSources>
+    <AssemblyName>Google.OrTools.AssumptionsSampleSat</AssemblyName>
+    <IsPackable>true</IsPackable>
+  </PropertyGroup>
+
+  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
+    <DebugType>full</DebugType>
+    <Optimize>true</Optimize>
+    <GenerateTailCalls>true</GenerateTailCalls>
+  </PropertyGroup>
+
+  <ItemGroup>
+    <Compile Include="AssumptionsSampleSat.cs" />
+    <PackageReference Include="Google.OrTools" Version="8.2.*" />
+  </ItemGroup>
+</Project>

ortools/sat/samples/AssumptionsSampleSat.java

@@ -0,0 +1,60 @@
+// Copyright 2021 Xiang Chen
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// [START program]
+package com.google.ortools.sat.samples;
+
+import com.google.ortools.Loader;
+import com.google.ortools.sat.CpModel;
+import com.google.ortools.sat.CpSolver;
+import com.google.ortools.sat.CpSolverSolutionCallback;
+import com.google.ortools.sat.IntVar;
+import com.google.ortools.sat.LinearExpr;
+import com.google.ortools.sat.Literal;
+
+/** Minimal CP-SAT example to showcase assumptions. */
+public class AssumptionsSampleSat {
+  public static void main(String[] args) throws Exception {
+    Loader.loadNativeLibraries();
+    // Create the model.
+    // [START model]
+    CpModel model = new CpModel();
+    // [END model]
+
+    // Create the variables.
+    // [START variables]
+    IntVar x = model.newIntVar(0, 10, "x");
+    IntVar y = model.newIntVar(0, 10, "y");
+    IntVar a = model.newBoolVar("a");
+    IntVar b = model.newBoolVar("b");
+    // [END variables]
+
+    // Creates the constraints.
+    // [START constraints]
+    model.addGreaterThan(x, 10).onlyEnforceIf(a);
+    model.addLessOrEqual(y, 10).onlyEnforceIf(b);
+    // [END constraints]
+
+    // Add assumptions
+    model.addAssumptions(new Literal[] {a, b});
+
+    // Create a solver and solve the model.
+    // [START solve]
+    CpSolver solver = new CpSolver();
+    solver.solve(model);
+    System.out.println(solver.sufficientAssumptionsForInfeasibility());
+    // [END solve]
+  }
+
+}
+// [END program]

ortools/sat/samples/assumptions_sample_sat.cc

@@ -0,0 +1,58 @@
+// Copyright 2021 Xiang Chen
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// [START program]
+#include "ortools/sat/cp_model.h"
+#include "ortools/sat/model.h"
+
+namespace operations_research {
+namespace sat {
+
+void AssumptionsSampleSat() {
+  // [START model]
+  CpModelBuilder cp_model;
+  // [END model]
+
+  // [START variables]
+  const Domain domain(0, 10);
+  const IntVar x = cp_model.NewIntVar(domain).WithName("x");
+  const IntVar y = cp_model.NewIntVar(domain).WithName("y");
+  const BoolVar a = cp_model.NewBoolVar().WithName("a");
+  const BoolVar b = cp_model.NewBoolVar().WithName("b");
+  // [END variables]
+
+  // [START constraints]
+  cp_model.AddGreaterThan(x, 10).OnlyEnforceIf(a);
+  cp_model.AddLessOrEqual(y, 10).OnlyEnforceIf(b);
+  // [END constraints]
+
+  // Add assumptions
+  cp_model.AddAssumptions({a, b});
+
+  // Solving part.
+  // [START solve]
+  const CpSolverResponse response = Solve(cp_model.Build());
+  LOG(INFO) << CpSolverResponseStats(response);
+  LOG(INFO) << response.sufficient_assumptions_for_infeasibility()[0];
+  // [END solve]
+}
+
+}  // namespace sat
+}  // namespace operations_research
+
+int main() {
+  operations_research::sat::AssumptionsSampleSat();
+
+  return EXIT_SUCCESS;
+}
+// [END program]

ortools/sat/samples/assumptions_sample_sat.py

@@ -0,0 +1,54 @@
+# Copyright 2021 Xiang Chen
+# Licensed under the Apache License, Version 2.0 (the "License");
+# you may not use this file except in compliance with the License.
+# You may obtain a copy of the License at
+#
+#     http://www.apache.org/licenses/LICENSE-2.0
+#
+# Unless required by applicable law or agreed to in writing, software
+# distributed under the License is distributed on an "AS IS" BASIS,
+# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+# See the License for the specific language governing permissions and
+# limitations under the License.
+"""Code sample that solves a model and gets the infeasibility assumptions."""
+
+# [START program]
+from ortools.sat.python import cp_model
+
+
+def AssumptionsSampleSat():
+    """Showcases assumptions."""
+    # Creates the model.
+    # [START model]
+    model = cp_model.CpModel()
+    # [END model]
+
+    # Creates the variables.
+    # [START variables]
+    x = model.NewIntVar(0, 10, 'x')
+    y = model.NewIntVar(0, 10, 'y')
+    a = model.NewBoolVar('a')
+    b = model.NewBoolVar('b')
+    # [END variables]
+
+    # Creates the constraints.
+    # [START constraints]
+    model.Add(x > 10).OnlyEnforceIf(a)
+    model.Add(y <= 10).OnlyEnforceIf(b)
+    # [END constraints]
+
+    # Add assumptions
+    model.AddAssumptions([a, b])
+
+    # Creates a solver and solves.
+    # [START solve]
+    solver = cp_model.CpSolver()
+    status = solver.Solve(model)
+    # [END solve]
+
+    print('Status = %s' % solver.StatusName(status))
+    print('SufficientAssumptionsForInfeasibility = %s' % solver.SufficientAssumptionsForInfeasibility())
+
+
+AssumptionsSampleSat()
+# [END program]