155 : postsolver_(postsolver),
156 num_trivial_clauses_(0),
157 drat_proof_handler_(nullptr),
171 equiv_mapping_ = mapping;
177 void AddClause(absl::Span<const Literal> clause);
188 bool Presolve(
const std::vector<bool>& var_that_can_be_removed);
199 int NumVariables()
const {
return literal_to_clause_sizes_.size() / 2; }
234 drat_proof_handler_ = drat_proof_handler;
239 bool ProcessClauseToSimplifyOthersUsingLiteral(
ClauseIndex clause_index,
245 void AddClauseInternal(std::vector<Literal>* clause);
249 void RebuildLiteralToClauses();
254 void RemoveAllClauseContaining(
Literal x,
bool register_for_postsolve);
260 bool ProcessAllClauses();
264 Literal FindLiteralWithShortestOccurrenceList(
265 absl::Span<const Literal> clause);
266 LiteralIndex FindLiteralWithShortestOccurrenceListExcluding(
267 const std::vector<Literal>& clause,
Literal to_exclude);
279 void SimpleBva(LiteralIndex l);
282 void DisplayStats(
double elapsed_seconds);
287 uint64_t ComputeSignatureOfClauseVariables(
ClauseIndex ci);
292 void InitializePriorityQueue();
293 void UpdatePriorityQueue(BooleanVariable var);
295 PQElement() : heap_index(-1), variable(-1), weight(0.0) {}
298 void SetHeapIndex(
int h) { heap_index = h; }
299 int GetHeapIndex()
const {
return heap_index; }
303 bool operator<(
const PQElement& other)
const {
304 return weight > other.weight;
308 BooleanVariable variable;
311 util_intops::StrongVector<BooleanVariable, PQElement> var_pq_elements_;
312 AdjustablePriorityQueue<PQElement> var_pq_;
316 void InitializeBvaPriorityQueue();
317 void UpdateBvaPriorityQueue(LiteralIndex lit);
318 void AddToBvaPriorityQueue(LiteralIndex lit);
319 struct BvaPqElement {
320 BvaPqElement() : heap_index(-1), literal(-1), weight(0.0) {}
323 void SetHeapIndex(
int h) { heap_index = h; }
324 int GetHeapIndex()
const {
return heap_index; }
328 bool operator<(
const BvaPqElement& other)
const {
329 return weight < other.weight;
333 LiteralIndex literal;
336 std::deque<BvaPqElement> bva_pq_elements_;
337 AdjustablePriorityQueue<BvaPqElement> bva_pq_;
340 absl::btree_set<LiteralIndex> m_lit_;
341 std::vector<ClauseIndex> m_cls_;
342 util_intops::StrongVector<LiteralIndex, int> literal_to_p_size_;
343 std::vector<std::pair<LiteralIndex, ClauseIndex>> flattened_p_;
344 std::vector<Literal> tmp_new_clause_;
348 std::vector<bool> in_clause_to_process_;
349 std::deque<ClauseIndex> clause_to_process_;
353 std::vector<std::vector<Literal>> clauses_;
356 std::vector<uint64_t> signatures_;
357 int64_t num_inspected_signatures_ = 0;
358 int64_t num_inspected_literals_ = 0;
365 int64_t num_deleted_literals_since_last_cleanup_ = 0;
366 util_intops::StrongVector<LiteralIndex, std::vector<ClauseIndex>>
371 util_intops::StrongVector<LiteralIndex, int> literal_to_clause_sizes_;
374 SatPostsolver* postsolver_;
377 util_intops::StrongVector<LiteralIndex, LiteralIndex> equiv_mapping_;
379 int num_trivial_clauses_;
380 SatParameters parameters_;
381 DratProofHandler* drat_proof_handler_;
382 TimeLimit* time_limit_ =
nullptr;
383 SolverLogger* logger_;
SatPostsolver & operator=(const SatPostsolver &)=delete
std::vector< Literal > Clause(int i) const
const VariablesAssignment & assignment()
std::vector< bool > PostsolveSolution(const std::vector< bool > &solution)
void ApplyMapping(const util_intops::StrongVector< BooleanVariable, BooleanVariable > &mapping)
SatPostsolver(int num_variables)
void Add(Literal x, absl::Span< const Literal > clause)
SatPostsolver(const SatPostsolver &)=delete
This type is neither copyable nor movable.
std::vector< bool > ExtractAndPostsolveSolution(const SatSolver &solver)