C++ Reference: class SatPostsolver
Note: 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.
| Method | |
|---|---|
Add | Return type: Arguments: 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. |
ApplyMapping | Return type: Arguments: 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). |
Clause | Return type: Arguments: |
ExtractAndPostsolveSolution | Return type: Arguments: 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). |
FixVariable | Return type: Arguments: 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. |
NumClauses | Return type: Getters to the clauses managed by this class. Important: This will always put the associated literal first. |
PostsolveSolution | Return type: Arguments: |
SatPostsolver | Return type: Arguments: |