139 lines
6.0 KiB
C++
139 lines
6.0 KiB
C++
// Copyright 2010-2025 Google LLC
|
|
// Licensed under the Apache License, Version 2.0 (the "License");
|
|
// you may not use this file except in compliance with the License.
|
|
// You may obtain a copy of the License at
|
|
//
|
|
// http://www.apache.org/licenses/LICENSE-2.0
|
|
//
|
|
// Unless required by applicable law or agreed to in writing, software
|
|
// distributed under the License is distributed on an "AS IS" BASIS,
|
|
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
|
// See the License for the specific language governing permissions and
|
|
// limitations under the License.
|
|
|
|
#ifndef ORTOOLS_SAT_LRAT_CHECKER_H_
|
|
#define ORTOOLS_SAT_LRAT_CHECKER_H_
|
|
|
|
#include <stddef.h>
|
|
|
|
#include <cstdint>
|
|
#include <string>
|
|
#include <string_view>
|
|
|
|
#include "absl/container/flat_hash_map.h"
|
|
#include "absl/container/flat_hash_set.h"
|
|
#include "absl/types/span.h"
|
|
#include "ortools/base/strong_int.h"
|
|
#include "ortools/sat/sat_base.h"
|
|
#include "ortools/sat/util.h"
|
|
|
|
namespace operations_research {
|
|
namespace sat {
|
|
|
|
// The ID of a clause.
|
|
DEFINE_STRONG_INT_TYPE(ClauseId, int64_t);
|
|
|
|
// An incremental checker for LRAT proofs (https://arxiv.org/abs/1612.02353).
|
|
class LratChecker {
|
|
public:
|
|
// The clause IDs used in a proof that a clause has a Resolution Asymmetric
|
|
// Tautology (RAT) property. See AddInferredClause() for more details.
|
|
struct RatIds {
|
|
ClauseId resolvant_id;
|
|
absl::Span<const ClauseId> unit_ids;
|
|
};
|
|
|
|
// Adds a clause of the problem. Returns true if successful, i.e., if the
|
|
// given ID is not already used by another clause (it is OK to reuse the ID of
|
|
// a deleted clause). Does nothing if a previous step failed or if the proof
|
|
// is already complete, or if the clause contains a literal and its negation
|
|
// (since it is always true, it should not be needed to infer anything).
|
|
//
|
|
// Problem clauses can be added after inferred clauses which do not reference
|
|
// them. This can be used to add learned clauses proved by another worker, or
|
|
// "axioms" that we admit without proof.
|
|
bool AddProblemClause(ClauseId id, absl::Span<const Literal> clause);
|
|
|
|
// Adds a clause which is inferred from the problem clauses and/or the
|
|
// previously inferred clauses (that have not been deleted; they are called
|
|
// the 'current' clauses). Does nothing if a previous step failed or if the
|
|
// proof is already complete, or if the clause contains a literal and its
|
|
// negation (since it is always true, it should not be needed to infer
|
|
// anything). Otherwise, returns true if the given inference proof is valid,
|
|
// i.e., if the following conditions hold (checked sequentially):
|
|
//
|
|
// 1) The clause ID is not already used by another clause (it is OK to reuse
|
|
// the ID of a deleted clause).
|
|
// 2) The `unit_ids` clauses exist and are or become unit (or, for the last
|
|
// one, possibly empty) if all the literals of `clause` are assumed to be
|
|
// false. This list must be in unit propagation order: if a clause c
|
|
// becomes unit (or empty) because clauses c_1, ..., c_k are unit, then c
|
|
// must appear after c_1, ..., c_k in the list. Let RUP be all the
|
|
// literals which are found to be false by unit propagation.
|
|
// 3) If `rat` is empty, the last `unit_ids` clause must become empty after
|
|
// unit propagation.
|
|
// 4) Otherwise `clause` must not be empty, and `rat_clauses` must contain
|
|
// all the current clauses which contain the negation of the first
|
|
// literal of `clause` (called the pivot 'p') -- and no other clauses.
|
|
// Moreover, for each r in `rat`:
|
|
// * Either `clause` and the `r.resolvant_id` clause have two pairs of
|
|
// complementary literals.
|
|
// * Or all the `r.unit_ids` clauses must become unit (except the last one,
|
|
// which must become empty) if all the literals of `clause` and of the
|
|
// `r.resolvant_id` clause (minus ~p), as well as those in RUP (from
|
|
// condition 2), are assumed to be false (this list must be in unit
|
|
// propagation order, as explained above).
|
|
bool AddInferredClause(ClauseId id, absl::Span<const Literal> clause,
|
|
absl::Span<const ClauseId> unit_ids,
|
|
absl::Span<const RatIds> rat);
|
|
|
|
// Deletes problem or inferred clauses. It is OK to delete a clause which has
|
|
// already been deleted or has never been added.
|
|
void DeleteClauses(absl::Span<const ClauseId> clause_ids);
|
|
|
|
// Returns true if the unsatisfiability proof is valid and complete, i.e.
|
|
// whether the empty clause has been successfully inferred.
|
|
bool Check() const { return complete_; }
|
|
|
|
// Returns the reason of the first failed operation, or an empty string if all
|
|
// operations were successful.
|
|
std::string_view error_message() const { return error_message_; }
|
|
|
|
private:
|
|
bool AddClauseInternal(ClauseId id, absl::Span<const Literal> clause,
|
|
bool is_problem_clause,
|
|
absl::Span<const ClauseId> unit_ids,
|
|
absl::Span<const RatIds> rat);
|
|
|
|
bool Error(ClauseId id, std::string_view error);
|
|
|
|
// The problem and inferred clauses which have not been deleted. The clause
|
|
// literals are sorted and without duplicates.
|
|
// TODO(user): investigate more cache friendly data structures (could be
|
|
// more efficient but their correctness could be harder to trust).
|
|
absl::flat_hash_map<ClauseId, FixedCapacityVector<Literal>> clauses_;
|
|
|
|
// The number of clauses in `clauses_` which contain each literal.
|
|
absl::flat_hash_map<Literal, int> occurrences_;
|
|
|
|
// Whether all the operations made so far were valid.
|
|
bool valid_ = true;
|
|
std::string error_message_;
|
|
|
|
// Whether the proof is complete, i.e., whether the empty clause has been
|
|
// successfully inferred.
|
|
bool complete_ = false;
|
|
|
|
// Temporary sets used to check unit propagation proofs.
|
|
absl::flat_hash_set<Literal> tmp_false_literals_set_;
|
|
absl::flat_hash_set<Literal> tmp_rat_false_literals_set_;
|
|
|
|
// Temporary set used to check the RAT property of an inferred clause.
|
|
absl::flat_hash_set<ClauseId> tmp_clause_ids_;
|
|
};
|
|
|
|
} // namespace sat
|
|
} // namespace operations_research
|
|
|
|
#endif // ORTOOLS_SAT_LRAT_CHECKER_H_
|