operations_research::sat::SatClause Class Reference

#include <clause.h>

Public Member Functions
void	operator delete (void *p)
	Non-sized delete because this is a tail-padded class.
int	size () const
	Number of literals in the clause.
int	IsRemoved () const
const Literal *	begin () const
	Allows for range based iteration: for (Literal literal : clause) {}.
const Literal *	end () const
Literal	FirstLiteral () const
Literal	SecondLiteral () const
Literal	PropagatedLiteral () const
absl::Span< const Literal >	PropagationReason () const
absl::Span< const Literal >	AsSpan () const
	Returns a Span<> representation of the clause.
bool	RemoveFixedLiteralsAndTestIfTrue (const VariablesAssignment &assignment)
bool	IsSatisfied (const VariablesAssignment &assignment) const
std::string	DebugString () const

Static Public Member Functions
static SatClause *	Create (absl::Span< const Literal > literals)
	--— SatClause --—

Friends
class	ClauseManager

Detailed Description

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.

Definition at line 53 of file clause.h.

Member Function Documentation

AsSpan()

absl::Span< const Literal > operations_research::sat::SatClause::AsSpan ( ) const

inline

Returns a Span<> representation of the clause.

Definition at line 97 of file clause.h.

begin()

const Literal * operations_research::sat::SatClause::begin ( ) const

inline

Allows for range based iteration: for (Literal literal : clause) {}.

Definition at line 76 of file clause.h.

Create()

SatClause * operations_research::sat::SatClause::Create ( absl::Span< const Literal > literals )

static

--— SatClause --—

Creates a sat clause. There must be at least 2 literals. Clause with one literal fix variable directly and are never constructed.

Note

in practice, we use BinaryImplicationGraph for the clause of size 2, so this is used for size at least 3.

static

Definition at line 2479 of file clause.cc.

DebugString()

std::string operations_research::sat::SatClause::DebugString

(

)

const

Definition at line 2523 of file clause.cc.

end()

const Literal * operations_research::sat::SatClause::end ( ) const

inline

Definition at line 77 of file clause.h.

FirstLiteral()

Literal operations_research::sat::SatClause::FirstLiteral ( ) const

inline

Returns the first and second literals. These are always the watched literals if the clause is attached in the LiteralWatchers.

Definition at line 81 of file clause.h.

IsRemoved()

int operations_research::sat::SatClause::IsRemoved ( ) const

inline

We re-use the size to lazily remove clause and notify that they need to be deleted. It is why this is not called empty() to emphasis that fact. Note that we never create an initially empty clause, so there is no confusion with an infeasible model with an empty clause inside.

Definition at line 73 of file clause.h.

IsSatisfied()

bool operations_research::sat::SatClause::IsSatisfied

(

const VariablesAssignment &

assignment

)

const

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.

Definition at line 2516 of file clause.cc.

operator delete()

void operations_research::sat::SatClause::operator delete ( void * p )

inline

Non-sized delete because this is a tail-padded class.

Definition at line 62 of file clause.h.

PropagatedLiteral()

Literal operations_research::sat::SatClause::PropagatedLiteral ( ) const

inline

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.

Definition at line 87 of file clause.h.

PropagationReason()

absl::Span< const Literal > operations_research::sat::SatClause::PropagationReason ( ) const

inline

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.

Definition at line 92 of file clause.h.

RemoveFixedLiteralsAndTestIfTrue()

bool operations_research::sat::SatClause::RemoveFixedLiteralsAndTestIfTrue

(

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

the removed literal can still be accessed in the portion [size, old_size) of literals().

for an attached clause, removing fixed literal is okay because if any of the watched literal is assigned, then the clause is necessarily true.

Definition at line 2492 of file clause.cc.

SecondLiteral()

Literal operations_research::sat::SatClause::SecondLiteral ( ) const

inline

Definition at line 82 of file clause.h.

size()

int operations_research::sat::SatClause::size ( ) const

inline

Number of literals in the clause.

Definition at line 67 of file clause.h.

Friends And Related Symbol Documentation

ClauseManager

friend class ClauseManager

friend

The manager needs to permute the order of literals in the clause and call Clear()/Rewrite.

Definition at line 119 of file clause.h.

---

The documentation for this class was generated from the following files:

• ortools/sat/clause.h
• ortools/sat/clause.cc