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

more work on sat solver

Browse Source
This commit is contained in:
lperron@google.com
2014-01-17 18:32:42 +00:00
parent 6aaf76dbd9
commit 2863a3314e
9 changed files with 257 additions and 142 deletions
Download Patch File Download Diff File Expand all files Collapse all files

19
src/sat/boolean_problem.cc
View File

@@ -19,10 +19,12 @@ namespace sat {
bool LoadBooleanProblem(const LinearBooleanProblem& problem,
SatSolver* solver) {
LOG(INFO) << "Loading problem '" << problem.name() << "', "
<< problem.num_variables() << " variables, "
<< problem.constraints_size() << " constraints.";
solver->Reset(problem.num_variables());
if (solver->parameters().log_search_progress()) {
LOG(INFO) << "Loading problem '" << problem.name() << "', "
<< problem.num_variables() << " variables, "
<< problem.constraints_size() << " constraints.";
}
solver->SetNumVariables(problem.num_variables());
std::vector<LiteralWithCoeff> cst;
int64 num_terms = 0;
for (const LinearBooleanConstraint& constraint : problem.constraints()) {
@@ -42,8 +44,14 @@ bool LoadBooleanProblem(const LinearBooleanProblem& problem,
return false;
}
}
LOG(INFO) << "The problem contains " << num_terms << " terms.";
if (solver->parameters().log_search_progress()) {
LOG(INFO) << "The problem contains " << num_terms << " terms.";
}
return true;
}
void UseObjectiveForSatAssignmentPreference(const LinearBooleanProblem& problem,
SatSolver* solver) {
// Initialize the heuristic to look for a good solution.
if (problem.type() == LinearBooleanProblem::MINIMIZATION ||
problem.type() == LinearBooleanProblem::MAXIMIZATION) {
@@ -66,7 +74,6 @@ bool LoadBooleanProblem(const LinearBooleanProblem& problem,
}
}
}
return true;
}
bool AddObjectiveConstraint(const LinearBooleanProblem& problem,

5
src/sat/boolean_problem.h
View File

@@ -22,6 +22,11 @@ namespace sat {
// Loads a BooleanProblem into a given SatSolver instance.
bool LoadBooleanProblem(const LinearBooleanProblem& problem, SatSolver* solver);
// Uses the objective coefficient to drive the SAT search towards an
// heuristically better solution.
void UseObjectiveForSatAssignmentPreference(const LinearBooleanProblem& problem,
SatSolver* solver);
// Adds the constraint that the objective is smaller or equals to the given
// upper bound.
bool AddObjectiveConstraint(const LinearBooleanProblem& problem,

11
src/sat/pb_constraint.cc
View File

@@ -195,7 +195,7 @@ bool UpperBoundedLinearConstraint::Propagate(int trail_index,
}
}
Update(current_rhs, slack);
return true;
return *slack >= 0;
}
void UpperBoundedLinearConstraint::FillReason(const Trail& trail,
@@ -223,12 +223,18 @@ void UpperBoundedLinearConstraint::FillReason(const Trail& trail,
reason->push_back(literal.Negated());
}
current_rhs -= coeffs_[coeff_index];
// If current_rhs reaches zero, then we already have a minimal reason for
// the constraint to be unsat. We can stop there.
if (current_rhs == 0) break;
}
if (i == starts_[coeff_index]) {
--coeff_index;
}
}
if (reason->size() == 0) return;
// In both cases, we can't minimize the reason further.
if (reason->size() <= 1 || coeffs_.size() == 1) return;
// Find the smallest coefficient greater than current_rhs.
// We want a coefficient of a literal that wasn't assigned at the time.
@@ -240,6 +246,7 @@ void UpperBoundedLinearConstraint::FillReason(const Trail& trail,
if (!trail.Assignment().IsVariableAssigned(literal.Variable()) ||
trail.Info(literal.Variable()).trail_index > source_trail_index) {
coeff = coeffs_[coeff_index];
if (coeff == current_rhs + 1) break;
}
if (i == starts_[coeff_index]) --coeff_index;
}

11
src/sat/pb_constraint.h
View File

@@ -15,6 +15,7 @@
#include <deque>
#include "base/hash.h"
#include "base/hash.h"
#include "sat/sat_base.h"
#include "util/stats.h"
@@ -169,9 +170,11 @@ class PbConstraints {
num_constraint_lookups_(0),
num_slack_updates_(0) {}
~PbConstraints() {
IF_STATS_ENABLED(LOG(INFO) << stats_.StatString());
LOG(INFO) << "num_constraint_lookups_: " << num_constraint_lookups_;
LOG(INFO) << "num_slack_updates_: " << num_slack_updates_;
IF_STATS_ENABLED({
LOG(INFO) << stats_.StatString();
LOG(INFO) << "num_constraint_lookups_: " << num_constraint_lookups_;
LOG(INFO) << "num_slack_updates_: " << num_slack_updates_;
});
}
// Changes the number of variables.
@@ -281,7 +284,7 @@ class PbReasonCache {
return std::make_pair(info.pb_constraint, info.source_trail_index);
}
std::map<std::pair<UpperBoundedLinearConstraint*, int>, VariableIndex> map_;
hash_map<std::pair<UpperBoundedLinearConstraint*, int>, VariableIndex> map_;
DISALLOW_COPY_AND_ASSIGN(PbReasonCache);
};

10
src/sat/sat_conflict.cc
View File

@@ -471,6 +471,12 @@ void SatSolver::CompressLearnedClausesIfNeeded() {
if (num_learned_clause_before_cleanup_ > 0) return;
SCOPED_TIME_STAT(&stats_);
// First time?
if (learned_clauses_.size() == 0) {
InitLearnedClauseLimit();
return;
}
// Move the clause that should be kept at the beginning and sort the other
// using the ClauseOrdering order.
std::vector<SatClause*>::iterator clause_to_keep_end = std::partition(
@@ -509,9 +515,9 @@ bool SatSolver::ShouldRestart() {
void SatSolver::InitRestart() {
SCOPED_TIME_STAT(&stats_);
restart_count_ = 0;
if (parameters_.restart_period() > 0) {
CHECK_EQ(restart_count_, 0);
CHECK_EQ(SUniv(1), 1);
DCHECK_EQ(SUniv(1), 1);
conflicts_until_next_restart_ = parameters_.restart_period();
} else {
conflicts_until_next_restart_ = -1;

30
src/sat/sat_parameters.proto
View File

@@ -17,16 +17,21 @@ package operations_research.sat;
// Contains the definitions for all the sat algorithm parameters and their
// default values.
message SatParameters {
// Specifies how the variable activities should be initialized.
// Variable with high activity are selected first for branching.
enum InitialActivity {
ALL_ZERO_ACTIVITY = 0;
RANDOM_ACTIVITY = 1;
SCALED_USAGE_ACTIVITY = 2;
// Tie breaking for the variable activity. If two variables have the same
// activity, then the one with higher weight will be selected first for
// branching.
enum VariableWeight {
// Zero by default but can be changed with SetAssignmentPreference().
// This stays the same between Solve() calls.
DEFAULT_WEIGHT = 0;
// Both value below are recomputed at the beginning of each Solve() call.
RANDOM_WEIGHT = 1;
STATIC_SCALED_USAGE_WEIGHT = 2;
}
optional InitialActivity initial_activity = 1 [default = ALL_ZERO_ACTIVITY];
optional VariableWeight variable_weight = 1 [default = DEFAULT_WEIGHT];
// Specifies how branching on variable should be done.
// Note that this is overridden by calls to SetAssignmentPreference().
enum VariableBranching {
// Always branch on the variable being true.
FIXED_POSITIVE = 0;
@@ -53,7 +58,7 @@ message SatParameters {
// Specifies how literals should be initially sorted in a clause.
enum LiteralOrdering {
// Do nothing and keep literals in order.
// Do nothing and keep literals in their current order.
LITERAL_IN_ORDER = 0;
// Sort the literals by increasing order of their variable appearance in the
// problem.
@@ -159,4 +164,13 @@ message SatParameters {
// Maximum number of conflicts allowed to solve a problem.
optional int64 max_number_of_conflicts = 37
[default = 0x7FFFFFFFFFFFFFFF]; // kint64max
// Maximum memory allowed for the whole thread containing the solver. The
// solver will abort as soon as it detects that this limit is crossed. As a
// result, this limit is approximative, but usually the solver will not go too
// much over.
optional int64 max_memory_in_mb = 40 [default = 4096];
// Whether the solver should log the search progress to LOG(INFO).
optional bool log_search_progress = 41 [default = false];
}

227
src/sat/sat_solver.cc
View File

@@ -19,6 +19,7 @@
#include "base/integral_types.h"
#include "base/logging.h"
#include "base/sysinfo.h"
#include "base/join.h"
#include "util/time_limit.h"
#include "base/stl_util.h"
@@ -57,28 +58,26 @@ bool CompareLiteral(Literal l1, Literal l2) { return l1.Index() < l2.Index(); }
// ----- LiteralWatchers -----
LiteralWatchers::LiteralWatchers()
: is_clean_(true), num_inspected_clauses_(0), stats_("LiteralWatchers") {}
: is_clean_(true),
num_inspected_clauses_(0),
num_watched_clauses_(0),
stats_("LiteralWatchers") {}
LiteralWatchers::~LiteralWatchers() {
IF_STATS_ENABLED(LOG(INFO) << stats_.StatString());
}
void LiteralWatchers::Init() {
is_clean_ = true;
num_inspected_clauses_ = 0;
num_watched_clauses_ = 0;
}
void LiteralWatchers::Resize(int num_variables) {
DCHECK(is_clean_);
watchers_on_false_.resize(num_variables << 1);
needs_cleaning_.assign(num_variables << 1, false);
needs_cleaning_.resize(num_variables << 1, false);
statistics_.resize(num_variables);
}
// Note that this is the only place where we add Watcher so the DCHECK
// guarantees that there are no duplicates.
void LiteralWatchers::AttachOnFalse(Literal a, Literal b, SatClause* clause) {
SCOPED_TIME_STAT(&stats_);
DCHECK(is_clean_);
DCHECK(!WatcherListContains(watchers_on_false_[a.Index()], *clause));
watchers_on_false_[a.Index()].push_back(Watcher(clause, b));
@@ -128,6 +127,7 @@ bool LiteralWatchers::PropagateOnFalse(Literal false_literal, Trail* trail) {
}
bool LiteralWatchers::AttachAndPropagate(SatClause* clause, Trail* trail) {
SCOPED_TIME_STAT(&stats_);
++num_watched_clauses_;
UpdateStatistics(*clause, /*added=*/true);
clause->SortLiterals(statistics_, parameters_);
@@ -135,6 +135,7 @@ bool LiteralWatchers::AttachAndPropagate(SatClause* clause, Trail* trail) {
}
void LiteralWatchers::LazyDetach(SatClause* clause) {
SCOPED_TIME_STAT(&stats_);
--num_watched_clauses_;
UpdateStatistics(*clause, /*added=*/false);
clause->LazyDetach();
@@ -176,7 +177,6 @@ void LiteralWatchers::UpdateStatistics(const SatClause& clause, bool added) {
void BinaryImplicationGraph::Resize(int num_variables) {
SCOPED_TIME_STAT(&stats_);
implications_.resize(num_variables << 1);
num_propagations_ = 0;
}
void BinaryImplicationGraph::AddBinaryClause(Literal a, Literal b) {
@@ -520,11 +520,15 @@ std::string SatClause::DebugString() const {
SatSolver::SatSolver()
: num_variables_(0),
pb_constraints_(&trail_),
current_decision_level_(0),
propagation_trail_index_(0),
binary_propagation_trail_index_(0),
counters_(),
is_model_unsat_(false),
variable_activity_increment_(1.0),
clause_activity_increment_(1.0),
num_learned_clause_before_cleanup_(0),
target_number_of_learned_clauses_(0),
conflicts_until_next_restart_(0),
restart_count_(0),
reason_cache_(trail_),
@@ -538,14 +542,13 @@ SatSolver::~SatSolver() {
void SatSolver::SetNumVariables(int num_variables) {
SCOPED_TIME_STAT(&stats_);
CHECK_GE(num_variables, num_variables_);
num_variables_ = num_variables;
watched_clauses_.Resize(num_variables);
binary_implication_graph_.Resize(num_variables);
watched_clauses_.Resize(num_variables);
trail_.Resize(num_variables);
pb_constraints_.Resize(num_variables);
queue_elements_.resize(num_variables);
variable_activity_increment_ = 1.0;
clause_activity_increment_ = 1.0;
activities_.resize(num_variables, 0.0);
objective_weights_.resize(num_variables << 1, 0.0);
decisions_.resize(num_variables);
@@ -580,6 +583,12 @@ std::string SatSolver::Indent() const {
return result;
}
bool SatSolver::IsMemoryLimitReached() const {
const int64 memory_usage = GetProcessMemoryUsage();
const int64 kMegaByte = 1024 * 1024;
return memory_usage > kMegaByte * parameters_.max_memory_in_mb();
}
bool SatSolver::ModelUnsat() {
is_model_unsat_ = true;
return false;
@@ -701,32 +710,20 @@ void SatSolver::AddLearnedClauseAndEnqueueUnitPropagation(
}
}
// TODO(user): Clear the solver state and all the constraints.
void SatSolver::Reset(int num_variables) {
SCOPED_TIME_STAT(&stats_);
current_decision_level_ = 0;
SetNumVariables(num_variables);
is_model_unsat_ = false;
leave_initial_activities_unchanged_ = false;
counters_ = Counters();
watched_clauses_.Init();
restart_count_ = 0;
InitRestart();
InitLearnedClauseLimit();
random_.Reset(parameters_.random_seed());
}
bool SatSolver::InitialPropagation() {
SCOPED_TIME_STAT(&stats_);
CHECK_EQ(CurrentDecisionLevel(), 0);
if (!Propagate()) {
return ModelUnsat();
}
ProcessNewlyFixedVariables();
return true;
}
int SatSolver::EnqueueDecisionAndBackjumpOnConflict(Literal true_literal) {
SCOPED_TIME_STAT(&stats_);
CHECK_EQ(propagation_trail_index_, trail_.Index());
// We are back at level 0. This can happen because of a restart, or because
// we proved that some variables must take a given value in any satisfiable
// assignment. Trigger a simplification of the clauses if there is new fixed
@@ -820,6 +817,7 @@ int SatSolver::EnqueueDecisionAndBackjumpOnConflict(Literal true_literal) {
int SatSolver::EnqueueDecisionAndBacktrackOnConflict(Literal true_literal) {
SCOPED_TIME_STAT(&stats_);
CHECK_EQ(propagation_trail_index_, trail_.Index());
int max_level = current_decision_level_;
int first_propagation_index =
EnqueueDecisionAndBackjumpOnConflict(true_literal);
@@ -861,71 +859,119 @@ void SatSolver::Backtrack(int target_level) {
trail_.SetDecisionLevel(target_level);
}
namespace {
// Return the next value that is a multiple of interval.
int NextMultipleOf(int64 value, int64 interval) {
return interval * (1 + value / interval);
}
} // namespace
SatSolver::Status SatSolver::Solve() {
SCOPED_TIME_STAT(&stats_);
TimeLimit time_limit(parameters_.max_time_in_seconds());
if (is_model_unsat_) return MODEL_UNSAT;
if (CurrentDecisionLevel() > 0) {
LOG(ERROR) << "Wrong state when calling SatSolver::Solve()";
return INTERNAL_ERROR;
}
TimeLimit time_limit(parameters_.max_time_in_seconds());
timer_.Restart();
// Display initial statistics.
LOG(INFO) << "Initial memory usage: " << MemoryUsage();
LOG(INFO) << "Number of clauses (size > 2): " << problem_clauses_.size();
LOG(INFO) << "Number of binary clauses: "
<< binary_implication_graph_.NumberOfImplications();
LOG(INFO) << "Number of linear constraints: "
<< pb_constraints_.NumberOfConstraints();
LOG(INFO) << "Number of initial fixed variables: " << trail_.Index();
// Fill in the LiteralWatchers structure and perform the initial propagation
// if there was any clauses of length 1.
if (!InitialPropagation()) {
LOG(INFO) << "UNSAT (initial propagation) \n" << StatusString();
return MODEL_UNSAT;
if (parameters_.log_search_progress()) {
LOG(INFO) << "Initial memory usage: " << MemoryUsage();
LOG(INFO) << "Number of clauses (size > 2): " << problem_clauses_.size();
LOG(INFO) << "Number of binary clauses: "
<< binary_implication_graph_.NumberOfImplications();
LOG(INFO) << "Number of linear constraints: "
<< pb_constraints_.NumberOfConstraints();
LOG(INFO) << "Number of initial fixed variables: " << trail_.Index();
}
ProcessNewlyFixedVariables();
// Performs the initial propagation if some variables are fixed.
if (CurrentDecisionLevel() == 0 && !InitialPropagation()) {
if (parameters_.log_search_progress()) {
LOG(INFO) << "UNSAT (initial propagation) \n" << StatusString();
}
return MODEL_UNSAT;
}
if (parameters_.log_search_progress()) {
LOG(INFO) << "Number of assigned variables after initial propagation: "
<< trail_.Index();
LOG(INFO) << "Number of initial watched clauses: "
<< watched_clauses_.num_watched_clauses();
LOG(INFO) << "Parameters: " << parameters_.ShortDebugString();
}
// Any decisions taken before this point is treated as an user provided
// assumption, and the solver will return ASSUMPTIONS_UNSAT if it proves that
// the model is UNSAT with the given assumption.
const int assumption_level = CurrentDecisionLevel();
// Initialize Solve() dependent variables.
InitRestart();
random_.Reset(parameters_.random_seed());
ComputeInitialVariableOrdering();
LOG(INFO) << "Number of assigned variables after initial propagation: "
<< trail_.Index();
LOG(INFO) << "Number of initial watched clauses: "
<< watched_clauses_.num_watched_clauses();
// Variables used to show the search progress.
const int kDisplayFrequency = 10000;
int next_progression_display = kDisplayFrequency;
int next_display = parameters_.log_search_progress()
? NextMultipleOf(num_failures(), kDisplayFrequency)
: std::numeric_limits<int>::max();
// Variables used to check the memory limit every kMemoryCheckFrequency.
const int kMemoryCheckFrequency = 10000;
int next_memory_check = NextMultipleOf(num_failures(), kMemoryCheckFrequency);
// The max_number_of_conflicts is per solve but the counter is for the whole
// solver.
const int64 kFailureLimit =
parameters_.max_number_of_conflicts() == std::numeric_limits<int64>::max()
? std::numeric_limits<int64>::max()
: counters_.num_failures + parameters_.max_number_of_conflicts();
// Starts search.
LOG(INFO) << "Start Search: " << parameters_.ShortDebugString();
for (;;) {
// Test if a limit is reached.
if (time_limit.LimitReached()) {
LOG(INFO) << "The time limit has been reached. Aborting.";
LOG(INFO) << RunningStatisticsString();
if (parameters_.log_search_progress()) {
LOG(INFO) << "The time limit has been reached. Aborting.";
LOG(INFO) << RunningStatisticsString();
}
return LIMIT_REACHED;
}
if (counters_.num_failures >= parameters_.max_number_of_conflicts()) {
LOG(INFO) << "The conflict limit has been reached. Aborting.";
LOG(INFO) << RunningStatisticsString();
if (num_failures() >= kFailureLimit) {
if (parameters_.log_search_progress()) {
LOG(INFO) << "The conflict limit has been reached. Aborting.";
LOG(INFO) << RunningStatisticsString();
}
return LIMIT_REACHED;
}
// This is done this way because counters_.num_failures may augment by
// more than one at each iterations.
if (counters_.num_failures >= next_progression_display) {
// The current memory checking takes time, so we only execute it every
// kMemoryCheckFrequency conflict. We use >= because counters_.num_failures
// may augment by more than one at each iteration.
//
// TODO(user): Find a better way.
if (counters_.num_failures >= next_memory_check) {
next_memory_check = NextMultipleOf(num_failures(), kMemoryCheckFrequency);
if (IsMemoryLimitReached()) {
if (parameters_.log_search_progress()) {
LOG(INFO) << "The memory limit has been reached. Aborting.";
}
return LIMIT_REACHED;
}
}
// Display search progression. We use >= because counters_.num_failures may
// augment by more than one at each iteration.
if (counters_.num_failures >= next_display) {
LOG(INFO) << RunningStatisticsString();
next_progression_display =
kDisplayFrequency * (1 + counters_.num_failures / kDisplayFrequency);
next_display = NextMultipleOf(num_failures(), kDisplayFrequency);
}
if (trail_.Index() == num_variables_.value()) { // At a leaf.
LOG(INFO) << RunningStatisticsString();
LOG(INFO) << "SAT \n" << StatusString();
if (parameters_.log_search_progress()) {
LOG(INFO) << RunningStatisticsString();
LOG(INFO) << "SAT \n" << StatusString();
}
if (!IsAssignmentValid(trail_.Assignment())) {
LOG(INFO) << "Something is wrong, the computed model is not true";
LOG(ERROR) << "Something is wrong, the computed model is not true";
return INTERNAL_ERROR;
}
return MODEL_SAT;
@@ -933,8 +979,8 @@ SatSolver::Status SatSolver::Solve() {
// Note that ShouldRestart() comes first because it had side effects and
// should be executed even if CurrentDecisionLevel() is zero.
if (ShouldRestart() && CurrentDecisionLevel() > 0) {
Backtrack(0);
if (ShouldRestart() && CurrentDecisionLevel() > assumption_level) {
Backtrack(assumption_level);
}
// Choose the next decision variable and propagate it.
@@ -946,9 +992,22 @@ SatSolver::Status SatSolver::Solve() {
next_branch = next_branch.Negated();
}
if (EnqueueDecisionAndBackjumpOnConflict(next_branch) == -1) {
LOG(INFO) << "UNSAT \n" << StatusString();
if (parameters_.log_search_progress()) {
LOG(INFO) << "UNSAT \n" << StatusString();
}
return MODEL_UNSAT;
}
// If we backtracked past the assumptions level, then the model is UNSAT
// given the assumption.
if (CurrentDecisionLevel() < assumption_level) {
if (parameters_.log_search_progress()) {
LOG(INFO) << "ASSUMPTIONS_UNSAT\n" << StatusString();
}
// TODO(user): Reapply the assumptions that are still valid so it is
// easier for a client to see what was incompatible?
return ASSUMPTIONS_UNSAT;
}
}
}
@@ -1008,7 +1067,7 @@ void SatSolver::RescaleVariableActivities(double scaling_factor) {
var_ordering_.Clear();
for (VariableIndex var(0); var < num_variables_; ++var) {
if (!trail_.Assignment().IsVariableAssigned(var)) {
queue_elements_[var].set_weight(activities_[var]);
queue_elements_[var].weight = activities_[var];
var_ordering_.Add(&queue_elements_[var]);
}
}
@@ -1143,13 +1202,12 @@ std::string SatSolver::RunningStatisticsString() const {
}
double SatSolver::ComputeInitialVariableWeight(VariableIndex var) const {
if (leave_initial_activities_unchanged_) return activities_[var];
switch (parameters_.initial_activity()) {
case SatParameters::ALL_ZERO_ACTIVITY:
return 0;
case SatParameters::RANDOM_ACTIVITY:
switch (parameters_.variable_weight()) {
case SatParameters::DEFAULT_WEIGHT:
return queue_elements_[var].tie_breaker;
case SatParameters::RANDOM_WEIGHT:
return random_.RandDouble();
case SatParameters::SCALED_USAGE_ACTIVITY: {
case SatParameters::STATIC_SCALED_USAGE_WEIGHT: {
return watched_clauses_.VariableStatistic(var).weighted_num_appearances /
static_cast<double>(watched_clauses_.num_watched_clauses());
}
@@ -1296,16 +1354,16 @@ Literal SatSolver::NextBranch() {
// TODO(user): This may not be super efficient if almost all the
// variables are assigned.
var = (*var_ordering_.Raw())[random_.Uniform(var_ordering_.Raw()->size())]
->variable();
->variable;
var_ordering_.Remove(&queue_elements_[var]);
} while (trail_.Assignment().IsVariableAssigned(var));
} else {
// The loop is done this way in order to leave the final choice in the heap.
var = var_ordering_.Top()->variable();
var = var_ordering_.Top()->variable;
while (trail_.Assignment().IsVariableAssigned(var)) {
var_ordering_.Pop();
DCHECK(!var_ordering_.IsEmpty());
var = var_ordering_.Top()->variable();
var = var_ordering_.Top()->variable;
}
}
@@ -1332,14 +1390,15 @@ Literal SatSolver::NextBranch() {
}
}
// Note that the activity is left unchanged from one Solve() to the next.
void SatSolver::ComputeInitialVariableOrdering() {
SCOPED_TIME_STAT(&stats_);
var_ordering_.Clear();
for (VariableIndex var(0); var < num_variables_; ++var) {
activities_[var] = ComputeInitialVariableWeight(var);
queue_elements_[var].set_variable(var);
queue_elements_[var].variable = var;
queue_elements_[var].tie_breaker = ComputeInitialVariableWeight(var);
if (!trail_.Assignment().IsVariableAssigned(var)) {
queue_elements_[var].set_weight(activities_[var]);
queue_elements_[var].weight = activities_[var];
var_ordering_.Add(&queue_elements_[var]);
}
}
@@ -1356,12 +1415,12 @@ void SatSolver::Untrail(int target_trail_index) {
WeightedVarQueueElement* element = &(queue_elements_[var]);
const double new_weight = activities_[var];
if (var_ordering_.Contains(element)) {
if (new_weight != element->weight()) {
element->set_weight(new_weight);
if (new_weight != element->weight) {
element->weight = new_weight;
var_ordering_.NoteChangedPriority(element);
}
} else {
element->set_weight(new_weight);
element->weight = new_weight;
var_ordering_.Add(element);
}
}

83
src/sat/sat_solver.h
View File

@@ -81,25 +81,27 @@ struct VariableInfo {
double weighted_num_appearances;
};
// Priority queue element to support var ordering by lowest weight first.
class WeightedVarQueueElement {
public:
WeightedVarQueueElement() : heap_index_(-1), weight_(0.0), var_(-1) {}
bool operator<(const WeightedVarQueueElement& other) const {
return weight_ < other.weight_ ||
(weight_ == other.weight_ && var_ < other.var_);
}
void SetHeapIndex(int h) { heap_index_ = h; }
int GetHeapIndex() const { return heap_index_; }
void set_weight(double weight) { weight_ = weight; }
double weight() const { return weight_; }
void set_variable(VariableIndex var) { var_ = var; }
VariableIndex variable() const { return var_; }
// Priority queue element to support variable ordering by larger weight first.
struct WeightedVarQueueElement {
WeightedVarQueueElement()
: heap_index(-1), weight(0.0), tie_breaker(0.0), variable(-1) {}
private:
int heap_index_;
double weight_;
VariableIndex var_;
// Interface for the AdjustablePriorityQueue.
void SetHeapIndex(int h) { heap_index = h; }
int GetHeapIndex() const { return heap_index; }
// Priority order.
bool operator<(const WeightedVarQueueElement& other) const {
return weight < other.weight ||
(weight == other.weight &&
(tie_breaker < other.tie_breaker ||
(tie_breaker == other.tie_breaker && variable < other.variable)));
}
int heap_index;
double weight;
double tie_breaker;
VariableIndex variable;
};
// This is how the SatSolver store a clause. A clause is just a disjunction of
@@ -218,9 +220,6 @@ class LiteralWatchers {
LiteralWatchers();
~LiteralWatchers();
// Reinit data structures at the beginning of the search.
void Init();
// Resizes the data structure.
void Resize(int num_variables);
@@ -389,6 +388,9 @@ class BinaryImplicationGraph {
int64 num_literals_removed_;
// Bitset used by MinimizeClause().
// TODO(user): use the same one as the one used in the classic minimization
// because they are already initialized. Moreover they contains more
// information.
SparseBitset<LiteralIndex> is_marked_;
SparseBitset<LiteralIndex> is_removed_;
@@ -411,15 +413,13 @@ class SatSolver {
void SetParameters(const SatParameters& parameters);
const SatParameters& parameters() const;
// Initializes the solver to solve a new problem with the given number of
// variables.
//
// TODO(user): This currently only works only on a newly created class...
// Fix this.
void Reset(int num_variables);
// Increases the number of variables of the current problem.
void SetNumVariables(int num_variables);
// Adds a clause to the problem. Returns false if the clause is always false
// and thus make the problem unsatisfiable.
//
// TODO(user): Remove this from the API and only use AddLinearConstraint()?
bool AddProblemClause(const std::vector<Literal>& literals);
// Adds a pseudo-Boolean constraint to the problem. Returns false if the
@@ -438,24 +438,34 @@ class SatSolver {
std::vector<LiteralWithCoeff>* cst);
// Gives a hint so the solver tries to find a solution with the given literal
// sets to true. The weight is a number in [0,1] reflecting the relative
// sets to true. The weight is a positive number reflecting the relative
// importance between multiple calls to SetAssignmentPreference().
//
// Note that this hint is just followed at the beginning, and as such it
// shouldn't impact the solver performance other than make it start looking
// for a solution in a branch that seems better for the problem at hand.
// If the weight is non-zero, branching on a variable will always be done
// according to the preference. If the weight is zero, then the branch will
// be chosen with the current variable_branching() parameter.
//
// The weight is also used as a tie-breaker between variable with the same
// activities provided that the variable_weight parameter is set to
// DEFAULT_WEIGHT.
void SetAssignmentPreference(Literal literal, double weight) {
if (!parameters_.use_optimization_hints()) return;
DCHECK_GE(weight, 0.0);
DCHECK_LE(weight, 1.0);
leave_initial_activities_unchanged_ = true;
activities_[literal.Variable()] = weight;
queue_elements_[literal.Variable()].tie_breaker = weight;
objective_weights_[literal.Index()] = 0.0;
objective_weights_[literal.NegatedIndex()] = weight;
objective_weights_[literal.NegatedIndex()] = 1.0;
}
// Solves the problem and returns its status.
//
// If any EnqueueDecision*() call has been made before Solve() is called then
// this will treat them as assumptions. If, given these assumptions, the model
// is UNSAT, the ASSUMPTIONS_UNSAT status will be returned. MODEL_UNSAT is
// reserved for the case where the model is proven to be unsat without any
// assumptions.
enum Status {
ASSUMPTIONS_UNSAT,
MODEL_UNSAT,
MODEL_SAT,
LIMIT_REACHED,
@@ -528,6 +538,9 @@ class SatSolver {
int64 num_propagations() const;
private:
// Returns false if the thread memory is over the limit.
bool IsMemoryLimitReached() const;
// Sets is_model_unsat_ to true and return false.
bool ModelUnsat();
@@ -703,8 +716,6 @@ class SatSolver {
// Init restart period.
void InitRestart();
void SetNumVariables(int num_variables);
std::string DebugString(const SatClause& clause) const;
std::string StatusString() const;
std::string RunningStatisticsString() const;

3
src/util/time_limit.h
View File

@@ -69,6 +69,9 @@ class TimeLimit {
// Returns 0.0 if the limit was reached.
double GetTimeLeft() const;
// Returns the time elapsed in seconds since the construction of this object.
double GetElapsedTime() const { return timer_.Get(); }
private:
// Size of the running window of measurements taken into account.
static const int kValues = 100;