sat Namespace Reference

Namespaces
namespace	concepts
	namespace containing various type concepts
namespace	detail
namespace	inout
	Namespace containing dimacs io utilities.
namespace	traits
	namespace containing various type traits. Prefer using the concepts.

Classes
class	Clause
	Clause class with watch literals. More...
struct	FirstVariable
	Variable selection strategy that selects the first unassigned variable. More...
class	Heuristic
	Type erasure heuristic wrapper that can hold any type of heuristic. More...
class	Literal
	Structure representing a literal in a CNF-SAT problem. More...
class	MovableHeuristic
	Wrapper for heuristics that do not support move construction or assignment. More...
class	Profiler
	Profiler that manages multiple events. More...
struct	Result
	Profiling result. More...
class	RNG
	Random number generator singleton class. More...
class	ScopeWatch
	Stop watch that automatically adds a timing event to a profiler at destruction. More...
class	Solver
	Main solver class. More...
class	StopWatch
	Used to measure time between start a start and a stop event. More...
class	SubscribableEvent
	C# inspired event class that manages a list of event handlers that can be invoked together. More...
class	SubscriberHandle
	Identifies a function handler subscribed to a SubscribableEvent. Can be used to unsubscribe the function handler. More...
struct	TimingEvent
	Represents an event with a duration. More...
class	Variable
	Structure representing a binary variable in a CNF-SAT problem. More...

Concepts
concept	clause_like
concept	heuristic

Typedefs
using	ClausePointer = std::shared_ptr< Clause >
using	ConstClausePointer = std::shared_ptr< const Clause >

Enumerations
enum class	TruthValue { False = -1 , Undefined = 0 , True = 1 }
	Represents a truth value. More...

Functions
Literal	pos (Variable x)
Literal	neg (Variable x)
Variable	var (Literal l)
std::ostream &	operator<< (std::ostream &os, Variable x)
std::ostream &	operator<< (std::ostream &os, Literal l)

Detailed Description

Author

Tim Luchterhand

Date

26.11.24

Author

Tim Luchterhand

Date

29.11.24

Author

Tim Luchterhand

Date

27.11.24

Author

Tim Luchterhand

Date

09.08.2024

Enumeration Type Documentation

TruthValue

enum class sat::TruthValue

strong

Represents a truth value.

Enumerator
False	variable is true
Undefined	variable is unassigned
True	variable is true

Function Documentation

neg()

Literal sat::neg

(

Variable

x

)

Creates the negative Literal for a given variable

Parameters

x	Variable for which to create the literal

Returns

negative literal of x

operator<<() [1/2]

std::ostream & sat::operator<<	(	std::ostream &	os,
		Literal	l
	)

Ostream operator allowing for easy printing of literals

References sat::Variable::get(), sat::Literal::get(), sat::Literal::sign(), and var().

Here is the call graph for this function:

operator<<() [2/2]

std::ostream & sat::operator<<	(	std::ostream &	os,
		Variable	x
	)

Ostream operator allowing for easy printing of variables

References sat::Variable::get().

Here is the call graph for this function:

pos()

Literal sat::pos

(

Variable

x

)

Creates the positive Literal for a given variable

Parameters

x	Variable for which to create the literal

Returns

positive literal of x

var()

Variable sat::var

(

Literal

l

)

Gets the corresponding Variable of a Literal

Parameters

l

Returns

Variable of given Literal

Referenced by operator<<(), and sat::inout::to_dimacs().

Here is the caller graph for this function: