Stay organized with collections
Save and categorize content based on your preferences.
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.
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.
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).
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).
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.
[[["Easy to understand","easyToUnderstand","thumb-up"],["Solved my problem","solvedMyProblem","thumb-up"],["Other","otherUp","thumb-up"]],[["Missing the information I need","missingTheInformationINeed","thumb-down"],["Too complicated / too many steps","tooComplicatedTooManySteps","thumb-down"],["Out of date","outOfDate","thumb-down"],["Samples / code issue","samplesCodeIssue","thumb-down"],["Other","otherDown","thumb-down"]],["Last updated 2024-08-06 UTC."],[[["SatPostsolver helps recover the initial solution of a problem after presolve algorithms have been applied."],["It works by recording the operations performed during presolving and applying them in reverse to the solution of the presolved problem."],["SatPostsolver provides methods to add clauses, fix variables, and apply variable mappings, reflecting the presolve operations."],["Users can extract and postsolve a solution from a SatSolver using the provided methods."],["It's essential to apply the same variable mapping to the initial solution before postsolving."]]],["The `SatPostsolver` class recovers the initial problem's solution from a presolved one. Key actions include `Add`, which sets a literal true if its clause is false. `ApplyMapping` updates the problem's variable mapping. `FixVariable` enforces a literal's truth. `ExtractAndPostsolveSolution` extracts and processes a solver's assignment. `PostsolveSolution` takes in a solution. `Clause` and `NumClauses` get clause data, and `SatPostsolver` initializes the class. These methods enable reverse-order processing of changes to reconstruct the original solution.\n"]]
