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

backport sat from main

Browse Source
This commit is contained in:
Laurent Perron
2025-11-24 15:39:26 +01:00
committed by Corentin Le Molgat
parent 84046f9e6b
commit cd37bacd2a
19 changed files with 302 additions and 196 deletions
Download Patch File Download Diff File Expand all files Collapse all files

8
ortools/sat/BUILD.bazel
View File

@@ -904,23 +904,16 @@ cc_test(
":cp_model_cc_proto",
":cp_model_checker",
":cp_model_solver",
":cp_model_solver_helpers",
":cp_model_test_utils",
":cp_model_utils",
":drat_checker",
":lp_utils",
":model",
":sat_base",
":sat_parameters_cc_proto",
":sat_solver",
":synchronization",
"//ortools/base:gmock_main",
"//ortools/base:parse_test_proto",
"//ortools/linear_solver:linear_solver_cc_proto",
"//ortools/port:os",
"//ortools/util:logging",
"@abseil-cpp//absl/container:flat_hash_set",
"@abseil-cpp//absl/flags:flag",
"@abseil-cpp//absl/log",
"@abseil-cpp//absl/strings",
],
@@ -4274,6 +4267,7 @@ cc_library(
":model",
":sat_base",
"//ortools/base:file",
"@abseil-cpp//absl/flags:flag",
"@abseil-cpp//absl/log",
"@abseil-cpp//absl/log:check",
"@abseil-cpp//absl/strings",

35
ortools/sat/clause.cc
View File

@@ -103,6 +103,8 @@ bool LiteralsAreFixedAtRoot(const Trail& trail,
ClauseManager::ClauseManager(Model* model)
: SatPropagator("ClauseManager"),
clause_id_generator_(model->GetOrCreate<ClauseIdGenerator>()),
parameters_(*model->GetOrCreate<SatParameters>()),
assignment_(model->GetOrCreate<Trail>()->Assignment()),
implication_graph_(model->GetOrCreate<BinaryImplicationGraph>()),
trail_(model->GetOrCreate<Trail>()),
num_inspected_clauses_(0),
@@ -327,6 +329,9 @@ SatClause* ClauseManager::AddRemovableClause(ClauseId id,
}
if (add_clause_callback_ != nullptr) add_clause_callback_(lbd, literals);
CHECK(AttachAndPropagate(clause, trail));
// Create an entry in clauses_info_ to mark that clause as removable.
clauses_info_[clause].lbd = lbd;
return clause;
}
@@ -484,6 +489,35 @@ bool ClauseManager::InprocessingFixLiteral(
return implication_graph_->Propagate(trail_);
}
void ClauseManager::ChangeLbdIfBetter(SatClause* clause, int new_lbd) {
auto it = clauses_info_.find(clause);
if (it == clauses_info_.end()) return;
// Always take the min.
if (new_lbd > it->second.lbd) return;
++num_lbd_promotions_;
if (new_lbd <= parameters_.clause_cleanup_lbd_bound()) {
// We keep the clause forever.
clauses_info_.erase(it);
} else {
it->second.lbd = new_lbd;
}
}
bool ClauseManager::RemoveFixedLiteralsAndTestIfTrue(SatClause* clause) {
if (clause->RemoveFixedLiteralsAndTestIfTrue(assignment_)) {
// The clause is always true, detach it.
LazyDelete(clause, DeletionSourceForStat::FIXED_AT_TRUE);
return true;
}
// We should have dealt with unit and unsat clause before this.
CHECK_GE(clause->size(), 2);
ChangeLbdIfBetter(clause, clause->size());
return false;
}
bool ClauseManager::InprocessingRewriteClause(
SatClause* clause, absl::Span<const Literal> new_clause,
absl::Span<const ClauseId> clause_ids) {
@@ -543,6 +577,7 @@ bool ClauseManager::InprocessingRewriteClause(
}
clause->Rewrite(new_clause);
ChangeLbdIfBetter(clause, new_clause.size());
// And we reattach it.
if (all_clauses_are_attached_) {

45
ortools/sat/clause.h
View File

@@ -107,14 +107,6 @@ class SatClause {
return absl::Span<const Literal>(&(literals_[0]), size_);
}
// Removes literals that are fixed. This should only be called at level 0
// where a literal is fixed iff it is assigned. Aborts and returns true if
// they are not all false.
//
// Note that the removed literal can still be accessed in the portion [size,
// old_size) of literals().
bool RemoveFixedLiteralsAndTestIfTrue(const VariablesAssignment& assignment);
// Returns true if the clause is satisfied for the given assignment. Note that
// the assignment may be partial, so false does not mean that the clause can't
// be satisfied by completing the assignment.
@@ -134,6 +126,14 @@ class SatClause {
// never be used afterwards.
void Clear() { size_ = 0; }
// Removes literals that are fixed. This should only be called at level 0
// where a literal is fixed iff it is assigned. Aborts and returns true if
// they are not all false.
//
// Note that the removed literal can still be accessed in the portion [size,
// old_size) of literals().
bool RemoveFixedLiteralsAndTestIfTrue(const VariablesAssignment& assignment);
// Rewrites a clause with another shorter one. Note that the clause shouldn't
// be attached when this is called.
void Rewrite(absl::Span<const Literal> new_clause) {
@@ -154,7 +154,7 @@ class SatClause {
struct ClauseInfo {
double activity = 0.0;
int32_t lbd = 0;
bool protected_during_next_cleanup = false;
int32_t num_cleanup_rounds_since_last_bumped = 0;
};
class BinaryImplicationGraph;
@@ -267,6 +267,18 @@ class ClauseManager : public SatPropagator {
if (it == clauses_info_.end()) return 0;
return it->second.lbd;
}
void KeepClauseForever(SatClause* const clause) {
clauses_info_.erase(clause);
}
void RescaleClauseActivities(double scaling_factor) {
for (auto& entry : clauses_info_) {
entry.second.activity *= scaling_factor;
}
}
// If the new lbd is better than the stored one, update it.
// And return the result of IsRemovable() (this save one hash lookup).
void ChangeLbdIfBetter(SatClause* clause, int new_lbd);
// Total number of clauses inspected during calls to Propagate().
int64_t num_inspected_clauses() const { return num_inspected_clauses_; }
@@ -280,6 +292,10 @@ class ClauseManager : public SatPropagator {
// Number of clauses currently watched.
int64_t num_watched_clauses() const { return num_watched_clauses_; }
// Number of time an existing clause lbd was reduced (due to inprocessing or
// recomputation of lbd in different branches).
int64_t num_lbd_promotions() const { return num_lbd_promotions_; }
ClauseId GetClauseId(const SatClause* clause) const {
const auto it = clause_id_.find(clause);
return it != clause_id_.end() ? it->second : kNoClauseId;
@@ -343,6 +359,8 @@ class ClauseManager : public SatPropagator {
SatClause* clause, absl::Span<const Literal> new_clause,
absl::Span<const ClauseId> clause_ids = {});
bool RemoveFixedLiteralsAndTestIfTrue(SatClause* clause);
// Fix a literal either with an existing LRAT `unit_clause_id`, or with a new
// inferred unit clause, using `clause_ids` as proof.
// This do NOT need to be between [Detach/Attach]AllClauses() calls.
@@ -427,14 +445,17 @@ class ClauseManager : public SatPropagator {
SparseBitset<LiteralIndex> needs_cleaning_;
bool is_clean_ = true;
const SatParameters& parameters_;
const VariablesAssignment& assignment_;
BinaryImplicationGraph* implication_graph_;
Trail* trail_;
// For statistic reporting.
std::vector<int64_t> deletion_counters_;
int64_t num_inspected_clauses_;
int64_t num_inspected_clause_literals_;
int64_t num_watched_clauses_;
int64_t num_inspected_clauses_ = 0;
int64_t num_inspected_clause_literals_ = 0;
int64_t num_watched_clauses_ = 0;
int64_t num_lbd_promotions_ = 0;
mutable StatsGroup stats_;
// For DetachAllClauses()/AttachAllClauses().

2
ortools/sat/cp_model_presolve_test.cc
View File

@@ -8155,10 +8155,10 @@ TEST(PresolveCpModelTest, SolveDiophantine) {
SatParameters params;
params.set_cp_model_presolve(true);
params.set_num_workers(1);
// Should solve in < .01 second. Note that deterministic time is not
// completely accurate.
params.set_max_deterministic_time(.001);
params.set_num_workers(1);
const CpSolverResponse response_with =
SolveWithParameters(model_proto, params);

7
ortools/sat/cp_model_search.cc
View File

@@ -934,6 +934,13 @@ std::vector<SatParameters> GetFullWorkerParameters(
params.search_branching() == SatParameters::FIXED_SEARCH) {
continue;
}
// As of November 2025, we don't support any LP reasoning when producing an
// UNSAT proof.
if ((params.check_lrat_proof() || params.check_drat_proof() ||
params.output_drat_proof()) &&
params.linearization_level() > 1) {
continue;
}
// TODO(user): Enable probing_search in deterministic mode.
// Currently it timeouts on small problems as the deterministic time limit

60
ortools/sat/cp_model_solver.cc
View File

@@ -49,7 +49,6 @@
#include "absl/types/span.h"
#include "google/protobuf/arena.h"
#include "google/protobuf/text_format.h"
#include "ortools/base/file.h"
#include "ortools/base/helpers.h"
#include "ortools/base/logging.h"
#include "ortools/base/options.h"
@@ -132,32 +131,6 @@ ABSL_FLAG(bool, cp_model_use_hint_for_debug_only, false,
"complete, validate that no buggy propagator make it infeasible.");
ABSL_FLAG(bool, cp_model_fingerprint_model, true, "Fingerprint the model.");
ABSL_FLAG(std::string, cp_model_drat_output, "",
"If non-empty, a proof in DRAT format will be written to this file. "
"This only works in the same conditions as the --cp_model_lrat_check "
"flag, and only for pure SAT models.");
ABSL_FLAG(bool, cp_model_drat_check, false,
"If true, a proof in DRAT format will be stored in memory and "
"checked if the problem is UNSAT. This only works in the same "
"conditions as the --cp_model_lrat_check flag, and only for pure SAT "
"models.");
ABSL_FLAG(bool, cp_model_lrat_check, false,
"If true, inferred clauses are checked with an LRAT checker as they "
"are learned. As of November 2025, this only works with a single "
"worker and symmetry level 0 or 1. This also works with presolve, if "
"find_clauses_that_are_exactly_one is false and "
"merge_at_most_one_work_limit is 0. However, in this case, the "
"presolved problem is assumed to be correct, without proof. If the "
"model is not pure SAT, the checks are only partial (some clauses "
"can be assumed without proof).");
ABSL_FLAG(double, cp_model_max_drat_time_in_seconds,
std::numeric_limits<double>::infinity(),
"Maximum time in seconds to check the DRAT proof. This will only "
"be used is the cp_model_drat_check flag is enabled.");
ABSL_FLAG(bool, cp_model_check_intermediate_solutions, false,
"When true, all intermediate solutions found by the solver will be "
"checked. This can be expensive, therefore it is off by default.");
@@ -1035,26 +1008,6 @@ bool SolutionHintIsCompleteAndFeasible(
}
}
std::unique_ptr<LratProofHandler> MaybeCreateLratProofHandler(Model* model) {
const bool check_lrat = absl::GetFlag(FLAGS_cp_model_lrat_check);
const bool check_drat = absl::GetFlag(FLAGS_cp_model_drat_check);
File* drat_output = nullptr;
if (!absl::GetFlag(FLAGS_cp_model_drat_output).empty()) {
CHECK_OK(file::Open(absl::GetFlag(FLAGS_cp_model_drat_output), "w",
&drat_output, file::Defaults()));
}
if (!check_lrat && !check_drat && drat_output == nullptr) return nullptr;
// TODO(user): pass the [presolved] model proto to the handler, so that
// it can map internal problem clause IDs to constraint indices in the
// original model. This will be needed to write the LRAT proof in a file that
// can be checked with an external LRAT checker, expecting the standard LRAT
// ASCII file format (which requires problem clauses IDs between 1 and n).
return std::make_unique<LratProofHandler>(model, check_lrat, check_drat,
drat_output,
/*in_binary_drat_format=*/false);
}
// Encapsulate a full CP-SAT solve without presolve in the SubSolver API.
class FullProblemSolver : public SubSolver {
public:
@@ -1082,7 +1035,7 @@ class FullProblemSolver : public SubSolver {
shared_->RegisterSharedClassesInLocalModel(&local_model_);
std::unique_ptr<LratProofHandler> lrat_proof_handler =
MaybeCreateLratProofHandler(&local_model_);
LratProofHandler::MaybeCreate(&local_model_);
if (lrat_proof_handler != nullptr) {
local_model_.Register<LratProofHandler>(lrat_proof_handler.get());
local_model_.TakeOwnership(lrat_proof_handler.release());
@@ -1111,8 +1064,7 @@ class FullProblemSolver : public SubSolver {
WallTimer timer;
timer.Start();
const bool valid = local_model_.GetOrCreate<SatSolver>()->ModelIsUnsat()
? lrat_proof_handler->Check(absl::GetFlag(
FLAGS_cp_model_max_drat_time_in_seconds))
? lrat_proof_handler->Check()
: lrat_proof_handler->Valid();
shared_->lrat_proof_status->NewSubsolverProofStatus(
valid ? DratChecker::Status::VALID : DratChecker::Status::INVALID,
@@ -1801,12 +1753,8 @@ void SolveCpModelParallel(SharedClasses* shared, Model* global_model) {
const SatParameters& params = *global_model->GetOrCreate<SatParameters>();
if (global_model->GetOrCreate<TimeLimit>()->LimitReached()) return;
if (absl::GetFlag(FLAGS_cp_model_drat_check) ||
!absl::GetFlag(FLAGS_cp_model_drat_output).empty()) {
LOG(WARNING)
<< "DRAT check and output are skipped when using several workers";
absl::SetFlag(&FLAGS_cp_model_drat_check, false);
absl::SetFlag(&FLAGS_cp_model_drat_output, "");
if (params.check_drat_proof() || params.output_drat_proof()) {
LOG(FATAL) << "DRAT proofs are not supported with several workers";
}
// If specified by the user, we might disable some parameters based on their

3
ortools/sat/cp_model_solver.h
View File

@@ -26,9 +26,6 @@
#ifndef SWIG
OR_DLL ABSL_DECLARE_FLAG(bool, cp_model_dump_response);
OR_DLL ABSL_DECLARE_FLAG(bool, cp_model_drat_check);
OR_DLL ABSL_DECLARE_FLAG(bool, cp_model_lrat_check);
OR_DLL ABSL_DECLARE_FLAG(double, cp_model_max_drat_time_in_seconds);
#endif
namespace operations_research {

23
ortools/sat/cp_model_solver_test.cc
View File

@@ -14,12 +14,10 @@
#include "ortools/sat/cp_model_solver.h"
#include <cstdint>
#include <memory>
#include <string>
#include <vector>
#include "absl/container/flat_hash_set.h"
#include "absl/flags/flag.h"
#include "absl/log/log.h"
#include "absl/strings/str_join.h"
#include "gtest/gtest.h"
@@ -29,15 +27,10 @@
#include "ortools/port/os.h"
#include "ortools/sat/cp_model.pb.h"
#include "ortools/sat/cp_model_checker.h"
#include "ortools/sat/cp_model_solver_helpers.h"
#include "ortools/sat/cp_model_test_utils.h"
#include "ortools/sat/cp_model_utils.h"
#include "ortools/sat/lp_utils.h"
#include "ortools/sat/model.h"
#include "ortools/sat/sat_base.h"
#include "ortools/sat/sat_parameters.pb.h"
#include "ortools/sat/sat_solver.h"
#include "ortools/sat/synchronization.h"
#include "ortools/util/logging.h"
namespace operations_research {
@@ -5462,11 +5455,11 @@ TEST(CpModelSolverTest, DratProofIsValidForRandom3Sat) {
SatParameters params;
params.set_num_workers(1);
params.set_cp_model_presolve(false);
params.set_symmetry_level(0);
params.set_linearization_level(0);
params.set_symmetry_level(1);
params.set_linearization_level(1);
params.set_check_drat_proof(true);
params.set_max_drat_time_in_seconds(60);
params.set_debug_crash_if_lrat_check_fails(true);
absl::SetFlag(&FLAGS_cp_model_drat_check, true);
absl::SetFlag(&FLAGS_cp_model_max_drat_time_in_seconds, 60);
int num_infeasible = 0;
for (int i = 0; i < 100; ++i) {
@@ -5484,12 +5477,12 @@ TEST(CpModelSolverTest, DratProofIsValidForRandom3Sat) {
TEST(CpModelSolverTest, LratProofIsValidForRandom3Sat) {
SatParameters params;
params.set_num_workers(1);
params.set_num_workers(8);
params.set_cp_model_presolve(false);
params.set_symmetry_level(0);
params.set_linearization_level(0);
params.set_symmetry_level(1);
params.set_linearization_level(1);
params.set_check_lrat_proof(true);
params.set_debug_crash_if_lrat_check_fails(true);
absl::SetFlag(&FLAGS_cp_model_lrat_check, true);
int num_infeasible = 0;
for (int i = 0; i < 100; ++i) {

2
ortools/sat/csharp/CpSolver.cs
View File

@@ -201,6 +201,8 @@ public sealed class CpSolver : IDisposable
public double WallTime() => Response!.WallTime;
public string SolveLog() => Response!.SolveLog;
public IList<int> SufficientAssumptionsForInfeasibility() => Response!.SufficientAssumptionsForInfeasibility;
public string SolutionInfo() => Response!.SolutionInfo;

28
ortools/sat/java/CpSolverTest.java
View File

@@ -109,7 +109,7 @@ public final class CpSolverTest {
final CpSolverStatus status = solver.solve(model);
assertThat(status).isEqualTo(CpSolverStatus.MODEL_INVALID);
assertEquals("var #0 has no domain(): name: \"x\"", solver.getSolutionInfo());
assertEquals("var #0 has no domain(): name: \"x\"", solver.solutionInfo());
}
@Test
@@ -309,6 +309,32 @@ public final class CpSolverTest {
assertThat(log).contains("OPTIMAL");
}
@Test
public void testCpSolver_logToResponse() throws Exception {
System.out.println("testCpSolver_logToResponse");
final CpModel model = new CpModel();
assertNotNull(model);
// Creates the variables.
final int numVals = 3;
final IntVar x = model.newIntVar(0, numVals - 1, "x");
final IntVar y = model.newIntVar(0, numVals - 1, "y");
// Creates the constraints.
model.addDifferent(x, y);
// Creates a solver and solves the model.
final CpSolver solver = new CpSolver();
assertNotNull(solver);
solver.getParameters().setLogToStdout(false).setLogSearchProgress(true).setLogToResponse(true);
final CpSolverStatus status = solver.solve(model);
assertThat(status).isEqualTo(CpSolverStatus.OPTIMAL);
String log = solver.solveLog();
assertThat(log).isNotEmpty();
assertThat(log).contains("Parameters");
assertThat(log).contains("log_to_stdout: false");
assertThat(log).contains("OPTIMAL");
}
@Test
public void testCpSolver_customLogMultiThread() {
System.out.println("testCpSolver_customLogMultiThread");

55
ortools/sat/lrat_proof_handler.cc
View File

@@ -16,19 +16,30 @@
#include <algorithm>
#include <cstdlib>
#include <memory>
#include <string>
#include <vector>
#include "absl/flags/flag.h"
#include "absl/log/check.h"
#include "absl/log/log.h"
#include "absl/strings/str_join.h"
#include "absl/types/span.h"
#include "ortools/base/file.h"
#include "ortools/base/options.h"
#include "ortools/sat/drat_checker.h"
#include "ortools/sat/drat_writer.h"
#include "ortools/sat/lrat_checker.h"
#include "ortools/sat/model.h"
#include "ortools/sat/sat_base.h"
#if defined(_MSC_VER)
ABSL_FLAG(std::string, cp_model_drat_output, ".\\drat.txt",
"File name for the generated DRAT proof, if DRAT output is enabled.");
#else
ABSL_FLAG(std::string, cp_model_drat_output, "/tmp/drat.txt",
"File name for the generated DRAT proof, if DRAT output is enabled.");
#endif
namespace operations_research {
namespace sat {
@@ -46,18 +57,33 @@ std::vector<Literal> SortClauseForDrat(absl::Span<const Literal> clause) {
}
} // namespace
LratProofHandler::LratProofHandler(Model* model, bool check_lrat,
bool check_drat, File* drat_output,
bool in_binary_drat_format)
: lrat_checker_(check_lrat ? std::make_unique<LratChecker>(model)
: nullptr),
drat_checker_(check_drat ? std::make_unique<DratChecker>() : nullptr),
drat_writer_(
drat_output != nullptr
? std::make_unique<DratWriter>(in_binary_drat_format, drat_output)
: nullptr),
debug_crash_on_error_(model->GetOrCreate<SatParameters>()
->debug_crash_if_lrat_check_fails()) {}
std::unique_ptr<LratProofHandler> LratProofHandler::MaybeCreate(Model* model) {
const SatParameters& params = *model->GetOrCreate<SatParameters>();
if (!params.check_lrat_proof() && !params.check_drat_proof() &&
!params.output_drat_proof()) {
return nullptr;
}
return std::unique_ptr<LratProofHandler>(new LratProofHandler(model));
}
LratProofHandler::LratProofHandler(Model* model) {
const SatParameters& params = *model->GetOrCreate<SatParameters>();
if (params.check_lrat_proof()) {
lrat_checker_ = std::make_unique<LratChecker>(model);
}
if (params.check_drat_proof()) {
drat_checker_ = std::make_unique<DratChecker>();
}
if (params.output_drat_proof()) {
File* drat_output = nullptr;
CHECK_OK(file::Open(absl::GetFlag(FLAGS_cp_model_drat_output), "w",
&drat_output, file::Defaults()));
drat_writer_ = std::make_unique<DratWriter>(
/*in_binary_drat_format=*/false, drat_output);
}
max_drat_time_in_seconds_ = params.max_drat_time_in_seconds();
debug_crash_on_error_ = params.debug_crash_if_lrat_check_fails();
}
bool LratProofHandler::AddProblemClause(ClauseId id,
absl::Span<const Literal> clause) {
@@ -193,15 +219,14 @@ DratChecker::Status LratProofHandler::Valid() const {
return DratChecker::Status::UNKNOWN;
}
DratChecker::Status LratProofHandler::Check(
double max_drat_check_time_in_seconds) {
DratChecker::Status LratProofHandler::Check() {
DratChecker::Status status = DratChecker::Status::UNKNOWN;
if (lrat_checker_ != nullptr) {
status = CheckResult(lrat_checker_->Check()) ? DratChecker::Status::VALID
: DratChecker::Status::INVALID;
}
if (status != DratChecker::Status::INVALID && drat_checker_ != nullptr) {
drat_checker_->Check(max_drat_check_time_in_seconds);
drat_checker_->Check(max_drat_time_in_seconds_);
if (status == DratChecker::Status::INVALID && debug_crash_on_error_) {
LOG(FATAL) << "DRAT check failed";
}

17
ortools/sat/lrat_proof_handler.h
View File

@@ -20,7 +20,6 @@
#include <vector>
#include "absl/types/span.h"
#include "ortools/base/file.h"
#include "ortools/sat/drat_checker.h"
#include "ortools/sat/drat_writer.h"
#include "ortools/sat/lrat_checker.h"
@@ -34,8 +33,12 @@ namespace sat {
// and/or by saving it to a file.
class LratProofHandler {
public:
explicit LratProofHandler(Model* model, bool check_lrat, bool check_drat,
File* drat_output, bool in_binary_drat_format);
// TODO(user): pass the [presolved] model proto to the handler, so that
// it can map internal problem clause IDs to constraint indices in the
// original model. This will be needed to write the LRAT proof in a file that
// can be checked with an external LRAT checker, expecting the standard LRAT
// ASCII file format (which requires problem clauses IDs between 1 and n).
static std::unique_ptr<LratProofHandler> MaybeCreate(Model* model);
bool lrat_check_enabled() const { return lrat_checker_ != nullptr; }
bool drat_check_enabled() const { return drat_checker_ != nullptr; }
@@ -84,23 +87,25 @@ class LratProofHandler {
// whether the empty clause has been successfully inferred. Returns INVALID if
// it is not. Returns UNKNOWN if the check timed out (this can only occur
// with DRAT checks), or if neither LRAT nor DRAT checks were enabled.
DratChecker::Status Check(double max_drat_check_time_in_seconds =
std::numeric_limits<double>::infinity());
DratChecker::Status Check();
void AddStats() const;
int64_t num_assumed_clauses() const { return num_assumed_clauses_; }
private:
explicit LratProofHandler(Model* model);
bool CheckResult(bool result) const;
std::unique_ptr<LratChecker> lrat_checker_;
std::unique_ptr<DratChecker> drat_checker_;
std::unique_ptr<DratWriter> drat_writer_;
double max_drat_time_in_seconds_ = std::numeric_limits<double>::infinity();
bool debug_crash_on_error_ = false;
bool all_problem_clauses_loaded_ = false;
int64_t num_assumed_clauses_ = 0;
bool debug_crash_on_error_ = false;
ClauseId pinned_clause_id_ = kNoClauseId;
std::vector<Literal> pinned_clause_;

1
ortools/sat/parameters_validation.cc
View File

@@ -106,6 +106,7 @@ std::string ValidateParameters(const SatParameters& params) {
TEST_NOT_NAN(max_time_in_seconds);
TEST_NOT_NAN(max_deterministic_time);
TEST_NOT_NAN(max_drat_time_in_seconds);
// Parallelism.
const int kMaxReasonableParallelism = 10'000;

7
ortools/sat/probing.cc
View File

@@ -1353,7 +1353,12 @@ void FailedLiteralProbing::MaybeSubsumeWithBinaryClause(
break;
}
}
if (!subsumed) return;
if (!subsumed) {
// The clause is not subsumed but its lbd is 2 when last_decision is
// propagated. This is a "glue" clause.
clause_manager_->ChangeLbdIfBetter(clause, 2);
return;
}
// Since we will remove the clause, we need to make sure we do have the
// implication in our repository.

24
ortools/sat/python/cp_model.py
View File

@@ -1869,6 +1869,19 @@ class CpSolver:
"""Returns the user time in seconds since the creation of the solver."""
return self._checked_response.user_time
@property
def solve_log(self) -> str:
"""Returns the solve log.
To enable this, the parameter log_to_response must be set to True.
"""
return self._checked_response.solve_log
@property
def solve_info(self) -> str:
"""Returns the information about the solve."""
return self._checked_response.solve_info
@property
def response_proto(self) -> cmh.CpSolverResponse:
"""Returns the response object."""
@@ -1948,17 +1961,6 @@ class CpSolver:
def WallTime(self) -> float:
return self.wall_time
def SolveWithSolutionCallback(
self, model: CpModel, callback: "CpSolverSolutionCallback"
) -> cmh.CpSolverStatus:
"""DEPRECATED Use solve() with the callback argument."""
warnings.warn(
"solve_with_solution_callback is deprecated; use solve() with"
+ "the callback argument.",
DeprecationWarning,
)
return self.solve(model, callback)
def SearchForAllSolutions(
self, model: CpModel, callback: "CpSolverSolutionCallback"
) -> cmh.CpSolverStatus:

21
ortools/sat/python/cp_model_test.py
View File

@@ -2080,7 +2080,26 @@ class CpModelTest(absltest.TestCase):
self.assertEqual(10, solver.value(x))
self.assertEqual(-5, solver.value(y))
self.assertRegex(log_callback.log, ".*log_to_stdout.*")
self.assertRegex(log_callback.log, "Starting CP-SAT solver")
def test_log_to_response(self) -> None:
model = cp_model.CpModel()
x = model.new_int_var(-10, 10, "x")
y = model.new_int_var(-10, 10, "y")
model.add_linear_constraint(x + 2 * y, 0, 10)
model.minimize(y)
solver = cp_model.CpSolver()
solver.parameters.log_search_progress = True
solver.parameters.log_to_stdout = False
solver.parameters.log_to_response = True
self.assertEqual(cp_model.OPTIMAL, solver.solve(model))
self.assertEqual(10, solver.value(x))
self.assertEqual(-5, solver.value(y))
self.assertRegex(solver.solve_log, "Starting CP-SAT solver")
print(solver.solution_info)
print(solver.solve_log)
def test_issue2762(self) -> None:
model = cp_model.CpModel()

67
ortools/sat/sat_parameters.proto
View File

@@ -24,7 +24,7 @@ option java_multiple_files = true;
// Contains the definitions for all the sat algorithm parameters and their
// default values.
//
// NEXT TAG: 344
// NEXT TAG: 351
message SatParameters {
// In some context, like in a portfolio of search, it makes sense to name a
// given parameters set for logging purpose.
@@ -176,23 +176,25 @@ message SatParameters {
// target of clauses to keep.
optional double clause_cleanup_ratio = 190 [default = 0.5];
// Each time a clause activity is bumped, the clause has a chance to be
// protected during the next cleanup phase. Note that clauses used as a reason
// are always protected.
enum ClauseProtection {
PROTECTION_NONE = 0; // No protection.
PROTECTION_ALWAYS = 1; // Protect all clauses whose activity is bumped.
PROTECTION_LBD = 2; // Only protect clause with a better LBD.
}
optional ClauseProtection clause_cleanup_protection = 58
[default = PROTECTION_NONE];
// All the clauses with a LBD (literal blocks distance) lower or equal to this
// parameters will always be kept.
//
// Note that the LBD of a clause that just propagated is 1 + number of
// different decision levels of its literals. So that the "classic" LBD of a
// learned conflict is the same as its LBD when we backjump and then propagate
// it.
optional int32 clause_cleanup_lbd_bound = 59 [default = 5];
// Only protect clauses up to this maximum LBD.
optional int32 clause_protection_lbd_bound = 338 [default = 8];
// All the clause with a LBD lower or equal to this will be kept except if
// its activity hasn't been bumped in the last 32 cleanup phase. Note that
// this has no effect if it is <= clause_cleanup_lbd_bound.
optional int32 clause_cleanup_lbd_tier1 = 349 [default = 0];
// All the clause with a LBD lower or equal to this will be kept except if its
// activity hasn't been bumped since the previous cleanup phase. Note that
// this has no effect if it is <= clause_cleanup_lbd_bound or <=
// clause_cleanup_lbd_tier1.
optional int32 clause_cleanup_lbd_tier2 = 350 [default = 0];
// The clauses that will be kept during a cleanup are the ones that come
// first under this order. We always keep or exclude ties together.
@@ -778,6 +780,43 @@ message SatParameters {
// The amount of dtime between each export of shared glue clauses.
optional double share_glue_clauses_dtime = 322 [default = 1.0];
// ==========================================================================
// Proofs
// ==========================================================================
// If true, inferred clauses are checked with an LRAT checker as they are
// learned. As of November 2025, this only works with pure SAT problems, with
// - cp_model_presolve = false,
// - linearization_level <= 1,
// - symmetry_level <= 1,
// - shared_tree_num_workers = 0.
optional bool check_lrat_proof = 344 [default = false];
// TODO(user): add and implement an output_lrat_proof field.
reserved 345;
// If true, and if the problem is UNSAT, a DRAT proof of this UNSAT property
// is checked after the solver has finished. As of November 2025, this only
// works for pure SAT problems, with
// - num_workers = 1,
// - cp_model_presolve = false,
// - linearization_level <= 1,
// - symmetry_level <= 1.
optional bool check_drat_proof = 346 [default = false];
// If true, a DRAT proof that all the clauses inferred by the solver are valid
// is output to a file. As of November 2025, this only works for pure SAT
// problems, with
// - num_workers = 1,
// - cp_model_presolve = false,
// - linearization_level <= 1,
// - symmetry_level <= 1.
optional bool output_drat_proof = 347 [default = false];
// The maximum time allowed to check the DRAT proof (this can take more time
// than the solve itself). Only used if check_drat_proof is true.
optional double max_drat_time_in_seconds = 348 [default = inf];
// ==========================================================================
// Debugging parameters
// ==========================================================================

75
ortools/sat/sat_solver.cc
View File

@@ -492,10 +492,6 @@ int SatSolver::AddLearnedClauseAndEnqueueUnitPropagation(
SatClause* clause = clauses_propagator_->AddRemovableClause(
clause_id, literals, trail_, lbd);
// 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;
BumpClauseActivity(clause);
} else {
CHECK(clauses_propagator_->AddClause(clause_id, literals, trail_, lbd));
@@ -831,16 +827,17 @@ void SatSolver::ProcessCurrentConflict(
}
// Bump the clause activities.
// Note that the activity of the learned clause will be bumped too
// by AddLearnedClauseAndEnqueueUnitPropagation().
//
// Note that the activity of the learned clause will be bumped too by
// AddLearnedClauseAndEnqueueUnitPropagation() after we update the increment.
if (trail_->FailingSatClause() != nullptr) {
BumpClauseActivity(trail_->FailingSatClause());
}
BumpReasonActivities(reason_used_to_infer_the_conflict_);
UpdateClauseActivityIncrement();
// Decay the activities.
decision_policy_->UpdateVariableActivityIncrement();
UpdateClauseActivityIncrement();
pb_constraints_->UpdateActivityIncrement();
// Hack from Glucose that seems to perform well.
@@ -1385,8 +1382,7 @@ void SatSolver::KeepAllClausesUsedToInfer(BooleanVariable variable) {
const BooleanVariable var = (*trail_)[trail_index].Variable();
SatClause* clause = ReasonClauseOrNull(var);
if (clause != nullptr) {
// Keep this clause.
clauses_propagator_->mutable_clauses_info()->erase(clause);
clauses_propagator_->KeepClauseForever(clause);
}
if (trail_->AssignmentType(var) == AssignmentType::kSearchDecision) {
continue;
@@ -2044,43 +2040,26 @@ void SatSolver::BumpClauseActivity(SatClause* clause) {
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.
const int new_lbd = ComputeLbd(clause->AsSpan());
if (new_lbd <= parameters_->clause_cleanup_lbd_bound()) {
clauses_propagator_->mutable_clauses_info()->erase(clause);
return;
}
// Potentially protect this clause for the next cleanup phase.
if (new_lbd <= parameters_->clause_protection_lbd_bound()) {
switch (parameters_->clause_cleanup_protection()) {
case SatParameters::PROTECTION_NONE:
break;
case SatParameters::PROTECTION_ALWAYS:
it->second.protected_during_next_cleanup = true;
break;
case SatParameters::PROTECTION_LBD:
if (new_lbd < it->second.lbd) {
it->second.protected_during_next_cleanup = true;
it->second.lbd = new_lbd;
}
}
}
it->second.num_cleanup_rounds_since_last_bumped = 0;
// Increase the activity.
const double activity = it->second.activity += clause_activity_increment_;
if (activity > parameters_->max_clause_activity_value()) {
RescaleClauseActivities(1.0 / parameters_->max_clause_activity_value());
}
// Update this clause LBD using the new decision orders.
// Note that this can keep the clause forever depending on the parameters.
//
// TODO(user): This cause one more hash lookup, probably not a big deal, but
// could be optimized away.
clauses_propagator_->ChangeLbdIfBetter(clause, ComputeLbd(clause->AsSpan()));
}
void SatSolver::RescaleClauseActivities(double scaling_factor) {
SCOPED_TIME_STAT(&stats_);
clause_activity_increment_ *= scaling_factor;
for (auto& entry : *clauses_propagator_->mutable_clauses_info()) {
entry.second.activity *= scaling_factor;
}
clauses_propagator_->RescaleClauseActivities(scaling_factor);
}
void SatSolver::UpdateClauseActivityIncrement() {
@@ -2157,9 +2136,7 @@ int SatSolver::ComputeLbd(absl::Span<const Literal> literals) {
const SatDecisionLevel level(AssignmentLevel(literal.Variable()));
DCHECK_GE(level, 0);
num_at_max_level += (level == max_level) ? 1 : 0;
if (level > limit && !is_level_marked_[level]) {
is_level_marked_.Set(level);
}
if (level > limit) is_level_marked_.Set(level);
}
return is_level_marked_.NumberOfSetCallsWithDifferentArguments() +
@@ -2258,10 +2235,7 @@ void SatSolver::ProcessNewlyFixedVariables() {
if (clause->IsRemoved()) continue;
const size_t old_size = clause->size();
if (clause->RemoveFixedLiteralsAndTestIfTrue(trail_->Assignment())) {
// The clause is always true, detach it.
clauses_propagator_->LazyDelete(clause,
DeletionSourceForStat::FIXED_AT_TRUE);
if (clauses_propagator_->RemoveFixedLiteralsAndTestIfTrue(clause)) {
++num_detached_clauses;
continue;
}
@@ -3253,14 +3227,25 @@ void SatSolver::CleanClauseDatabaseIfNeeded() {
std::vector<Entry> entries;
auto& clauses_info = *(clauses_propagator_->mutable_clauses_info());
for (auto& entry : clauses_info) {
entry.second.num_cleanup_rounds_since_last_bumped++;
if (clauses_propagator_->ClauseIsUsedAsReason(entry.first)) continue;
if (entry.second.protected_during_next_cleanup) {
entry.second.protected_during_next_cleanup = false;
if (entry.second.lbd <= parameters_->clause_cleanup_lbd_tier1() &&
entry.second.num_cleanup_rounds_since_last_bumped <= 32) {
continue;
}
if (entry.second.lbd <= parameters_->clause_cleanup_lbd_tier2() &&
entry.second.num_cleanup_rounds_since_last_bumped <= 1) {
continue;
}
// The LBD should always have been updated to be <= size.
DCHECK_LE(entry.second.lbd, entry.first->size());
entries.push_back(entry);
}
const int num_protected_clauses = clauses_info.size() - entries.size();
const int num_protected_clauses =
clauses_propagator_->num_removable_clauses() - entries.size();
if (parameters_->clause_cleanup_ordering() == SatParameters::CLAUSE_LBD) {
// Order the clauses by decreasing LBD and then increasing activity.

18
ortools/sat/stat_tables.cc
View File

@@ -115,16 +115,17 @@ void SharedStatTables::AddClausesStat(absl::string_view name, Model* model) {
// Track reductions of Boolean variables.
if (bool_var_table_.empty()) {
bool_var_table_.push_back(
{"Boolean variables", "Fixed", "Equiv", "Total", "Left"});
{"Boolean variables", "Fixed", "Equiv", "Total", "Left", "Binary"});
}
auto* binary = model->GetOrCreate<BinaryImplicationGraph>();
const int64_t num_fixed = sat_solver->NumFixedVariables();
const int64_t num_equiv =
model->GetOrCreate<BinaryImplicationGraph>()->num_redundant_literals() /
2;
const int64_t num_equiv = binary->num_redundant_literals() / 2;
const int64_t num_bools = sat_solver->NumVariables();
bool_var_table_.push_back({FormatName(name), FormatCounter(num_fixed),
FormatCounter(num_equiv), FormatCounter(num_bools),
FormatCounter(num_bools - num_equiv - num_fixed)});
bool_var_table_.push_back(
{FormatName(name), FormatCounter(num_fixed), FormatCounter(num_equiv),
FormatCounter(num_bools),
FormatCounter(num_bools - num_equiv - num_fixed),
FormatCounter(binary->ComputeNumImplicationsForLog())});
// Track the "life of a non-binary clause".
CpSolverResponse r;
@@ -134,7 +135,7 @@ void SharedStatTables::AddClausesStat(absl::string_view name, Model* model) {
clauses_deletion_table_.push_back(
{"Clause deletion", "at_true", "l_and_not(l)", "to_binary",
"sub_conflict", "sub_eager", "sub_vivify", "sub_probing", "sub_inpro",
"blocked", "eliminated", "forgotten", "#conflicts"});
"blocked", "eliminated", "forgotten", "promoted", "conflicts"});
}
absl::Span<const int64_t> deletion_by_source =
model->GetOrCreate<ClauseManager>()->DeletionCounters();
@@ -162,6 +163,7 @@ void SharedStatTables::AddClausesStat(absl::string_view name, Model* model) {
DeletionSourceForStat::ELIMINATED)]),
FormatCounter(deletion_by_source[static_cast<int>(
DeletionSourceForStat::GARBAGE_COLLECTED)]),
FormatCounter(model->GetOrCreate<ClauseManager>()->num_lbd_promotions()),
FormatCounter(r.num_conflicts())});
}