always-cautious/ortools-clone
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

c# support for sat, + micro test using the cp_model proto in C#

Browse Source
This commit is contained in:
Laurent Perron
2017-08-01 16:14:04 -07:00
parent 2a64d85317
commit 0c02286320
7 changed files with 284 additions and 28 deletions
Download Patch File Download Diff File Expand all files Collapse all files

142
examples/tests/testsat.cs Normal file
View File

@@ -0,0 +1,142 @@
// Copyright 2010-2014 Google
// 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.
using System;
using Google.OrTools.Sat;
public class CsTestCpOperator
{
// TODO(user): Add proper tests.
static int error_count_ = 0;
static void Check(bool test, String message)
{
if (!test)
{
Console.WriteLine("Error: " + message);
error_count_++;
}
}
static void CheckLongEq(long v1, long v2, String message)
{
if (v1 != v2)
{
Console.WriteLine("Error: " + v1 + " != " + v2 + " " + message);
error_count_++;
}
}
static IntegerVariableProto NewIntegerVariable(long lb, long ub) {
IntegerVariableProto var = new IntegerVariableProto();
var.Domain.Add(lb);
var.Domain.Add(ub);
return var;
}
static ConstraintProto NewLinear2(int v1, int v2,
long c1, long c2,
long lb, long ub) {
LinearConstraintProto linear = new LinearConstraintProto();
linear.Vars.Add(v1);
linear.Vars.Add(v2);
linear.Coeffs.Add(c1);
linear.Coeffs.Add(c2);
linear.Domain.Add(lb);
linear.Domain.Add(ub);
ConstraintProto ct = new ConstraintProto();
ct.Linear = linear;
return ct;
}
static ConstraintProto NewLinear3(int v1, int v2, int v3,
long c1, long c2, long c3,
long lb, long ub) {
LinearConstraintProto linear = new LinearConstraintProto();
linear.Vars.Add(v1);
linear.Vars.Add(v2);
linear.Vars.Add(v3);
linear.Coeffs.Add(c1);
linear.Coeffs.Add(c2);
linear.Coeffs.Add(c3);
linear.Domain.Add(lb);
linear.Domain.Add(ub);
ConstraintProto ct = new ConstraintProto();
ct.Linear = linear;
return ct;
}
static CpObjectiveProto NewMinimize1(int v1, long c1) {
CpObjectiveProto obj = new CpObjectiveProto();
obj.Vars.Add(v1);
obj.Coeffs.Add(c1);
return obj;
}
static CpObjectiveProto NewMaximize1(int v1, long c1) {
CpObjectiveProto obj = new CpObjectiveProto();
obj.Vars.Add(-v1 - 1);
obj.Coeffs.Add(c1);
obj.ScalingFactor = -1;
return obj;
}
static CpObjectiveProto NewMaximize2(int v1, int v2, long c1, long c2) {
CpObjectiveProto obj = new CpObjectiveProto();
obj.Vars.Add(-v1 - 1);
obj.Vars.Add(-v2 - 1);
obj.Coeffs.Add(c1);
obj.Coeffs.Add(c2);
obj.ScalingFactor = -1;
return obj;
}
static void TestSimpleLinearModel() {
CpModelProto model = new CpModelProto();
model.Variables.Add(NewIntegerVariable(-10, 10));
model.Variables.Add(NewIntegerVariable(-10, 10));
model.Variables.Add(NewIntegerVariable(-1000000, 1000000));
model.Constraints.Add(NewLinear2(0, 1 , 1, 1, -1000000, 100000));
model.Constraints.Add(NewLinear3(0, 1, 2, 1, 2, -1, 0, 100000));
model.Objective = NewMaximize1(2, 1);
CpSolverResponse response = SatHelper.Solve(model);
Console.WriteLine("model = " + model.ToString());
Console.WriteLine("response = " + response.ToString());
}
static void TestSimpleLinearModel2() {
CpModelProto model = new CpModelProto();
model.Variables.Add(NewIntegerVariable(-10, 10));
model.Variables.Add(NewIntegerVariable(-10, 10));
model.Constraints.Add(NewLinear2(0, 1 , 1, 1, -1000000, 100000));
model.Objective = NewMaximize2(0, 1, 1, -2);
CpSolverResponse response = SatHelper.Solve(model);
Console.WriteLine("model = " + model.ToString());
Console.WriteLine("response = " + response.ToString());
}
static void Main() {
TestSimpleLinearModel();
TestSimpleLinearModel2();
if (error_count_ != 0) {
Console.WriteLine("Found " + error_count_ + " errors.");
Environment.Exit(1);
}
}
}

35
makefiles/Makefile.csharp.mk
View File

@@ -106,6 +106,7 @@ clean_csharp:
-$(DEL) $(LIB_DIR)$S$(LIB_PREFIX)$(CLR_ORTOOLS_FZ_DLL_NAME).$(SWIG_LIB_SUFFIX)
-$(DEL) $(GEN_DIR)$Sortools$Slinear_solver$S*csharp_wrap*
-$(DEL) $(GEN_DIR)$Sortools$Sconstraint_solver$S*csharp_wrap*
-$(DEL) $(GEN_DIR)$Sortools$Ssat$S*csharp_wrap*
-$(DEL) $(GEN_DIR)$Sortools$Salgorithms$S*csharp_wrap*
-$(DEL) $(GEN_DIR)$Sortools$Sgraph$S*csharp_wrap*
-$(DEL) $(GEN_DIR)$Sortools$Sflatzinc$S*csharp_wrap*
@@ -113,6 +114,7 @@ clean_csharp:
-$(DEL) $(GEN_DIR)$Scom$Sgoogle$Sortools$Slinearsolver$S*.cs
-$(DEL) $(GEN_DIR)$Scom$Sgoogle$Sortools$Sconstraintsolver$S*.cs
-$(DEL) $(GEN_DIR)$Scom$Sgoogle$Sortools$Sknapsacksolver$S*.cs
-$(DEL) $(GEN_DIR)$Scom$Sgoogle$Sortools$Ssat$S*.cs
-$(DEL) $(GEN_DIR)$Scom$Sgoogle$Sortools$Sgraph$S*.cs
-$(DEL) $(GEN_DIR)$Scom$Sgoogle$Sortools$Sflatzinc$Sproperties$S*cs
-$(DEL) $(GEN_DIR)$Scom$Sgoogle$Sortools$Sflatzinc$S*.cs
@@ -205,6 +207,18 @@ $(GEN_DIR)/ortools/graph/graph_csharp_wrap.cc: \
$(OBJ_DIR)/swig/graph_csharp_wrap.$O: $(GEN_DIR)/ortools/graph/graph_csharp_wrap.cc
$(CCC) $(CFLAGS) -c $(GEN_DIR)$Sortools$Sgraph$Sgraph_csharp_wrap.cc $(OBJ_OUT)$(OBJ_DIR)$Sswig$Sgraph_csharp_wrap.$O
$(GEN_DIR)/ortools/sat/sat_csharp_wrap.cc: \
$(SRC_DIR)/ortools/base/base.i \
$(SRC_DIR)/ortools/sat/csharp/sat.i \
$(SRC_DIR)/ortools/sat/swig_helper.h \
$(SRC_DIR)/ortools/util/csharp/proto.i \
$(SAT_DEPS)
$(SWIG_BINARY) $(SWIG_INC) -I$(INC_DIR) -c++ -csharp -o $(GEN_DIR)$Sortools$Ssat$Ssat_csharp_wrap.cc -module operations_research_sat -namespace $(BASE_CLR_ORTOOLS_DLL_NAME).Sat -dllimport "$(CLR_ORTOOLS_DLL_NAME).$(SWIG_LIB_SUFFIX)" -outdir $(GEN_DIR)$Scom$Sgoogle$Sortools$Ssat $(SRC_DIR)$Sortools$Ssat$Scsharp$Ssat.i
$(OBJ_DIR)/swig/sat_csharp_wrap.$O: $(GEN_DIR)/ortools/sat/sat_csharp_wrap.cc
$(CCC) $(CFLAGS) -c $(GEN_DIR)/ortools/sat/sat_csharp_wrap.cc $(OBJ_OUT)$(OBJ_DIR)$Sswig$Ssat_csharp_wrap.$O
# Protobufs
$(GEN_DIR)/com/google/ortools/constraintsolver/SearchLimit.g.cs: $(SRC_DIR)/ortools/constraint_solver/search_limit.proto
@@ -222,6 +236,11 @@ $(GEN_DIR)/com/google/ortools/constraintsolver/RoutingParameters.g.cs: $(SRC_DIR
$(GEN_DIR)/com/google/ortools/constraintsolver/RoutingEnums.g.cs: $(SRC_DIR)/ortools/constraint_solver/routing_enums.proto
$(PROTOBUF_DIR)/bin/protoc --proto_path=$(SRC_DIR) --csharp_out=$(GEN_DIR)$Scom$Sgoogle$Sortools$Sconstraintsolver --csharp_opt=file_extension=.g.cs $(SRC_DIR)$Sortools$Sconstraint_solver$Srouting_enums.proto
$(GEN_DIR)/com/google/ortools/sat/CpModel.g.cs: $(SRC_DIR)/ortools/sat/cp_model.proto
$(PROTOBUF_DIR)/bin/protoc --proto_path=$(SRC_DIR) --csharp_out=$(GEN_DIR)$Scom$Sgoogle$Sortools$Ssat --csharp_opt=file_extension=.g.cs $(SRC_DIR)$Sortools$Ssat$Scp_model.proto
# Main DLL
$(CLR_KEYFILE):
@@ -234,6 +253,7 @@ $(BIN_DIR)/$(CLR_ORTOOLS_DLL_NAME)$(DLL): \
$(CLR_KEYFILE) \
$(BIN_DIR)/$(CLR_PROTOBUF_DLL_NAME)$(DLL) \
$(OBJ_DIR)/swig/linear_solver_csharp_wrap.$O \
$(OBJ_DIR)/swig/sat_csharp_wrap.$O \
$(OBJ_DIR)/swig/constraint_solver_csharp_wrap.$O \
$(OBJ_DIR)/swig/knapsack_solver_csharp_wrap.$O \
$(OBJ_DIR)/swig/graph_csharp_wrap.$O \
@@ -256,13 +276,14 @@ $(BIN_DIR)/$(CLR_ORTOOLS_DLL_NAME)$(DLL): \
$(GEN_DIR)/com/google/ortools/constraintsolver/SolverParameters.g.cs\
$(GEN_DIR)/com/google/ortools/constraintsolver/RoutingParameters.g.cs\
$(GEN_DIR)/com/google/ortools/constraintsolver/RoutingEnums.g.cs\
$(GEN_DIR)/com/google/ortools/sat/CpModel.g.cs \
$(OR_TOOLS_LIBS)
ifeq ($(SYSTEM),win)
$(CSC) /target:module /out:$(LIB_DIR)$S$(LIB_PREFIX)$(CLR_ORTOOLS_DLL_NAME).netmodule /lib:$(BIN_DIR) /r:$(CLR_PROTOBUF_DLL_NAME)$(DLL) /warn:0 /nologo /debug $(GEN_DIR)\\com\\google\\ortools\\linearsolver\\*.cs $(SRC_DIR)\\ortools\\com\\google\\ortools\\linearsolver\\*.cs $(GEN_DIR)\\com\\google\\ortools\\constraintsolver\\*.cs $(SRC_DIR)\\ortools\\com\\google\\ortools\\constraintsolver\\*.cs $(GEN_DIR)\\com\\google\\ortools\\algorithms\\*.cs $(SRC_DIR)\\ortools\\com\\google\\ortools\\algorithms\\*.cs $(GEN_DIR)\\com\\google\\ortools\\graph\\*.cs $(SRC_DIR)\\ortools\\com\\google\\ortools\\util\\*.cs $(GEN_DIR)\\com\\google\\ortools\\properties\\*.cs
$(DYNAMIC_LD) $(SIGNING_FLAGS) $(LDOUT)$(BIN_DIR)$S$(CLR_ORTOOLS_DLL_NAME)$(DLL) $(LIB_DIR)$S$(LIB_PREFIX)$(CLR_ORTOOLS_DLL_NAME).netmodule $(OBJ_DIR)$Sswig$Slinear_solver_csharp_wrap.$O $(OBJ_DIR)$Sswig$Sconstraint_solver_csharp_wrap.$O $(OBJ_DIR)$Sswig$Sknapsack_solver_csharp_wrap.$O $(OBJ_DIR)$Sswig$Sgraph_csharp_wrap.$O $(OR_TOOLS_LNK) $(OR_TOOLS_LD_FLAGS)
$(CSC) /target:module /out:$(LIB_DIR)$S$(LIB_PREFIX)$(CLR_ORTOOLS_DLL_NAME).netmodule /lib:$(BIN_DIR) /r:$(CLR_PROTOBUF_DLL_NAME)$(DLL) /warn:0 /nologo /debug $(GEN_DIR)\\com\\google\\ortools\\linearsolver\\*.cs $(GEN_DIR)\\com\\google\\ortools\\sat\\*.cs $(SRC_DIR)\\ortools\\com\\google\\ortools\\linearsolver\\*.cs $(GEN_DIR)\\com\\google\\ortools\\constraintsolver\\*.cs $(SRC_DIR)\\ortools\\com\\google\\ortools\\constraintsolver\\*.cs $(GEN_DIR)\\com\\google\\ortools\\algorithms\\*.cs $(SRC_DIR)\\ortools\\com\\google\\ortools\\algorithms\\*.cs $(GEN_DIR)\\com\\google\\ortools\\graph\\*.cs $(SRC_DIR)\\ortools\\com\\google\\ortools\\util\\*.cs $(GEN_DIR)\\com\\google\\ortools\\properties\\*.cs
$(DYNAMIC_LD) $(SIGNING_FLAGS) $(LDOUT)$(BIN_DIR)$S$(CLR_ORTOOLS_DLL_NAME)$(DLL) $(LIB_DIR)$S$(LIB_PREFIX)$(CLR_ORTOOLS_DLL_NAME).netmodule $(OBJ_DIR)$Sswig$Slinear_solver_csharp_wrap.$O $(OBJ_DIR)$Sswig$Ssat_csharp_wrap.$O $(OBJ_DIR)$Sswig$Sconstraint_solver_csharp_wrap.$O $(OBJ_DIR)$Sswig$Sknapsack_solver_csharp_wrap.$O $(OBJ_DIR)$Sswig$Sgraph_csharp_wrap.$O $(OR_TOOLS_LNK) $(OR_TOOLS_LD_FLAGS)
else
$(CSC) /target:library /out:$(BIN_DIR)/$(CLR_ORTOOLS_DLL_NAME)$(DLL) /lib:$(BIN_DIR) /r:$(CLR_PROTOBUF_DLL_NAME)$(DLL) /warn:0 /nologo /debug $(SRC_DIR)/ortools/com/google/ortools/util/*.cs $(GEN_DIR)/com/google/ortools/linearsolver/*.cs $(SRC_DIR)/ortools/com/google/ortools/linearsolver/*.cs $(GEN_DIR)/com/google/ortools/constraintsolver/*.cs $(SRC_DIR)/ortools/com/google/ortools/constraintsolver/*.cs $(SRC_DIR)/ortools/com/google/ortools/algorithms/*.cs $(GEN_DIR)/com/google/ortools/algorithms/*.cs $(GEN_DIR)/com/google/ortools/graph/*.cs $(GEN_DIR)/com/google/ortools/properties/*.cs
$(DYNAMIC_LD) $(LDOUT)$(LIB_DIR)$S$(LIB_PREFIX)$(CLR_ORTOOLS_DLL_NAME).$(SWIG_LIB_SUFFIX) $(OBJ_DIR)/swig/linear_solver_csharp_wrap.$O $(OBJ_DIR)/swig/constraint_solver_csharp_wrap.$O $(OBJ_DIR)/swig/knapsack_solver_csharp_wrap.$O $(OBJ_DIR)/swig/graph_csharp_wrap.$O $(OR_TOOLS_LNK) $(OR_TOOLS_LD_FLAGS)
$(CSC) /target:library /out:$(BIN_DIR)/$(CLR_ORTOOLS_DLL_NAME)$(DLL) /lib:$(BIN_DIR) /r:$(CLR_PROTOBUF_DLL_NAME)$(DLL) /warn:0 /nologo /debug $(SRC_DIR)/ortools/com/google/ortools/util/*.cs $(GEN_DIR)/com/google/ortools/linearsolver/*.cs $(SRC_DIR)/ortools/com/google/ortools/linearsolver/*.cs $(GEN_DIR)/com/google/ortools/sat/*.cs $(GEN_DIR)/com/google/ortools/constraintsolver/*.cs $(SRC_DIR)/ortools/com/google/ortools/constraintsolver/*.cs $(SRC_DIR)/ortools/com/google/ortools/algorithms/*.cs $(GEN_DIR)/com/google/ortools/algorithms/*.cs $(GEN_DIR)/com/google/ortools/graph/*.cs $(GEN_DIR)/com/google/ortools/properties/*.cs
$(DYNAMIC_LD) $(LDOUT)$(LIB_DIR)$S$(LIB_PREFIX)$(CLR_ORTOOLS_DLL_NAME).$(SWIG_LIB_SUFFIX) $(OBJ_DIR)/swig/linear_solver_csharp_wrap.$O $(OBJ_DIR)/swig/sat_csharp_wrap.$O $(OBJ_DIR)/swig/constraint_solver_csharp_wrap.$O $(OBJ_DIR)/swig/knapsack_solver_csharp_wrap.$O $(OBJ_DIR)/swig/graph_csharp_wrap.$O $(OR_TOOLS_LNK) $(OR_TOOLS_LD_FLAGS)
endif
# csharp linear solver examples
@@ -314,6 +335,12 @@ $(BIN_DIR)/testcp$(CLR_EXE_SUFFIX).exe: $(BIN_DIR)/$(CLR_ORTOOLS_DLL_NAME)$(DLL)
testcp: $(BIN_DIR)/testcp$(CLR_EXE_SUFFIX).exe
$(MONO) $(BIN_DIR)$Stestcp$(CLR_EXE_SUFFIX).exe
$(BIN_DIR)/testsat$(CLR_EXE_SUFFIX).exe: $(BIN_DIR)/$(CLR_ORTOOLS_DLL_NAME)$(DLL) $(EX_DIR)/tests/testsat.cs
$(CSC) $(SIGNING_FLAGS) /target:exe /out:$(BIN_DIR)$Stestsat$(CLR_EXE_SUFFIX).exe /platform:$(NETPLATFORM) /lib:$(BIN_DIR) /r:$(CLR_ORTOOLS_DLL_NAME)$(DLL) /r:$(CLR_PROTOBUF_DLL_NAME)$(DLL) $(EX_DIR)$Stests$Stestsat.cs
testsat: $(BIN_DIR)/testsat$(CLR_EXE_SUFFIX).exe
$(MONO) $(BIN_DIR)$Stestsat$(CLR_EXE_SUFFIX).exe
$(BIN_DIR)/issue18$(CLR_EXE_SUFFIX).exe: $(BIN_DIR)/$(CLR_ORTOOLS_DLL_NAME)$(DLL) $(EX_DIR)/tests/issue18.cs
$(CSC) $(SIGNING_FLAGS) /target:exe /out:$(BIN_DIR)$Sissue18$(CLR_EXE_SUFFIX).exe /platform:$(NETPLATFORM) /lib:$(BIN_DIR) /r:$(CLR_ORTOOLS_DLL_NAME)$(DLL) /r:$(CLR_PROTOBUF_DLL_NAME)$(DLL) $(EX_DIR)$Stests$Sissue18.cs

4
makefiles/Makefile.third_party.unix.mk
View File

@@ -40,6 +40,7 @@ MISSING_DIRECTORIES = \
ortools/gen/com/google/ortools/constraintsolver \
ortools/gen/com/google/ortools/flatzinc \
ortools/gen/com/google/ortools/graph \
ortools/gen/com/google/ortools/sat \
ortools/gen/com/google/ortools/linearsolver \
ortools/gen/com/google/ortools/properties \
ortools/gen/ortools/algorithms \
@@ -121,6 +122,9 @@ ortools/gen/com/google/ortools/linearsolver:
ortools/gen/com/google/ortools/flatzinc:
$(MKDIR_P) ortools$Sgen$Scom$Sgoogle$Sortools$Sflatzinc
ortools/gen/com/google/ortools/sat:
$(MKDIR_P) ortools$Sgen$Scom$Sgoogle$Sortools$Ssat
ortools/gen/com/google/ortools/properties:
$(MKDIR_P) ortools$Sgen$Scom$Sgoogle$Sortools$Sproperties

2
ortools/sat/cp_model.proto
View File

@@ -14,6 +14,8 @@
// Proto describing a general Constraint Programming (CP) problem.
syntax = "proto3";
option csharp_namespace = "Google.OrTools.Sat";
package operations_research.sat;

2
ortools/sat/integer.h
View File

@@ -140,7 +140,7 @@ struct IntegerLiteral {
std::string DebugString() const {
return VariableIsPositive(var)
? StrCat("I", var.value() / 2, ">=", bound.value())
: StrCat("I", var.value() / 2, "<=", bound.value());
: StrCat("I", var.value() / 2, "<=", -bound.value());
}
// Note that bound should be in [kMinIntegerValue, kMaxIntegerValue + 1].

76
ortools/sat/optimization.cc
View File

@@ -29,6 +29,7 @@
#include "ortools/base/macros.h"
#include "ortools/base/stringprintf.h"
#include "ortools/base/timer.h"
#include "ortools/base/join.h"
#include "ortools/base/int_type.h"
#include "ortools/base/map_util.h"
#if defined(USE_CBC) || defined(USE_SCIP)
@@ -1209,15 +1210,14 @@ SatSolver::Status MinimizeWithCoreAndLazyEncoding(
feasible_solution_observer(*model);
}
// TODO(user): Investigate if constraining the objective is better.
if (/* DISABLES CODE */ (false)) {
sat_solver->Backtrack(0);
sat_solver->SetAssumptionLevel(0);
if (!integer_trail->Enqueue(
IntegerLiteral::LowerOrEqual(objective_var, objective - 1), {},
{})) {
return false;
}
// Constrain objective_var. This has a better result when objective_var is
// used in an LP relaxation for instance.
sat_solver->Backtrack(0);
sat_solver->SetAssumptionLevel(0);
if (!integer_trail->Enqueue(
IntegerLiteral::LowerOrEqual(objective_var, objective - 1), {},
{})) {
return false;
}
return true;
};
@@ -1263,10 +1263,11 @@ SatSolver::Status MinimizeWithCoreAndLazyEncoding(
sat_solver->SetAssumptionLevel(0);
// We assumes all terms at their lower-bound.
std::vector<Literal> assumptions;
assumption_to_term_index.clear();
std::vector<int> term_indices;
std::vector<IntegerLiteral> integer_assumptions;
IntegerValue next_stratified_threshold(0);
IntegerValue implied_objective_lb;
IntegerValue implied_objective_lb(0);
IntegerValue objective_offset(0);
for (int i = 0; i < terms.size(); ++i) {
const ObjectiveTerm term = terms[i];
const IntegerValue var_lb = integer_trail->LowerBound(term.var);
@@ -1279,16 +1280,19 @@ SatSolver::Status MinimizeWithCoreAndLazyEncoding(
// Skip fixed terms.
// We still keep them around for a proper lower-bound computation.
// TODO(user): we could keep an objective offset instead.
if (var_lb == integer_trail->UpperBound(term.var)) continue;
if (var_lb == integer_trail->UpperBound(term.var)) {
objective_offset += term.weight * var_lb.value();
continue;
}
// Only consider the terms above the threshold.
if (term.weight < stratified_threshold) {
next_stratified_threshold =
std::max(next_stratified_threshold, term.weight);
} else {
assumptions.push_back(integer_encoder->GetOrCreateAssociatedLiteral(
IntegerLiteral::LowerOrEqual(term.var, var_lb)));
InsertOrDie(&assumption_to_term_index, assumptions.back().Index(), i);
integer_assumptions.push_back(
IntegerLiteral::LowerOrEqual(term.var, var_lb));
term_indices.push_back(i);
}
}
@@ -1304,21 +1308,37 @@ SatSolver::Status MinimizeWithCoreAndLazyEncoding(
}
// No assumptions with the current stratified_threshold? use the new one.
if (assumptions.empty() && next_stratified_threshold > 0) {
if (term_indices.empty() && next_stratified_threshold > 0) {
stratified_threshold = next_stratified_threshold;
--iter; // "false" iteration, the lower bound does not increase.
continue;
}
// If there is only one assumptions left, we switch the algorithm.
if (term_indices.size() == 1 && next_stratified_threshold == 0) {
if (log_info) LOG(INFO) << "Switching to linear scan...";
model->Add(LowerOrEqualWithOffset(
terms[term_indices[0]].var, objective_var, objective_offset.value()));
result = MinimizeIntegerVariableWithLinearScanAndLazyEncoding(
false, objective_var, next_decision, feasible_solution_observer,
model);
break;
}
// Display the progress.
const IntegerValue objective_lb = integer_trail->LowerBound(objective_var);
if (log_info) {
LOG(INFO) << StringPrintf(
" iter:%d lb:%lld (%lld) gap:%lld assumptions:%zu strat:%lld "
"depth:%d",
iter, objective_lb.value(), implied_objective_lb.value(),
(best_objective - objective_lb).value(), assumptions.size(),
stratified_threshold.value(), max_depth);
const int64 lb = objective_lb.value();
const int64 ub = best_objective.value();
const int gap = lb == ub ? 0
: static_cast<int>(std::ceil(100.0 * (ub - lb) /
std::max(ub, lb)));
LOG(INFO) << StrCat("unscaled_objective:[", lb, ",", ub,
"]"
" gap:",
gap, "%", " assumptions:", term_indices.size(),
" strat:", stratified_threshold.value(),
" depth:", max_depth);
}
// Abort if we have a solution and a gap of zero.
@@ -1327,6 +1347,16 @@ SatSolver::Status MinimizeWithCoreAndLazyEncoding(
break;
}
// Convert integer_assumptions to Literals.
std::vector<Literal> assumptions;
assumption_to_term_index.clear();
for (int i = 0; i < integer_assumptions.size(); ++i) {
assumptions.push_back(integer_encoder->GetOrCreateAssociatedLiteral(
integer_assumptions[i]));
InsertOrDie(&assumption_to_term_index, assumptions.back().Index(),
term_indices[i]);
}
// Solve under the assumptions.
std::vector<std::vector<Literal>> cores;
result = FindCores(assumptions, next_decision, model, &cores);

51
ortools/sat/swig_helper.h Normal file
View File

@@ -0,0 +1,51 @@
// Copyright 2010-2014 Google
// 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.
#ifndef OR_TOOLS_SAT_SWIG_HELPER_H_
#define OR_TOOLS_SAT_SWIG_HELPER_H_
#include "ortools/sat/cp_model.pb.h"
#include "ortools/sat/cp_model_solver.h"
#include "ortools/sat/model.h"
#include "ortools/sat/sat_parameters.pb.h"
namespace operations_research {
namespace sat {
class SatHelper {
public:
// The arguments of the functions defined below must follow these rules
// to be wrapped by swig correctly:
// 1) Their types must include the full operations_research::sat::
// namespace.
// 2) Their names must correspond to the ones declared in the .i
// file (see the python/ and java/ subdirectories).
static operations_research::sat::CpSolverResponse Solve(
const operations_research::sat::CpModelProto& model_proto) {
Model model;
return operations_research::sat::SolveCpModel(model_proto, &model);
}
static operations_research::sat::CpSolverResponse SolveWithParameters(
const operations_research::sat::CpModelProto& model_proto,
const operations_research::sat::SatParameters& parameters) {
Model model;
model.Add(NewSatParameters(parameters));
return SolveCpModel(model_proto, &model);
}
};
} // namespace sat
} // namespace operations_research
#endif // OR_TOOLS_SAT_SWIG_HELPER_H_