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.

Method
AsSpan	Return type: absl::Span<const Literal> Returns a Span<> representation of the clause.
begin	Return type: const Literal* const Allows for range based iteration: for (Literal literal : clause) {}.
Create	Return type: static SatClause* Arguments: absl::Span<const Literal> 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.
DebugString	Return type: std::string
delete	Return type: void operator Arguments: void* p Non-sized delete because this is a tail-padded class.
empty	Return type: int
end	Return type: const Literal* const
FirstLiteral	Return type: Literal Returns the first and second literals. These are always the watched literals if the clause is attached in the LiteralWatchers.
IsAttached	Return type: bool Returns true if the clause is attached to a LiteralWatchers.
IsSatisfied	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.
PropagatedLiteral	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.
PropagationReason	Return type: absl::Span<const Literal> 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.
RemoveFixedLiteralsAndTestIfTrue	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().
SecondLiteral	Return type: Literal
size	Return type: int Number of literals in the clause.