154 : postsolver_(postsolver),
155 num_trivial_clauses_(0),
156 drat_proof_handler_(nullptr),
170 equiv_mapping_ = mapping;
176 void AddClause(absl::Span<const Literal> clause);
187 bool Presolve(
const std::vector<bool>& var_that_can_be_removed);
198 int NumVariables()
const {
return literal_to_clause_sizes_.size() / 2; }
233 drat_proof_handler_ = drat_proof_handler;
238 bool ProcessClauseToSimplifyOthersUsingLiteral(
ClauseIndex clause_index,
244 void AddClauseInternal(std::vector<Literal>* clause);
249 void RemoveAndRegisterForPostsolveAllClauseContaining(
Literal x);
255 bool ProcessAllClauses();
259 Literal FindLiteralWithShortestOccurrenceList(
260 const std::vector<Literal>& clause);
261 LiteralIndex FindLiteralWithShortestOccurrenceListExcluding(
262 const std::vector<Literal>& clause,
Literal to_exclude);
274 void SimpleBva(LiteralIndex l);
277 void DisplayStats(
double elapsed_seconds);
282 uint64_t ComputeSignatureOfClauseVariables(
ClauseIndex ci);
287 void InitializePriorityQueue();
288 void UpdatePriorityQueue(BooleanVariable var);
290 PQElement() : heap_index(-1), variable(-1), weight(0.0) {}
293 void SetHeapIndex(
int h) { heap_index = h; }
294 int GetHeapIndex()
const {
return heap_index; }
298 bool operator<(
const PQElement& other)
const {
299 return weight > other.weight;
303 BooleanVariable variable;
306 util_intops::StrongVector<BooleanVariable, PQElement> var_pq_elements_;
307 AdjustablePriorityQueue<PQElement> var_pq_;
311 void InitializeBvaPriorityQueue();
312 void UpdateBvaPriorityQueue(LiteralIndex lit);
313 void AddToBvaPriorityQueue(LiteralIndex lit);
314 struct BvaPqElement {
315 BvaPqElement() : heap_index(-1), literal(-1), weight(0.0) {}
318 void SetHeapIndex(
int h) { heap_index = h; }
319 int GetHeapIndex()
const {
return heap_index; }
323 bool operator<(
const BvaPqElement& other)
const {
324 return weight < other.weight;
328 LiteralIndex literal;
331 std::deque<BvaPqElement> bva_pq_elements_;
332 AdjustablePriorityQueue<BvaPqElement> bva_pq_;
335 absl::btree_set<LiteralIndex> m_lit_;
336 std::vector<ClauseIndex> m_cls_;
337 util_intops::StrongVector<LiteralIndex, int> literal_to_p_size_;
338 std::vector<std::pair<LiteralIndex, ClauseIndex>> flattened_p_;
339 std::vector<Literal> tmp_new_clause_;
343 std::vector<bool> in_clause_to_process_;
344 std::deque<ClauseIndex> clause_to_process_;
348 std::vector<std::vector<Literal>> clauses_;
351 std::vector<uint64_t> signatures_;
352 int64_t num_inspected_signatures_ = 0;
353 int64_t num_inspected_literals_ = 0;
357 util_intops::StrongVector<LiteralIndex, std::vector<ClauseIndex>>
362 util_intops::StrongVector<LiteralIndex, int> literal_to_clause_sizes_;
365 SatPostsolver* postsolver_;
368 util_intops::StrongVector<LiteralIndex, LiteralIndex> equiv_mapping_;
370 int num_trivial_clauses_;
371 SatParameters parameters_;
372 DratProofHandler* drat_proof_handler_;
373 TimeLimit* time_limit_ =
nullptr;
374 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)
void FixVariable(Literal x)