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

change CP-SAT internals

Browse Source
This commit is contained in:
Laurent Perron
2019-04-01 13:27:21 +02:00
parent f8eb8bb5db
commit ee89733a60
8 changed files with 122 additions and 131 deletions
Download Patch File Download Diff File Expand all files Collapse all files

68
makefiles/Makefile.gen.mk
View File

@@ -166,8 +166,7 @@ objs/util/cached_log.$O: ortools/util/cached_log.cc \
objs/util/file_util.$O: ortools/util/file_util.cc ortools/util/file_util.h \
ortools/base/file.h ortools/base/integral_types.h ortools/base/logging.h \
ortools/base/macros.h ortools/base/status.h ortools/base/recordio.h \
ortools/base/statusor.h | $(OBJ_DIR)/util
ortools/base/macros.h ortools/base/status.h ortools/base/recordio.h | $(OBJ_DIR)/util
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sortools$Sutil$Sfile_util.cc $(OBJ_OUT)$(OBJ_DIR)$Sutil$Sfile_util.$O
objs/util/fp_utils.$O: ortools/util/fp_utils.cc ortools/util/fp_utils.h \
@@ -481,7 +480,7 @@ objs/lp_data/model_reader.$O: ortools/lp_data/model_reader.cc \
ortools/util/fp_utils.h ortools/base/file.h ortools/base/status.h \
ortools/lp_data/mps_reader.h ortools/base/commandlineflags.h \
ortools/base/map_util.h ortools/lp_data/proto_utils.h \
ortools/util/file_util.h ortools/base/recordio.h ortools/base/statusor.h | $(OBJ_DIR)/lp_data
ortools/util/file_util.h ortools/base/recordio.h | $(OBJ_DIR)/lp_data
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sortools$Slp_data$Smodel_reader.cc $(OBJ_OUT)$(OBJ_DIR)$Slp_data$Smodel_reader.$O
objs/lp_data/mps_reader.$O: ortools/lp_data/mps_reader.cc \
@@ -667,8 +666,7 @@ objs/glop/lp_solver.$O: ortools/glop/lp_solver.cc ortools/glop/lp_solver.h \
ortools/lp_data/matrix_scaler.h ortools/lp_data/proto_utils.h \
ortools/gen/ortools/linear_solver/linear_solver.pb.h \
ortools/gen/ortools/util/optional_boolean.pb.h ortools/util/file_util.h \
ortools/base/file.h ortools/base/status.h ortools/base/recordio.h \
ortools/base/statusor.h | $(OBJ_DIR)/glop
ortools/base/file.h ortools/base/status.h ortools/base/recordio.h | $(OBJ_DIR)/glop
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sortools$Sglop$Slp_solver.cc $(OBJ_OUT)$(OBJ_DIR)$Sglop$Slp_solver.$O
objs/glop/lu_factorization.$O: ortools/glop/lu_factorization.cc \
@@ -1198,8 +1196,8 @@ objs/sat/boolean_problem.$O: ortools/sat/boolean_problem.cc \
ortools/base/int_type.h ortools/base/status.h \
ortools/gen/ortools/sat/boolean_problem.pb.h \
ortools/gen/ortools/sat/cp_model.pb.h ortools/sat/pb_constraint.h \
ortools/base/hash.h ortools/base/basictypes.h ortools/sat/sat_base.h \
ortools/sat/model.h ortools/base/map_util.h ortools/base/typeid.h \
ortools/base/hash.h ortools/base/basictypes.h ortools/sat/model.h \
ortools/base/map_util.h ortools/base/typeid.h ortools/sat/sat_base.h \
ortools/util/bitset.h ortools/gen/ortools/sat/sat_parameters.pb.h \
ortools/util/stats.h ortools/base/timer.h ortools/sat/sat_solver.h \
ortools/sat/clause.h ortools/sat/drat_proof_handler.h \
@@ -1550,7 +1548,7 @@ objs/sat/diffn.$O: ortools/sat/diffn.cc ortools/sat/diffn.h \
ortools/sat/intervals.h ortools/sat/cp_constraints.h \
ortools/sat/integer_expr.h ortools/sat/precedences.h \
ortools/sat/theta_tree.h ortools/base/iterator_adaptors.h \
ortools/sat/cumulative.h ortools/util/sort.h | $(OBJ_DIR)/sat
ortools/base/stl_util.h ortools/sat/cumulative.h ortools/util/sort.h | $(OBJ_DIR)/sat
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sortools$Ssat$Sdiffn.cc $(OBJ_OUT)$(OBJ_DIR)$Ssat$Sdiffn.$O
objs/sat/disjunctive.$O: ortools/sat/disjunctive.cc \
@@ -1572,7 +1570,7 @@ objs/sat/disjunctive.$O: ortools/sat/disjunctive.cc \
ortools/sat/intervals.h ortools/sat/cp_constraints.h \
ortools/sat/integer_expr.h ortools/sat/precedences.h \
ortools/sat/theta_tree.h ortools/base/iterator_adaptors.h \
ortools/sat/all_different.h | $(OBJ_DIR)/sat
ortools/sat/all_different.h ortools/util/sort.h | $(OBJ_DIR)/sat
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sortools$Ssat$Sdisjunctive.cc $(OBJ_OUT)$(OBJ_DIR)$Ssat$Sdisjunctive.$O
objs/sat/drat_checker.$O: ortools/sat/drat_checker.cc \
@@ -1608,8 +1606,8 @@ objs/sat/encoding.$O: ortools/sat/encoding.cc ortools/sat/encoding.h \
ortools/base/integral_types.h ortools/base/logging.h \
ortools/gen/ortools/sat/boolean_problem.pb.h ortools/sat/pb_constraint.h \
ortools/base/hash.h ortools/base/basictypes.h \
ortools/base/int_type_indexed_vector.h ortools/sat/sat_base.h \
ortools/sat/model.h ortools/base/map_util.h ortools/base/typeid.h \
ortools/base/int_type_indexed_vector.h ortools/sat/model.h \
ortools/base/map_util.h ortools/base/typeid.h ortools/sat/sat_base.h \
ortools/util/bitset.h ortools/gen/ortools/sat/sat_parameters.pb.h \
ortools/util/stats.h ortools/base/timer.h ortools/sat/sat_solver.h \
ortools/sat/clause.h ortools/sat/drat_proof_handler.h \
@@ -1925,8 +1923,8 @@ objs/sat/pb_constraint.$O: ortools/sat/pb_constraint.cc \
ortools/sat/pb_constraint.h ortools/base/hash.h \
ortools/base/basictypes.h ortools/base/integral_types.h \
ortools/base/logging.h ortools/base/macros.h ortools/base/int_type.h \
ortools/base/int_type_indexed_vector.h ortools/sat/sat_base.h \
ortools/sat/model.h ortools/base/map_util.h ortools/base/typeid.h \
ortools/base/int_type_indexed_vector.h ortools/sat/model.h \
ortools/base/map_util.h ortools/base/typeid.h ortools/sat/sat_base.h \
ortools/util/bitset.h ortools/gen/ortools/sat/sat_parameters.pb.h \
ortools/util/stats.h ortools/base/timer.h ortools/base/thorough_hash.h \
ortools/util/saturated_arithmetic.h | $(OBJ_DIR)/sat
@@ -2241,8 +2239,8 @@ objs/bop/bop_base.$O: ortools/bop/bop_base.cc ortools/bop/bop_base.h \
ortools/algorithms/sparse_permutation.h ortools/base/status.h \
ortools/gen/ortools/sat/boolean_problem.pb.h \
ortools/gen/ortools/sat/cp_model.pb.h ortools/sat/pb_constraint.h \
ortools/base/hash.h ortools/sat/sat_base.h ortools/sat/model.h \
ortools/base/map_util.h ortools/base/typeid.h ortools/util/bitset.h \
ortools/base/hash.h ortools/sat/model.h ortools/base/map_util.h \
ortools/base/typeid.h ortools/sat/sat_base.h ortools/util/bitset.h \
ortools/gen/ortools/sat/sat_parameters.pb.h ortools/util/stats.h \
ortools/base/timer.h ortools/sat/sat_solver.h ortools/sat/clause.h \
ortools/sat/drat_proof_handler.h ortools/sat/drat_checker.h \
@@ -2263,8 +2261,8 @@ objs/bop/bop_fs.$O: ortools/bop/bop_fs.cc ortools/bop/bop_fs.h \
ortools/sat/boolean_problem.h ortools/algorithms/sparse_permutation.h \
ortools/base/status.h ortools/gen/ortools/sat/boolean_problem.pb.h \
ortools/gen/ortools/sat/cp_model.pb.h ortools/sat/pb_constraint.h \
ortools/base/hash.h ortools/sat/sat_base.h ortools/sat/model.h \
ortools/base/map_util.h ortools/base/typeid.h ortools/util/bitset.h \
ortools/base/hash.h ortools/sat/model.h ortools/base/map_util.h \
ortools/base/typeid.h ortools/sat/sat_base.h ortools/util/bitset.h \
ortools/gen/ortools/sat/sat_parameters.pb.h ortools/util/stats.h \
ortools/base/timer.h ortools/sat/sat_solver.h ortools/sat/clause.h \
ortools/sat/drat_proof_handler.h ortools/sat/drat_checker.h \
@@ -2304,8 +2302,8 @@ objs/bop/bop_lns.$O: ortools/bop/bop_lns.cc ortools/bop/bop_lns.h \
ortools/sat/boolean_problem.h ortools/algorithms/sparse_permutation.h \
ortools/base/status.h ortools/gen/ortools/sat/boolean_problem.pb.h \
ortools/gen/ortools/sat/cp_model.pb.h ortools/sat/pb_constraint.h \
ortools/base/hash.h ortools/sat/sat_base.h ortools/sat/model.h \
ortools/base/map_util.h ortools/base/typeid.h ortools/util/bitset.h \
ortools/base/hash.h ortools/sat/model.h ortools/base/map_util.h \
ortools/base/typeid.h ortools/sat/sat_base.h ortools/util/bitset.h \
ortools/gen/ortools/sat/sat_parameters.pb.h ortools/util/stats.h \
ortools/base/timer.h ortools/sat/sat_solver.h ortools/sat/clause.h \
ortools/sat/drat_proof_handler.h ortools/sat/drat_checker.h \
@@ -2345,8 +2343,8 @@ objs/bop/bop_ls.$O: ortools/bop/bop_ls.cc ortools/bop/bop_ls.h \
ortools/algorithms/sparse_permutation.h ortools/base/status.h \
ortools/gen/ortools/sat/boolean_problem.pb.h \
ortools/gen/ortools/sat/cp_model.pb.h ortools/sat/pb_constraint.h \
ortools/sat/sat_base.h ortools/sat/model.h ortools/base/map_util.h \
ortools/base/typeid.h ortools/util/bitset.h \
ortools/sat/model.h ortools/base/map_util.h ortools/base/typeid.h \
ortools/sat/sat_base.h ortools/util/bitset.h \
ortools/gen/ortools/sat/sat_parameters.pb.h ortools/util/stats.h \
ortools/base/timer.h ortools/sat/sat_solver.h ortools/sat/clause.h \
ortools/sat/drat_proof_handler.h ortools/sat/drat_checker.h \
@@ -2369,8 +2367,8 @@ objs/bop/bop_portfolio.$O: ortools/bop/bop_portfolio.cc \
ortools/algorithms/sparse_permutation.h ortools/base/status.h \
ortools/gen/ortools/sat/boolean_problem.pb.h \
ortools/gen/ortools/sat/cp_model.pb.h ortools/sat/pb_constraint.h \
ortools/base/hash.h ortools/sat/sat_base.h ortools/sat/model.h \
ortools/base/map_util.h ortools/base/typeid.h ortools/util/bitset.h \
ortools/base/hash.h ortools/sat/model.h ortools/base/map_util.h \
ortools/base/typeid.h ortools/sat/sat_base.h ortools/util/bitset.h \
ortools/gen/ortools/sat/sat_parameters.pb.h ortools/util/stats.h \
ortools/base/timer.h ortools/sat/sat_solver.h ortools/sat/clause.h \
ortools/sat/drat_proof_handler.h ortools/sat/drat_checker.h \
@@ -2408,8 +2406,8 @@ objs/bop/bop_solution.$O: ortools/bop/bop_solution.cc \
ortools/algorithms/sparse_permutation.h ortools/base/status.h \
ortools/gen/ortools/sat/boolean_problem.pb.h \
ortools/gen/ortools/sat/cp_model.pb.h ortools/sat/pb_constraint.h \
ortools/base/hash.h ortools/sat/sat_base.h ortools/sat/model.h \
ortools/base/map_util.h ortools/base/typeid.h ortools/util/bitset.h \
ortools/base/hash.h ortools/sat/model.h ortools/base/map_util.h \
ortools/base/typeid.h ortools/sat/sat_base.h ortools/util/bitset.h \
ortools/gen/ortools/sat/sat_parameters.pb.h ortools/util/stats.h \
ortools/base/timer.h ortools/sat/sat_solver.h ortools/sat/clause.h \
ortools/sat/drat_proof_handler.h ortools/sat/drat_checker.h \
@@ -2430,8 +2428,8 @@ objs/bop/bop_solver.$O: ortools/bop/bop_solver.cc ortools/bop/bop_solver.h \
ortools/algorithms/sparse_permutation.h ortools/base/status.h \
ortools/gen/ortools/sat/boolean_problem.pb.h \
ortools/gen/ortools/sat/cp_model.pb.h ortools/sat/pb_constraint.h \
ortools/base/hash.h ortools/sat/sat_base.h ortools/sat/model.h \
ortools/base/map_util.h ortools/base/typeid.h ortools/util/bitset.h \
ortools/base/hash.h ortools/sat/model.h ortools/base/map_util.h \
ortools/base/typeid.h ortools/sat/sat_base.h ortools/util/bitset.h \
ortools/gen/ortools/sat/sat_parameters.pb.h ortools/util/stats.h \
ortools/base/timer.h ortools/sat/sat_solver.h ortools/sat/clause.h \
ortools/sat/drat_proof_handler.h ortools/sat/drat_checker.h \
@@ -2473,8 +2471,8 @@ objs/bop/bop_util.$O: ortools/bop/bop_util.cc ortools/bop/bop_util.h \
ortools/algorithms/sparse_permutation.h ortools/base/status.h \
ortools/gen/ortools/sat/boolean_problem.pb.h \
ortools/gen/ortools/sat/cp_model.pb.h ortools/sat/pb_constraint.h \
ortools/base/hash.h ortools/sat/sat_base.h ortools/sat/model.h \
ortools/base/map_util.h ortools/base/typeid.h ortools/util/bitset.h \
ortools/base/hash.h ortools/sat/model.h ortools/base/map_util.h \
ortools/base/typeid.h ortools/sat/sat_base.h ortools/util/bitset.h \
ortools/gen/ortools/sat/sat_parameters.pb.h ortools/util/stats.h \
ortools/base/timer.h ortools/sat/sat_solver.h ortools/sat/clause.h \
ortools/sat/drat_proof_handler.h ortools/sat/drat_checker.h \
@@ -2496,8 +2494,8 @@ objs/bop/complete_optimizer.$O: ortools/bop/complete_optimizer.cc \
ortools/algorithms/sparse_permutation.h ortools/base/status.h \
ortools/gen/ortools/sat/boolean_problem.pb.h \
ortools/gen/ortools/sat/cp_model.pb.h ortools/sat/pb_constraint.h \
ortools/base/hash.h ortools/sat/sat_base.h ortools/sat/model.h \
ortools/base/map_util.h ortools/base/typeid.h ortools/util/bitset.h \
ortools/base/hash.h ortools/sat/model.h ortools/base/map_util.h \
ortools/base/typeid.h ortools/sat/sat_base.h ortools/util/bitset.h \
ortools/gen/ortools/sat/sat_parameters.pb.h ortools/util/stats.h \
ortools/base/timer.h ortools/sat/sat_solver.h ortools/sat/clause.h \
ortools/sat/drat_proof_handler.h ortools/sat/drat_checker.h \
@@ -2532,8 +2530,8 @@ objs/bop/integral_solver.$O: ortools/bop/integral_solver.cc \
ortools/algorithms/sparse_permutation.h ortools/base/status.h \
ortools/gen/ortools/sat/boolean_problem.pb.h \
ortools/gen/ortools/sat/cp_model.pb.h ortools/sat/pb_constraint.h \
ortools/sat/sat_base.h ortools/sat/model.h ortools/base/map_util.h \
ortools/base/typeid.h ortools/gen/ortools/sat/sat_parameters.pb.h \
ortools/sat/model.h ortools/base/map_util.h ortools/base/typeid.h \
ortools/sat/sat_base.h ortools/gen/ortools/sat/sat_parameters.pb.h \
ortools/util/stats.h ortools/sat/sat_solver.h ortools/sat/clause.h \
ortools/sat/drat_proof_handler.h ortools/sat/drat_checker.h \
ortools/sat/drat_writer.h ortools/base/file.h \
@@ -3445,8 +3443,8 @@ objs/constraint_solver/search.$O: ortools/constraint_solver/search.cc \
ortools/base/bitmap.h ortools/base/basictypes.h \
ortools/base/integral_types.h ortools/base/logging.h \
ortools/base/macros.h ortools/base/commandlineflags.h \
ortools/base/hash.h ortools/base/map_util.h ortools/base/random.h \
ortools/base/stl_util.h ortools/base/timer.h \
ortools/base/hash.h ortools/base/map_util.h ortools/base/mathutil.h \
ortools/base/random.h ortools/base/stl_util.h ortools/base/timer.h \
ortools/constraint_solver/constraint_solver.h ortools/base/sysinfo.h \
ortools/gen/ortools/constraint_solver/solver_parameters.pb.h \
ortools/util/piecewise_linear_function.h \

7
ortools/sat/clause.cc
View File

@@ -48,13 +48,14 @@ void RemoveIf(Container c, Predicate p) {
// ----- LiteralWatchers -----
LiteralWatchers::LiteralWatchers()
LiteralWatchers::LiteralWatchers(Model* model)
: SatPropagator("LiteralWatchers"),
is_clean_(true),
num_inspected_clauses_(0),
num_inspected_clause_literals_(0),
num_watched_clauses_(0),
stats_("LiteralWatchers") {}
stats_("LiteralWatchers") {
model->GetOrCreate<Trail>()->RegisterPropagator(this);
}
LiteralWatchers::~LiteralWatchers() {
gtl::STLDeleteElements(&clauses_);

4
ortools/sat/clause.h
View File

@@ -151,7 +151,7 @@ struct ClauseInfo {
// information.
class LiteralWatchers : public SatPropagator {
public:
LiteralWatchers();
explicit LiteralWatchers(Model* model);
~LiteralWatchers() override;
// Must be called before adding clauses refering to such variables.
@@ -289,7 +289,7 @@ class LiteralWatchers : public SatPropagator {
// Indicates if the corresponding watchers_on_false_ list need to be
// cleaned. The boolean is_clean_ is just used in DCHECKs.
SparseBitset<LiteralIndex> needs_cleaning_;
bool is_clean_;
bool is_clean_ = true;
int64 num_inspected_clauses_;
int64 num_inspected_clause_literals_;

2
ortools/sat/doc/navbar.md
View File

@@ -5,5 +5,5 @@
- [integer arithmetic](integer_arithmetic.md)
- [channeling constraints](channeling.md)
- [scheduling](scheduling.md)
- [Using the CP-SAT solver](solver.md)
- [solving a model](solver.md)
- [Reference manual for the CpModel and CpSolver classes](reference.md)

8
ortools/sat/pb_constraint.cc
View File

@@ -986,10 +986,10 @@ UpperBoundedLinearConstraint* PbConstraints::ReasonPbConstraint(
void PbConstraints::ComputeNewLearnedConstraintLimit() {
const int num_constraints = constraints_.size();
target_number_of_learned_constraint_ =
num_constraints + parameters_.pb_cleanup_increment();
num_constraints + parameters_->pb_cleanup_increment();
num_learned_constraint_before_cleanup_ =
static_cast<int>(target_number_of_learned_constraint_ /
parameters_.pb_cleanup_ratio()) -
parameters_->pb_cleanup_ratio()) -
num_constraints;
}
@@ -1065,7 +1065,7 @@ void PbConstraints::DeleteSomeLearnedConstraintIfNeeded() {
void PbConstraints::BumpActivity(UpperBoundedLinearConstraint* constraint) {
if (!constraint->is_learned()) return;
const double max_activity = parameters_.max_clause_activity_value();
const double max_activity = parameters_->max_clause_activity_value();
constraint->set_activity(constraint->activity() +
constraint_activity_increment_);
if (constraint->activity() > max_activity) {
@@ -1081,7 +1081,7 @@ void PbConstraints::RescaleActivities(double scaling_factor) {
}
void PbConstraints::UpdateActivityIncrement() {
const double decay = parameters_.clause_activity_decay();
const double decay = parameters_->clause_activity_decay();
constraint_activity_increment_ *= 1.0 / decay;
}

15
ortools/sat/pb_constraint.h
View File

@@ -28,6 +28,7 @@
#include "ortools/base/integral_types.h"
#include "ortools/base/logging.h"
#include "ortools/base/macros.h"
#include "ortools/sat/model.h"
#include "ortools/sat/sat_base.h"
#include "ortools/sat/sat_parameters.pb.h"
#include "ortools/util/bitset.h"
@@ -514,15 +515,18 @@ class UpperBoundedLinearConstraint {
// propagation.
class PbConstraints : public SatPropagator {
public:
PbConstraints()
explicit PbConstraints(Model* model)
: SatPropagator("PbConstraints"),
conflicting_constraint_index_(-1),
num_learned_constraint_before_cleanup_(0),
constraint_activity_increment_(1.0),
parameters_(model->GetOrCreate<SatParameters>()),
stats_("PbConstraints"),
num_constraint_lookups_(0),
num_inspected_constraint_literals_(0),
num_threshold_updates_(0) {}
num_threshold_updates_(0) {
model->GetOrCreate<Trail>()->RegisterPropagator(this);
}
~PbConstraints() override {
IF_STATS_ENABLED({
LOG(INFO) << stats_.StatString();
@@ -547,11 +551,6 @@ class PbConstraints : public SatPropagator {
}
}
// Parameter management.
void SetParameters(const SatParameters& parameters) {
parameters_ = parameters;
}
// Adds a constraint in canonical form to the set of managed constraints. Note
// that this detects constraints with exactly the same terms. In this case,
// the constraint rhs is updated if the new one is lower or nothing is done
@@ -669,7 +668,7 @@ class PbConstraints : public SatPropagator {
double constraint_activity_increment_;
// Algorithm parameters.
SatParameters parameters_;
SatParameters* parameters_;
// Some statistics.
mutable StatsGroup stats_;

137
ortools/sat/sat_solver.cc
View File

@@ -39,6 +39,8 @@ SatSolver::SatSolver() : SatSolver(new Model()) { owned_model_.reset(model_); }
SatSolver::SatSolver(Model* model)
: model_(model),
binary_implication_graph_(model->GetOrCreate<BinaryImplicationGraph>()),
clauses_propagator_(model->GetOrCreate<LiteralWatchers>()),
pb_constraints_(model->GetOrCreate<PbConstraints>()),
track_binary_clauses_(false),
trail_(model->GetOrCreate<Trail>()),
time_limit_(model->GetOrCreate<TimeLimit>()),
@@ -51,14 +53,7 @@ SatSolver::SatSolver(Model* model)
problem_is_pure_sat_(true),
drat_proof_handler_(nullptr),
stats_("SatSolver") {
// TODO(user): move these 2 classes in the Model so that everyone can access
// them if needed and we don't have the wiring here.
trail_->RegisterPropagator(&clauses_propagator_);
trail_->RegisterPropagator(&pb_constraints_);
InitializePropagators();
// TODO(user): use the model parameters directly in pb_constraints_.
pb_constraints_.SetParameters(*parameters_);
}
SatSolver::~SatSolver() { IF_STATS_ENABLED(LOG(INFO) << stats_.StatString()); }
@@ -70,10 +65,10 @@ void SatSolver::SetNumVariables(int num_variables) {
num_variables_ = num_variables;
binary_implication_graph_->Resize(num_variables);
clauses_propagator_.Resize(num_variables);
clauses_propagator_->Resize(num_variables);
trail_->Resize(num_variables);
decision_policy_->IncreaseNumVariables(num_variables);
pb_constraints_.Resize(num_variables);
pb_constraints_->Resize(num_variables);
same_reason_identifier_.Resize(num_variables);
// The +1 is a bit tricky, it is because in
@@ -99,13 +94,13 @@ double SatSolver::deterministic_time() const {
// guess.
return 1e-8 * (8.0 * trail_->NumberOfEnqueues() +
1.0 * binary_implication_graph_->num_inspections() +
4.0 * clauses_propagator_.num_inspected_clauses() +
1.0 * clauses_propagator_.num_inspected_clause_literals() +
4.0 * clauses_propagator_->num_inspected_clauses() +
1.0 * clauses_propagator_->num_inspected_clause_literals() +
// Here there is a factor 2 because of the untrail.
20.0 * pb_constraints_.num_constraint_lookups() +
2.0 * pb_constraints_.num_threshold_updates() +
1.0 * pb_constraints_.num_inspected_constraint_literals());
20.0 * pb_constraints_->num_constraint_lookups() +
2.0 * pb_constraints_->num_threshold_updates() +
1.0 * pb_constraints_->num_inspected_constraint_literals());
}
const SatParameters& SatSolver::parameters() const {
@@ -116,8 +111,6 @@ const SatParameters& SatSolver::parameters() const {
void SatSolver::SetParameters(const SatParameters& parameters) {
SCOPED_TIME_STAT(&stats_);
*parameters_ = parameters;
pb_constraints_.SetParameters(parameters);
restart_->Reset();
time_limit_->ResetLimitFromParameters(parameters);
}
@@ -212,7 +205,7 @@ bool SatSolver::AddProblemClauseInternal(const std::vector<Literal>& literals) {
if (parameters_->treat_binary_clauses_separately() && literals.size() == 2) {
AddBinaryClauseInternal(literals[0], literals[1]);
} else {
if (!clauses_propagator_.AddClause(literals, trail_)) {
if (!clauses_propagator_->AddClause(literals, trail_)) {
return SetModelUnsat();
}
}
@@ -272,7 +265,7 @@ bool SatSolver::AddLinearConstraintInternal(
// TODO(user): If this constraint forces all its literal to false (when rhs is
// zero for instance), we still add it. Optimize this?
const bool result = pb_constraints_.AddConstraint(cst, rhs, trail_);
const bool result = pb_constraints_->AddConstraint(cst, rhs, trail_);
InitializePropagators();
return result;
}
@@ -364,14 +357,14 @@ int SatSolver::AddLearnedClauseAndEnqueueUnitPropagation(
--num_learned_clause_before_cleanup_;
SatClause* clause =
clauses_propagator_.AddRemovableClause(literals, trail_);
clauses_propagator_->AddRemovableClause(literals, trail_);
// BumpClauseActivity() must be called after clauses_info_[clause] has
// been created or it will have no effect.
(*clauses_propagator_.mutable_clauses_info())[clause].lbd = lbd;
(*clauses_propagator_->mutable_clauses_info())[clause].lbd = lbd;
BumpClauseActivity(clause);
} else {
CHECK(clauses_propagator_.AddClause(literals, trail_));
CHECK(clauses_propagator_->AddClause(literals, trail_));
}
return lbd;
}
@@ -398,8 +391,8 @@ UpperBoundedLinearConstraint* SatSolver::ReasonPbConstraintOrNull(
// It is important to deal properly with "SameReasonAs" variables here.
var = trail_->ReferenceVarWithSameReason(var);
const AssignmentInfo& info = trail_->Info(var);
if (trail_->AssignmentType(var) == pb_constraints_.PropagatorId()) {
return pb_constraints_.ReasonPbConstraint(info.trail_index);
if (trail_->AssignmentType(var) == pb_constraints_->PropagatorId()) {
return pb_constraints_->ReasonPbConstraint(info.trail_index);
}
return nullptr;
}
@@ -407,8 +400,8 @@ UpperBoundedLinearConstraint* SatSolver::ReasonPbConstraintOrNull(
SatClause* SatSolver::ReasonClauseOrNull(BooleanVariable var) const {
DCHECK(trail_->Assignment().VariableIsAssigned(var));
const AssignmentInfo& info = trail_->Info(var);
if (trail_->AssignmentType(var) == clauses_propagator_.PropagatorId()) {
return clauses_propagator_.ReasonClause(info.trail_index);
if (trail_->AssignmentType(var) == clauses_propagator_->PropagatorId()) {
return clauses_propagator_->ReasonClause(info.trail_index);
}
return nullptr;
}
@@ -571,7 +564,7 @@ bool SatSolver::PropagateAndStopAfterOneConflictResolution() {
// Decay the activities.
decision_policy_->UpdateVariableActivityIncrement();
UpdateClauseActivityIncrement();
pb_constraints_.UpdateActivityIncrement();
pb_constraints_->UpdateActivityIncrement();
// Hack from Glucose that seems to perform well.
const int period = parameters_->glucose_decay_increment_period();
@@ -588,7 +581,7 @@ bool SatSolver::PropagateAndStopAfterOneConflictResolution() {
// in its resolution were clauses.
bool compute_pb_conflict = false;
if (parameters_->use_pb_resolution()) {
compute_pb_conflict = (pb_constraints_.ConflictingConstraint() != nullptr);
compute_pb_conflict = (pb_constraints_->ConflictingConstraint() != nullptr);
if (!compute_pb_conflict) {
for (Literal lit : reason_used_to_infer_the_conflict_) {
if (ReasonPbConstraintOrNull(lit.Variable()) != nullptr) {
@@ -604,7 +597,7 @@ bool SatSolver::PropagateAndStopAfterOneConflictResolution() {
if (compute_pb_conflict) {
pb_conflict_.ClearAndResize(num_variables_.value());
Coefficient initial_slack(-1);
if (pb_constraints_.ConflictingConstraint() == nullptr) {
if (pb_constraints_->ConflictingConstraint() == nullptr) {
// Generic clause case.
Coefficient num_literals(0);
for (Literal literal : trail_->FailingClause()) {
@@ -614,8 +607,8 @@ bool SatSolver::PropagateAndStopAfterOneConflictResolution() {
pb_conflict_.AddToRhs(num_literals - 1);
} else {
// We have a pseudo-Boolean conflict, so we start from there.
pb_constraints_.ConflictingConstraint()->AddToConflict(&pb_conflict_);
pb_constraints_.ClearConflictingConstraint();
pb_constraints_->ConflictingConstraint()->AddToConflict(&pb_conflict_);
pb_constraints_->ClearConflictingConstraint();
initial_slack =
pb_conflict_.ComputeSlackForTrailPrefix(*trail_, max_trail_index + 1);
}
@@ -646,11 +639,11 @@ bool SatSolver::PropagateAndStopAfterOneConflictResolution() {
// Use the PB conflict.
// Note that we don't need to call InitializePropagators() since when we
// are here, we are sure we have at least one pb constraint.
DCHECK_GT(pb_constraints_.NumberOfConstraints(), 0);
DCHECK_GT(pb_constraints_->NumberOfConstraints(), 0);
CHECK_LT(pb_backjump_level, CurrentDecisionLevel());
Backtrack(pb_backjump_level);
CHECK(pb_constraints_.AddLearnedConstraint(cst, pb_conflict_.Rhs(),
trail_));
CHECK(pb_constraints_->AddLearnedConstraint(cst, pb_conflict_.Rhs(),
trail_));
CHECK_GT(trail_->Index(), last_decision_or_backtrack_trail_index_);
counters_.num_learned_pb_literals += cst.size();
return false;
@@ -753,12 +746,12 @@ bool SatSolver::PropagateAndStopAfterOneConflictResolution() {
parameters_->subsumption_during_conflict_analysis()) {
for (SatClause* clause : subsumed_clauses_) {
DCHECK(ClauseSubsumption(learned_conflict_, clause));
if (!clauses_propagator_.IsRemovable(clause)) {
if (!clauses_propagator_->IsRemovable(clause)) {
is_redundant = false;
}
clauses_propagator_.LazyDetach(clause);
clauses_propagator_->LazyDetach(clause);
}
clauses_propagator_.CleanUpWatchers();
clauses_propagator_->CleanUpWatchers();
counters_.num_subsumed_clauses += subsumed_clauses_.size();
}
@@ -939,7 +932,7 @@ void SatSolver::KeepAllClauseUsedToInfer(BooleanVariable variable) {
const BooleanVariable var = (*trail_)[trail_index].Variable();
SatClause* clause = ReasonClauseOrNull(var);
if (clause != nullptr) {
clauses_propagator_.mutable_clauses_info()->erase(clause);
clauses_propagator_->mutable_clauses_info()->erase(clause);
}
for (const Literal l : trail_->Reason(var)) {
const AssignmentInfo& info = trail_->Info(l.Variable());
@@ -981,7 +974,7 @@ void SatSolver::TryToMinimizeClause(SatClause* clause) {
counters_.minimization_num_true++;
counters_.minimization_num_removed_literals += clause->Size();
Backtrack(0);
clauses_propagator_.Detach(clause);
clauses_propagator_->Detach(clause);
return;
}
@@ -996,7 +989,7 @@ void SatSolver::TryToMinimizeClause(SatClause* clause) {
// TODO(user): do not do that if it make us keep too many clauses?
KeepAllClauseUsedToInfer(literal.Variable());
Backtrack(0);
clauses_propagator_.Detach(clause);
clauses_propagator_->Detach(clause);
return;
} else {
// Simplify. Note(user): we could only keep in clause the literals
@@ -1045,7 +1038,7 @@ void SatSolver::TryToMinimizeClause(SatClause* clause) {
if (parameters_->treat_binary_clauses_separately() && candidate.size() == 2) {
counters_.minimization_num_removed_literals += clause->Size() - 2;
AddBinaryClauseInternal(candidate[0], candidate[1]);
clauses_propagator_.Detach(clause);
clauses_propagator_->Detach(clause);
// This is needed in the corner case where this was the first binary clause
// of the problem so that PropagationIsDone() returns true on the newly
@@ -1059,9 +1052,9 @@ void SatSolver::TryToMinimizeClause(SatClause* clause) {
// TODO(user): If the watched literal didn't change, we could just rewrite
// the clause while keeping the two watched literals at the beginning.
clauses_propagator_.Detach(clause);
clauses_propagator_->Detach(clause);
clause->Rewrite(candidate);
clauses_propagator_.Attach(clause, trail_);
clauses_propagator_->Attach(clause, trail_);
}
SatSolver::Status SatSolver::SolveInternal(TimeLimit* time_limit) {
@@ -1078,14 +1071,14 @@ SatSolver::Status SatSolver::SolveInternal(TimeLimit* time_limit) {
LOG(INFO) << "Initial memory usage: " << MemoryUsage();
LOG(INFO) << "Number of variables: " << num_variables_;
LOG(INFO) << "Number of clauses (size > 2): "
<< clauses_propagator_.num_clauses();
<< clauses_propagator_->num_clauses();
LOG(INFO) << "Number of binary clauses: "
<< binary_implication_graph_->NumberOfImplications();
LOG(INFO) << "Number of linear constraints: "
<< pb_constraints_.NumberOfConstraints();
<< pb_constraints_->NumberOfConstraints();
LOG(INFO) << "Number of fixed variables: " << trail_->Index();
LOG(INFO) << "Number of watched clauses: "
<< clauses_propagator_.num_watched_clauses();
<< clauses_propagator_->num_watched_clauses();
LOG(INFO) << "Parameters: " << ProtobufShortDebugString(*parameters_);
}
@@ -1201,21 +1194,21 @@ void SatSolver::MinimizeSomeClauses(int decisions_budget) {
const int64 target_num_branches = counters_.num_branches + decisions_budget;
while (counters_.num_branches < target_num_branches &&
(time_limit_ == nullptr || !time_limit_->LimitReached())) {
SatClause* to_minimize = clauses_propagator_.NextClauseToMinimize();
SatClause* to_minimize = clauses_propagator_->NextClauseToMinimize();
if (to_minimize != nullptr) {
TryToMinimizeClause(to_minimize);
if (is_model_unsat_) return;
} else {
if (to_minimize == nullptr) {
VLOG(1) << "Minimized all clauses, restarting from first one.";
clauses_propagator_.ResetToMinimizeIndex();
clauses_propagator_->ResetToMinimizeIndex();
}
break;
}
}
block_clause_deletion_ = false;
clauses_propagator_.DeleteDetachedClauses();
clauses_propagator_->DeleteDetachedClauses();
}
std::vector<Literal> SatSolver::GetLastIncompatibleDecisions() {
@@ -1295,7 +1288,7 @@ void SatSolver::BumpReasonActivities(const std::vector<Literal>& literals) {
if (pb_constraint != nullptr) {
// TODO(user): Because one pb constraint may propagate many literals,
// this may bias the constraint activity... investigate other policy.
pb_constraints_.BumpActivity(pb_constraint);
pb_constraints_->BumpActivity(pb_constraint);
}
}
}
@@ -1307,15 +1300,15 @@ void SatSolver::BumpClauseActivity(SatClause* clause) {
// that we will keep a clause forever, we don't need to create its Info. More
// than the speed, this allows to limit as much as possible the activity
// rescaling.
auto it = clauses_propagator_.mutable_clauses_info()->find(clause);
if (it == clauses_propagator_.mutable_clauses_info()->end()) return;
auto it = clauses_propagator_->mutable_clauses_info()->find(clause);
if (it == clauses_propagator_->mutable_clauses_info()->end()) return;
// Check if the new clause LBD is below our threshold to keep this clause
// indefinitely. Note that we use a +1 here because the LBD of a newly learned
// clause decrease by 1 just after the backjump.
const int new_lbd = ComputeLbd(*clause);
if (new_lbd + 1 <= parameters_->clause_cleanup_lbd_bound()) {
clauses_propagator_.mutable_clauses_info()->erase(clause);
clauses_propagator_->mutable_clauses_info()->erase(clause);
return;
}
@@ -1347,7 +1340,7 @@ void SatSolver::BumpClauseActivity(SatClause* clause) {
void SatSolver::RescaleClauseActivities(double scaling_factor) {
SCOPED_TIME_STAT(&stats_);
clause_activity_increment_ *= scaling_factor;
for (auto& entry : *clauses_propagator_.mutable_clauses_info()) {
for (auto& entry : *clauses_propagator_->mutable_clauses_info()) {
entry.second.activity *= scaling_factor;
}
}
@@ -1442,9 +1435,9 @@ std::string SatSolver::StatusString(Status status) const {
binary_implication_graph_->num_minimization(),
binary_implication_graph_->num_literals_removed()) +
absl::StrFormat(" num inspected clauses: %d\n",
clauses_propagator_.num_inspected_clauses()) +
clauses_propagator_->num_inspected_clauses()) +
absl::StrFormat(" num inspected clause_literals: %d\n",
clauses_propagator_.num_inspected_clause_literals()) +
clauses_propagator_->num_inspected_clause_literals()) +
absl::StrFormat(
" num learned literals: %d (avg: %.1f /clause)\n",
counters_.num_literals_learned,
@@ -1466,11 +1459,11 @@ std::string SatSolver::StatusString(Status status) const {
absl::StrFormat(" minimization_num_removed_literals: %d\n",
counters_.minimization_num_removed_literals) +
absl::StrFormat(" pb num threshold updates: %d\n",
pb_constraints_.num_threshold_updates()) +
pb_constraints_->num_threshold_updates()) +
absl::StrFormat(" pb num constraint lookups: %d\n",
pb_constraints_.num_constraint_lookups()) +
pb_constraints_->num_constraint_lookups()) +
absl::StrFormat(" pb num inspected constraint literals: %d\n",
pb_constraints_.num_inspected_constraint_literals()) +
pb_constraints_->num_inspected_constraint_literals()) +
restart_->InfoString() +
absl::StrFormat(" deterministic time: %f\n", deterministic_time());
}
@@ -1481,9 +1474,9 @@ std::string SatSolver::RunningStatisticsString() const {
"%6.2fs, mem:%s, fails:%d, depth:%d, clauses:%d, tmp:%d, bin:%u, "
"restarts:%d, vars:%d",
time_in_s, MemoryUsage(), counters_.num_failures, CurrentDecisionLevel(),
clauses_propagator_.num_clauses() -
clauses_propagator_.num_removable_clauses(),
clauses_propagator_.num_removable_clauses(),
clauses_propagator_->num_clauses() -
clauses_propagator_->num_removable_clauses(),
clauses_propagator_->num_removable_clauses(),
binary_implication_graph_->NumberOfImplications(),
restart_->NumRestarts(),
num_variables_.value() - num_processed_fixed_variables_);
@@ -1522,13 +1515,13 @@ void SatSolver::ProcessNewlyFixedVariables() {
// We remove the clauses that are always true and the fixed literals from the
// others. Note that none of the clause should be all false because we should
// have detected a conflict before this is called.
for (SatClause* clause : clauses_propagator_.AllClausesInCreationOrder()) {
for (SatClause* clause : clauses_propagator_->AllClausesInCreationOrder()) {
if (!clause->IsAttached()) continue;
const size_t old_size = clause->Size();
if (clause->RemoveFixedLiteralsAndTestIfTrue(trail_->Assignment())) {
// The clause is always true, detach it.
clauses_propagator_.LazyDetach(clause);
clauses_propagator_->LazyDetach(clause);
++num_detached_clauses;
continue;
}
@@ -1547,14 +1540,14 @@ void SatSolver::ProcessNewlyFixedVariables() {
// it is safe to do that because this clause can't be used as a reason
// since we are at level zero and the clause is not satisfied.
AddBinaryClauseInternal(clause->FirstLiteral(), clause->SecondLiteral());
clauses_propagator_.LazyDetach(clause);
clauses_propagator_->LazyDetach(clause);
++num_binary;
continue;
}
}
// Note that we will only delete the clauses during the next database cleanup.
clauses_propagator_.CleanUpWatchers();
clauses_propagator_->CleanUpWatchers();
if (num_detached_clauses > 0 || num_binary > 0) {
VLOG(1) << trail_->Index() << " fixed variables at level 0. "
<< "Detached " << num_detached_clauses << " clauses. " << num_binary
@@ -1604,9 +1597,9 @@ void SatSolver::InitializePropagators() {
if (binary_implication_graph_->NumberOfImplications() > 0) {
propagators_.push_back(binary_implication_graph_);
}
propagators_.push_back(&clauses_propagator_);
if (pb_constraints_.NumberOfConstraints() > 0) {
propagators_.push_back(&pb_constraints_);
propagators_.push_back(clauses_propagator_);
if (pb_constraints_->NumberOfConstraints() > 0) {
propagators_.push_back(pb_constraints_);
}
for (int i = 0; i < external_propagators_.size(); ++i) {
propagators_.push_back(external_propagators_[i]);
@@ -2408,7 +2401,7 @@ void SatSolver::CleanClauseDatabaseIfNeeded() {
// that appear in clauses_info can potentially be removed.
typedef std::pair<SatClause*, ClauseInfo> Entry;
std::vector<Entry> entries;
auto& clauses_info = *clauses_propagator_.mutable_clauses_info();
auto& clauses_info = *(clauses_propagator_->mutable_clauses_info());
for (auto& entry : clauses_info) {
if (ClauseIsUsedAsReason(entry.first)) continue;
if (entry.second.protected_during_next_cleanup) {
@@ -2459,14 +2452,14 @@ void SatSolver::CleanClauseDatabaseIfNeeded() {
for (const Entry& entry : entries) {
SatClause* clause = entry.first;
counters_.num_literals_forgotten += clause->Size();
clauses_propagator_.LazyDetach(clause);
clauses_propagator_->LazyDetach(clause);
}
clauses_propagator_.CleanUpWatchers();
clauses_propagator_->CleanUpWatchers();
// TODO(user): If the need arise, we could avoid this linear scan on the
// full list of clauses by not keeping the clauses from clauses_info there.
if (!block_clause_deletion_) {
clauses_propagator_.DeleteDetachedClauses();
clauses_propagator_->DeleteDetachedClauses();
}
}

12
ortools/sat/sat_solver.h
View File

@@ -320,13 +320,13 @@ class SatSolver {
if (num_processed_fixed_variables_ < trail_->Index()) {
ProcessNewlyFixedVariables();
}
clauses_propagator_.DeleteDetachedClauses();
clauses_propagator_->DeleteDetachedClauses();
// Note(user): Putting the binary clauses first help because the presolver
// currently process the clauses in order.
binary_implication_graph_->ExtractAllBinaryClauses(out);
for (SatClause* clause : clauses_propagator_.AllClausesInCreationOrder()) {
if (!clauses_propagator_.IsRemovable(clause)) {
for (SatClause* clause : clauses_propagator_->AllClausesInCreationOrder()) {
if (!clauses_propagator_->IsRemovable(clause)) {
out->AddClause(clause->AsSpan());
}
}
@@ -375,7 +375,7 @@ class SatSolver {
void SetDratProofHandler(DratProofHandler* drat_proof_handler) {
drat_proof_handler_ = drat_proof_handler;
clauses_propagator_.SetDratProofHandler(drat_proof_handler_);
clauses_propagator_->SetDratProofHandler(drat_proof_handler_);
}
// This function is here to deal with the case where a SAT/CP model is found
@@ -674,8 +674,8 @@ class SatSolver {
// Internal propagators. We keep them here because we need more than the
// SatPropagator interface for them.
BinaryImplicationGraph* binary_implication_graph_;
LiteralWatchers clauses_propagator_;
PbConstraints pb_constraints_;
LiteralWatchers* clauses_propagator_;
PbConstraints* pb_constraints_;
// Ordered list of propagators used by Propagate()/Untrail().
std::vector<SatPropagator*> propagators_;