C++ Reference: class SatPostsolver

This documentation is automatically generated.

A simple sat postsolver.

The idea is that any presolve algorithm can just update this class, and at the end, this class will recover a solution of the initial problem from a solution of the presolved problem.

Return type: void

Arguments: Literal x, const absl::Span<const Literal> clause

The postsolver will process the Add() calls in reverse order. If the given clause has all its literals at false, it simply sets the literal x to true. Note that x must be a literal of the given clause.


Return type: void

Arguments: const gtl::ITIVector<BooleanVariable, BooleanVariable>& mapping

This assumes that the given variable mapping has been applied to the problem. All the subsequent Add() and FixVariable() will refer to the new problem. During postsolve, the initial solution must also correspond to this new problem. Note that if mapping[v] == -1, then the literal v is assumed to be deleted. This can be called more than once. But each call must refer to the current variables set (after all the previous mapping have been applied).


Return type: std::vector<Literal>

Arguments: int i


Return type: std::vector<bool>

Arguments: const SatSolver& solver

Extracts the current assignment of the given solver and postsolve it. Node(fdid): This can currently be called only once (but this is easy to change since only some CHECK will fail).


Return type: void

Arguments: Literal x

Tells the postsolver that the given literal must be true in any solution. We currently check that the variable is not already fixed. TODO(user): this as almost the same effect as adding an unit clause, and we should probably remove this to simplify the code.


Return type: int

Getters to the clauses managed by this class.


Return type: std::vector<bool>

Arguments: const std::vector<bool>& solution


Return type: explicit

Arguments: int num_variables