Stay organized with collections
Save and categorize content based on your preferences.
C++ Reference: class SatClause
Note: This documentation is automatically generated.
This is how the SatSolver stores a clause. A clause is just a disjunction of
literals. In many places, we just use vector<literal> to encode one. But in
the critical propagation code, we use this class to remove one memory
indirection.
Creates a sat clause. There must be at least 2 literals.
Clause with one literal fix variable directly and are never constructed.
Note that in practice, we use BinaryImplicationGraph for the clause of size
2, so this is used for size at least 3.
Returns true if the clause is satisfied for the given assignment. Note that
the assignment may be partial, so false does not mean that the clause can't
be satisfied by completing the assignment.
Returns the literal that was propagated to true. This only works for a
clause that just propagated this literal. Otherwise, this will just returns
a literal of the clause.
Returns the reason for the last unit propagation of this clause. The
preconditions are the same as for PropagatedLiteral(). Note that we don't
need to include the propagated literal.
Removes literals that are fixed. This should only be called at level 0
where a literal is fixed iff it is assigned. Aborts and returns true if
they are not all false.
Note that the removed literal can still be accessed in the portion [size,
old_size) of literals().
[[["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\u003e\u003ccode\u003eSatClause\u003c/code\u003e is a class within the SatSolver used to efficiently store and process clauses, which are disjunctions of literals.\u003c/p\u003e\n"],["\u003cp\u003eIt provides methods for creating, accessing, and manipulating clauses, including checking for satisfaction and propagation.\u003c/p\u003e\n"],["\u003cp\u003e\u003ccode\u003eSatClause\u003c/code\u003e is optimized for performance in critical propagation code by removing a level of memory indirection compared to using \u003ccode\u003evector<literal>\u003c/code\u003e.\u003c/p\u003e\n"],["\u003cp\u003eClauses with one literal are directly fixed and not stored as \u003ccode\u003eSatClause\u003c/code\u003e objects; binary implications are handled by \u003ccode\u003eBinaryImplicationGraph\u003c/code\u003e.\u003c/p\u003e\n"],["\u003cp\u003eThe class offers functionalities like attaching to LiteralWatchers, removing fixed literals, and obtaining propagation reasons.\u003c/p\u003e\n"]]],["The `SatClause` class stores a disjunction of literals, used in the `SatSolver`. Key actions include: creating clauses with at least 3 literals via `Create`; iterating through literals with `begin` and `end`; getting the first and second literals with `FirstLiteral` and `SecondLiteral`; and accessing a span representation using `AsSpan`. It supports checking if it's `IsSatisfied` or `IsAttached`, and managing propagation using `PropagatedLiteral` and `PropagationReason`. `RemoveFixedLiteralsAndTestIfTrue` is used to remove literals. Also, it supports debug operations with `DebugString` and checks on the size.\n"],null,["# SatClause\n\nC++ Reference: class SatClause\n==============================\n\n\nNote: This documentation is automatically generated.\nThis is how the SatSolver stores a clause. A clause is just a disjunction of literals. In many places, we just use vector\\\u003cliteral\\\u003e to encode one. But in the critical propagation code, we use this class to remove one memory indirection.\n\n| Method ||\n|--------------------------------------------------------------------------------------------------------------|----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|\n| [`AsSpan`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/clause.h#L93) | Return type: `absl::Span\u003cconst Literal\u003e ` Returns a Span\\\u003c\\\u003e representation of the clause. |\n| [`begin`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/clause.h#L72) | Return type: `const Literal* const ` Allows for range based iteration: for (Literal literal : clause) {}. |\n| [`Create`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/clause.h#L60) | Return type: `static SatClause* ` Arguments: `absl::Span\u003cconst Literal\u003e literals` Creates a sat clause. There must be at least 2 literals. Clause with one literal fix variable directly and are never constructed. Note that in practice, we use BinaryImplicationGraph for the clause of size 2, so this is used for size at least 3. |\n| [`DebugString`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/clause.h#L113) | Return type: `std::string ` \u003cbr /\u003e |\n| [`delete`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/clause.h#L63) | Return type: `void operator ` Arguments: `void* p` Non-sized delete because this is a tail-padded class. |\n| [`empty`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/clause.h#L69) | Return type: `int ` \u003cbr /\u003e |\n| [`end`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/clause.h#L73) | Return type: `const Literal* const ` \u003cbr /\u003e |\n| [`FirstLiteral`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/clause.h#L77) | Return type: `Literal ` Returns the first and second literals. These are always the watched literals if the clause is attached in the LiteralWatchers. |\n| [`IsAttached`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/clause.h#L111) | Return type: `bool ` Returns true if the clause is attached to a LiteralWatchers. |\n| [`IsSatisfied`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/clause.h#L108) | Return type: `bool ` Arguments: `const VariablesAssignment& assignment` Returns true if the clause is satisfied for the given assignment. Note that the assignment may be partial, so false does not mean that the clause can't be satisfied by completing the assignment. |\n| [`PropagatedLiteral`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/clause.h#L83) | Return type: `Literal ` Returns the literal that was propagated to true. This only works for a clause that just propagated this literal. Otherwise, this will just returns a literal of the clause. |\n| [`PropagationReason`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/clause.h#L88) | Return type: `absl::Span\u003cconst Literal\u003e ` Returns the reason for the last unit propagation of this clause. The preconditions are the same as for PropagatedLiteral(). Note that we don't need to include the propagated literal. |\n| [`RemoveFixedLiteralsAndTestIfTrue`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/clause.h#L103) | Return type: `bool ` Arguments: `const VariablesAssignment& assignment` Removes literals that are fixed. This should only be called at level 0 where a literal is fixed iff it is assigned. Aborts and returns true if they are not all false. Note that the removed literal can still be accessed in the portion \\[size, old_size) of literals(). |\n| [`SecondLiteral`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/clause.h#L78) | Return type: `Literal ` \u003cbr /\u003e |\n| [`size`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/clause.h#L68) | Return type: `int ` Number of literals in the clause. |"]]
