C++ Reference: class SatClause

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 std::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. Smaller clause are treated separatly and never constructed. In practice, we do use BinaryImplicationGraph for the clause of size 2, so this is mainly 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.

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().

Rewrite

Return type: void

Arguments: absl::Span<const Literal> new_clause

Rewrites a clause with another shorter one. Note that the clause shouldn't be attached when this is called.

SecondLiteral

Return type: Literal

Size

Return type: int

Number of literals in the clause.