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."],[[["\u003cp\u003eSatPostsolver helps recover the initial solution of a problem after presolve algorithms have been applied.\u003c/p\u003e\n"],["\u003cp\u003eIt works by recording the operations performed during presolving and applying them in reverse to the solution of the presolved problem.\u003c/p\u003e\n"],["\u003cp\u003eSatPostsolver provides methods to add clauses, fix variables, and apply variable mappings, reflecting the presolve operations.\u003c/p\u003e\n"],["\u003cp\u003eUsers can extract and postsolve a solution from a SatSolver using the provided methods.\u003c/p\u003e\n"],["\u003cp\u003eIt's essential to apply the same variable mapping to the initial solution before postsolving.\u003c/p\u003e\n"]]],["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"],null,["# SatPostsolver\n\nC++ Reference: class SatPostsolver\n==================================\n\n\nNote: This documentation is automatically generated.\nA simple sat postsolver. \n\nThe 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.\n\n| Method ||\n|----------------------------------------------------------------------------------------------------------------|----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|\n| [`Add`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/simplification.h#L57) | Return type: `void ` Arguments: `Literal x, const absl::Span\u003cconst Literal\u003e 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. |\n| [`ApplyMapping`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/simplification.h#L74) | Return type: `void ` Arguments: ` const absl::StrongVector\u003cBooleanVariable, BooleanVariable\u003e& 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). |\n| [`Clause`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/simplification.h#L87) | Return type: `std::vector\u003cLiteral\u003e ` Arguments: `int i` \u003cbr /\u003e |\n| [`ExtractAndPostsolveSolution`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/simplification.h#L81) | Return type: `std::vector\u003cbool\u003e ` 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). |\n| [`FixVariable`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/simplification.h#L64) | 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. |\n| [`NumClauses`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/simplification.h#L86) | Return type: `int ` Getters to the clauses managed by this class. Important: This will always put the associated literal first. |\n| [`PostsolveSolution`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/simplification.h#L82) | Return type: `std::vector\u003cbool\u003e ` Arguments: `const std::vector\u003cbool\u003e& solution` \u003cbr /\u003e |\n| [`SatPostsolver`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/simplification.h#L52) | Return type: `explicit ` Arguments: `int num_variables` \u003cbr /\u003e |"]]
