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

fix circuit presolve; polish sat cookbook; fix bug with optional intervals sharing the same boolean

Browse Source
This commit is contained in:
Laurent Perron
2018-09-05 11:54:28 +02:00
parent 36393a1733
commit 466b2ee0e7
9 changed files with 88 additions and 67 deletions
Download Patch File Download Diff File Expand all files Collapse all files

80
ortools/sat/cp_model_presolve.cc
View File

@@ -210,11 +210,19 @@ struct PresolveContext {
is_unsat = true;
return;
}
bool added = false;
if (RefIsPositive(ref_a) == RefIsPositive(ref_b)) {
affine_relations.TryAdd(PositiveRef(ref_a), PositiveRef(ref_b), 1, 0);
var_equiv_relations.TryAdd(PositiveRef(ref_a), PositiveRef(ref_b), 1, 0);
added |=
affine_relations.TryAdd(PositiveRef(ref_a), PositiveRef(ref_b), 1, 0);
added |= var_equiv_relations.TryAdd(PositiveRef(ref_a),
PositiveRef(ref_b), 1, 0);
} else {
affine_relations.TryAdd(PositiveRef(ref_a), PositiveRef(ref_b), -1, 1);
added |= affine_relations.TryAdd(PositiveRef(ref_a), PositiveRef(ref_b),
-1, 1);
}
if (added) {
modified_domains.Set(PositiveRef(ref_a));
modified_domains.Set(PositiveRef(ref_b));
}
}
@@ -1410,8 +1418,8 @@ bool PresolveCircuit(ConstraintProto* ct, PresolveContext* context) {
}
int num_fixed_at_true = 0;
for (const auto& node_to_refs : {incoming_arcs, outgoing_arcs}) {
for (const std::vector<int>& refs : node_to_refs) {
for (const auto* node_to_refs : {&incoming_arcs, &outgoing_arcs}) {
for (const std::vector<int>& refs : *node_to_refs) {
if (refs.size() == 1) {
if (!context->LiteralIsTrue(refs.front())) {
++num_fixed_at_true;
@@ -1472,46 +1480,6 @@ bool PresolveCircuit(ConstraintProto* ct, PresolveContext* context) {
++new_size;
}
// Look for in/out-degree of two, this will imply that one of the indicator
// Boolean is equal to the negation of the other.
for (int i = 0; i < num_nodes; ++i) {
if (new_in_degree[i] == 2) {
std::vector<int> literals;
for (const int ref : incoming_arcs[i]) {
if (context->LiteralIsFalse(ref)) continue;
if (context->LiteralIsTrue(ref)) {
literals.clear();
break;
}
literals.push_back(ref);
}
if (literals.size() == 2) {
if (PositiveRef(literals[0]) != PositiveRef(literals[1])) {
context->UpdateRuleStats("circuit: degree 2");
}
context->AddBooleanEqualityRelation(literals[0],
NegatedRef(literals[1]));
}
}
if (new_out_degree[i] == 2) {
std::vector<int> literals;
for (const int ref : outgoing_arcs[i]) {
if (context->LiteralIsFalse(ref)) continue;
if (context->LiteralIsTrue(ref)) {
literals.clear();
break;
}
}
if (literals.size() == 2) {
if (PositiveRef(literals[0]) != PositiveRef(literals[1])) {
context->UpdateRuleStats("circuit: degree 2");
}
context->AddBooleanEqualityRelation(literals[0],
NegatedRef(literals[1]));
}
}
}
// Detect infeasibility due to a node having no more incoming or outgoing arc.
// This is a bit tricky because for now the meaning of the constraint says
// that all nodes that appear in at least one of the arcs must be in the
@@ -1558,6 +1526,28 @@ bool PresolveCircuit(ConstraintProto* ct, PresolveContext* context) {
}
}
// Look for in/out-degree of two, this will imply that one of the indicator
// Boolean is equal to the negation of the other.
for (int i = 0; i < num_nodes; ++i) {
for (const std::vector<int>* arc_literals :
{&incoming_arcs[i], &outgoing_arcs[i]}) {
std::vector<int> literals;
for (const int ref : *arc_literals) {
if (context->LiteralIsFalse(ref)) continue;
if (context->LiteralIsTrue(ref)) {
literals.clear();
break;
}
literals.push_back(ref);
}
if (literals.size() == 2 && literals[0] != NegatedRef(literals[1])) {
context->UpdateRuleStats("circuit: degree 2");
context->AddBooleanEqualityRelation(literals[0],
NegatedRef(literals[1]));
}
}
}
// Truncate the circuit and return.
if (new_size < num_arcs) {
proto.mutable_tails()->Truncate(new_size);

2
ortools/sat/cp_model_utils.cc
View File

@@ -72,7 +72,7 @@ void AddReferencesUsedByConstraint(const ConstraintProto& ct,
AddIndices(ct.element().vars(), &output->variables);
break;
case ConstraintProto::ConstraintCase::kCircuit:
AddIndices(ct.circuit().literals(), &output->variables);
AddIndices(ct.circuit().literals(), &output->literals);
break;
case ConstraintProto::ConstraintCase::kRoutes:
AddIndices(ct.routes().literals(), &output->literals);

20
ortools/sat/csharp/sat.i
View File

@@ -52,28 +52,38 @@ PROTO2_RETURN(
%unignore operations_research::sat::SatHelper;
%unignore operations_research::sat::SatHelper::Solve;
%unignore operations_research::sat::SatHelper::SolveWithStringParameters;
// We use the director version of the API.
%unignore operations_research::sat::SatHelper::SolveWithStringParametersAndSolutionCallback;
// --------- Include the swig helpers file to create the director classes ------
// We cannot use %ignoreall/%unignoreall as this is not compatible with nested
// swig files.
%feature("director") operations_research::sat::SolutionCallback;
%unignore operations_research::sat::SolutionCallback;
%unignore operations_research::sat::SolutionCallback::SolutionCallback;
%unignore operations_research::sat::SolutionCallback::~SolutionCallback;
%unignore operations_research::sat::SolutionCallback::NumBinaryPropagations;
%feature("nodirector") operations_research::sat::SolutionCallback::NumBinaryPropagations;
%unignore operations_research::sat::SolutionCallback::NumBooleans;
%feature("nodirector") operations_research::sat::SolutionCallback::NumBooleans;
%unignore operations_research::sat::SolutionCallback::NumBranches;
%feature("nodirector") operations_research::sat::SolutionCallback::NumBooleans;
%unignore operations_research::sat::SolutionCallback::NumConflicts;
%feature("nodirector") operations_research::sat::SolutionCallback::NumConflicts;
%unignore operations_research::sat::SolutionCallback::NumIntegerPropagations;
%feature("nodirector") operations_research::sat::SolutionCallback::NumIntegerPropagations;
%unignore operations_research::sat::SolutionCallback::ObjectiveValue;
%feature("nodirector") operations_research::sat::SolutionCallback::ObjectiveValue;
%unignore operations_research::sat::SolutionCallback::OnSolutionCallback;
%unignore operations_research::sat::SolutionCallback::Response;
%feature("nodirector") operations_research::sat::SolutionCallback::Response;
%unignore operations_research::sat::SolutionCallback::SolutionBooleanValue;
%feature("nodirector") operations_research::sat::SolutionCallback::SolutionBooleanValue;
%unignore operations_research::sat::SolutionCallback::SolutionIntegerValue;
%feature("nodirector") operations_research::sat::SolutionCallback::SolutionIntegerValue;
%unignore operations_research::sat::SolutionCallback::StopSearch;
%feature("nodirector") operations_research::sat::SolutionCallback::StopSearch;
%unignore operations_research::sat::SolutionCallback::UserTime;
%feature("nodirector") operations_research::sat::SolutionCallback::UserTime;
%unignore operations_research::sat::SolutionCallback::WallTime;
%feature("nodirector") operations_research::sat::SolutionCallback::WallTime;
%include "ortools/sat/swig_helper.h"

6
ortools/sat/disjunctive.cc
View File

@@ -366,7 +366,11 @@ bool DisjunctiveOverloadChecker::Propagate() {
helper_->AddStartMinReason(optional_task, window_start);
helper_->AddEndMaxReason(optional_task, window_end);
helper_->PushTaskAbsence(optional_task); // This never fails.
// If tasks shares the same presence literal, it is possible that we
// already pushed this task absence.
if (!helper_->IsAbsent(optional_task)) {
helper_->PushTaskAbsence(optional_task); // This never fails.
}
theta_tree_.RemoveEvent(optional_event);
}
}

32
ortools/sat/doc/solver.md
View File

@@ -918,10 +918,12 @@ public class CodeSamplesSat
Sometimes, one can decide that the current solution is good enough.
In this section, we will take the previous model, but only ask for the
first 5 solutions of the model.
first 5 solutions of the model.
### Python code
Stopping search is performed by calling CpSolverSolutionCallback.StopSearch()
when called on a solution.
```python
"""Code sample that solves a model and displays a small number of solutions."""
@@ -980,14 +982,18 @@ StopAfterNSolutions()
### C++ code
To search for all solution, a parameter of the sat solver must be changed.
Stopping search is done by registering an atomic bool on the model-owned time
limit, and setting this one to true.
```cpp
#include <atomic>
#include "ortools/sat/cp_model.pb.h"
#include "ortools/sat/cp_model_solver.h"
#include "ortools/sat/cp_model_utils.h"
#include "ortools/sat/model.h"
#include "ortools/sat/sat_parameters.pb.h"
#include "ortools/util/time_limit.h"
namespace operations_research {
namespace sat {
@@ -1032,9 +1038,8 @@ void StopAfterNSolutions() {
model.Add(NewSatParameters(parameters));
// Create an atomic Boolean that will be periodically checked by the limit.
std::atomic<bool> stopped;
model.GetOrCreate<TimeLimit>()->RegisterExternalBooleanAsLimit(
&stopped);
std::atomic<bool> stopped(false);
model.GetOrCreate<TimeLimit>()->RegisterExternalBooleanAsLimit(&stopped);
const int kSolutionLimit = 5;
int num_solutions = 0;
@@ -1065,6 +1070,9 @@ int main() {
### Java code
Stopping search is performed by calling CpSolverSolutionCallback.stopSearch()
when called on a solution.
```java
import com.google.ortools.sat.CpModel;
import com.google.ortools.sat.CpSolver;
@@ -1075,8 +1083,8 @@ public class StopAfterNSolutions {
static { System.loadLibrary("jniortools"); }
static class VarArraySolutionPrinter extends CpSolverSolutionCallback {
public VarArraySolutionPrinter(IntVar[] variables, int limit) {
static class VarArraySolutionPrinterWithLimit extends CpSolverSolutionCallback {
public VarArraySolutionPrinterWithLimit(IntVar[] variables, int limit) {
variableArray = variables;
solutionLimit = limit;
}
@@ -1117,7 +1125,8 @@ public class StopAfterNSolutions {
// Create a solver and solve the model.
CpSolver solver = new CpSolver();
VarArraySolutionPrinter cb = new VarArraySolutionPrinter(new IntVar[] {x, y, z}, 5);
VarArraySolutionPrinterWithLimit cb =
new VarArraySolutionPrinterWithLimit(new IntVar[] {x, y, z}, 5);
solver.searchAllSolutions(model, cb);
System.out.println(cb.getSolutionCount() + " solutions found.");
@@ -1127,12 +1136,17 @@ public class StopAfterNSolutions {
### C\# code
Stopping search is performed by calling CpSolverSolutionCallback.StopSearch()
when called on a solution.
```cs
using System;
using Google.OrTools.Sat;
public class VarArraySolutionPrinterWithLimit : CpSolverSolutionCallback {
public VarArraySolutionPrinter(IntVar[] variables, int solution_limit) {
public VarArraySolutionPrinterWithLimit(IntVar[] variables,
int solution_limit) {
variables_ = variables;
solution_limit_ = solution_limit;
}

1
ortools/sat/precedences.cc
View File

@@ -742,6 +742,7 @@ void PrecedencesPropagator::AddGreaterThanAtLeastOneOfConstraints(
// TODO(user): Find more than one disjoint set of incoming arcs.
// TODO(user): call MinimizeCoreWithPropagation() on the clause.
solver->Backtrack(0);
if (solver->IsModelUnsat()) return;
std::vector<Literal> clause;
for (const ArcIndex arc_index : incoming_arcs_[target]) {
const Literal literal = arcs_[arc_index].presence_literals.front();

7
ortools/sat/samples/StopAfterNSolutions.java
View File

@@ -20,8 +20,8 @@ public class StopAfterNSolutions {
static { System.loadLibrary("jniortools"); }
static class VarArraySolutionPrinter extends CpSolverSolutionCallback {
public VarArraySolutionPrinter(IntVar[] variables, int limit) {
static class VarArraySolutionPrinterWithLimit extends CpSolverSolutionCallback {
public VarArraySolutionPrinterWithLimit(IntVar[] variables, int limit) {
variableArray = variables;
solutionLimit = limit;
}
@@ -62,7 +62,8 @@ public class StopAfterNSolutions {
// Create a solver and solve the model.
CpSolver solver = new CpSolver();
VarArraySolutionPrinter cb = new VarArraySolutionPrinter(new IntVar[] {x, y, z}, 5);
VarArraySolutionPrinterWithLimit cb =
new VarArraySolutionPrinterWithLimit(new IntVar[] {x, y, z}, 5);
solver.searchAllSolutions(model, cb);
System.out.println(cb.getSolutionCount() + " solutions found.");

6
ortools/sat/samples/stop_after_n_solutions.cc
View File

@@ -11,6 +11,7 @@
// See the License for the specific language governing permissions and
// limitations under the License.
#include <atomic>
#include "ortools/sat/cp_model.pb.h"
#include "ortools/sat/cp_model_solver.h"
@@ -62,9 +63,8 @@ void StopAfterNSolutions() {
model.Add(NewSatParameters(parameters));
// Create an atomic Boolean that will be periodically checked by the limit.
std::atomic<bool> stopped;
model.GetOrCreate<TimeLimit>()->RegisterExternalBooleanAsLimit(
&stopped);
std::atomic<bool> stopped(false);
model.GetOrCreate<TimeLimit>()->RegisterExternalBooleanAsLimit(&stopped);
const int kSolutionLimit = 5;
int num_solutions = 0;

1
ortools/sat/samples/stop_after_n_solutions.cs
View File

@@ -11,6 +11,7 @@
// See the License for the specific language governing permissions and
// limitations under the License.
using System;
using Google.OrTools.Sat;