2-SAT solver using Tarjan's SCC algorithm. More...

#include <Two_Sat.H>

Collaboration diagram for Aleph::Two_Sat< GT >:

Public Types
using	Node = typename GT::Node

using	Arc = typename GT::Arc

Public Member Functions
	Two_Sat (const Two_Sat &)=delete
	Deleted copy constructor to avoid dangling internal Node* pointers.

Two_Sat &	operator= (const Two_Sat &)=delete
	Deleted copy assignment to avoid dangling internal Node* pointers.

	Two_Sat (const size_t n)
	Construct a solver for `n` variables.

size_t	size () const noexcept

size_t	num_nodes () const noexcept

const GT &	implication_graph () const noexcept

void	add_clause (size_t a, size_t b)
	Add a clause `(a OR b)`.

void	add_clause_signed (const long a, const long b)
	Add a clause using signed 1-based variables.

void	add_implication (const size_t a, const size_t b)
	Add an implication `a -> b`.

void	set_true (const size_t a)
	Force literal `a` to be true.

void	set_false (const size_t a)
	Force literal `a` to be false.

void	add_xor (const size_t a, const size_t b)
	Add XOR constraint: `exactly_one(a, b)`.

void	add_equiv (const size_t a, const size_t b)
	Add equivalence constraint: `a <-> b`.

void	add_at_most_one (const Array< size_t > &lits)
	Add at-most-one constraint over a set of literals.

bool	is_satisfiable ()
	Check if the formula is satisfiable.

std::pair< bool, Array< bool > >	solve ()
	Solve the 2-SAT instance.

Static Public Member Functions
Literal helpers
static constexpr size_t	pos_lit (const size_t var) noexcept
	Get the positive literal for a variable.

static constexpr size_t	neg_lit (const size_t var) noexcept
	Get the negative literal for a variable.

static constexpr size_t	negate_lit (const size_t lit) noexcept
	Negate a literal.

static constexpr size_t	lit_var (const size_t lit) noexcept
	Get the variable index of a literal.

static constexpr bool	is_pos_lit (const size_t lit) noexcept
	Check if a literal is positive.

static size_t	signed_to_lit (const long v)
	Convert a signed 1-based variable to a literal index.

Private Attributes
size_t	num_vars

GT	ig

Array< Node * >	lit_nodes

Detailed Description

template<class GT = List_Digraph<Graph_Node<Empty_Class>, Graph_Arc<Empty_Class>>>
class Aleph::Two_Sat< GT >

2-SAT solver using Tarjan's SCC algorithm.

Determines satisfiability of 2-CNF formulas in linear time.

Template Parameters

GT	Directed graph type for the internal implication graph. Defaults to `List_Digraph`.

Definition at line 83 of file Two_Sat.H.

Member Typedef Documentation

◆ Arc

template<class GT = List_Digraph<Graph_Node<Empty_Class>, Graph_Arc<Empty_Class>>>

using Aleph::Two_Sat< GT >::Arc = typename GT::Arc

Definition at line 87 of file Two_Sat.H.

◆ Node

template<class GT = List_Digraph<Graph_Node<Empty_Class>, Graph_Arc<Empty_Class>>>

using Aleph::Two_Sat< GT >::Node = typename GT::Node

Definition at line 86 of file Two_Sat.H.

Constructor & Destructor Documentation

◆ Two_Sat() [1/2]

template<class GT = List_Digraph<Graph_Node<Empty_Class>, Graph_Arc<Empty_Class>>>

Aleph::Two_Sat< GT >::Two_Sat ( const Two_Sat< GT > & )

delete

Deleted copy constructor to avoid dangling internal Node* pointers.

◆ Two_Sat() [2/2]

template<class GT = List_Digraph<Graph_Node<Empty_Class>, Graph_Arc<Empty_Class>>>

Aleph::Two_Sat< GT >::Two_Sat ( const size_t n )

inline

Construct a solver for n variables.

Parameters

n	Number of Boolean variables.

Definition at line 167 of file Two_Sat.H.

References Aleph::Two_Sat< GT >::ig, Aleph::List_Graph< _Graph_Node, _Graph_Arc >::insert_node(), and Aleph::Two_Sat< GT >::lit_nodes.

Member Function Documentation

◆ add_at_most_one()

template<class GT = List_Digraph<Graph_Node<Empty_Class>, Graph_Arc<Empty_Class>>>

void Aleph::Two_Sat< GT >::add_at_most_one ( const Array< size_t > & lits )

inline

Add at-most-one constraint over a set of literals.

Ensures that at most one of the given literals is true. This adds O(k^2) clauses where k is the number of distinct literals.

Singletons are validated but produce no clauses. Duplicate literals are normalized. Pairs of identical literals are skipped to avoid adding redundant forcing clauses.

Parameters

lits	Array of literal indices.

Exceptions

std::domain_error if any literal is out of range.

Definition at line 274 of file Two_Sat.H.

References Aleph::Two_Sat< GT >::add_clause(), ah_domain_error_if, Aleph::divide_and_conquer_partition_dp(), FunctionalMethods< Container, T >::for_each(), Aleph::Two_Sat< GT >::lit_var(), Aleph::Two_Sat< GT >::negate_lit(), Aleph::Two_Sat< GT >::num_vars, Aleph::Array< T >::size(), and Aleph::Array< T >::to_array().

◆ add_clause()

template<class GT = List_Digraph<Graph_Node<Empty_Class>, Graph_Arc<Empty_Class>>>

void Aleph::Two_Sat< GT >::add_clause	(	size_t	a,
		size_t	b
	)

inline

Add a clause (a OR b).

Parameters

a	First literal index.
b	Second literal index.

Exceptions

std::domain_error if literals are out of range.

Definition at line 188 of file Two_Sat.H.

References ah_domain_error_if, Aleph::Two_Sat< GT >::ig, Aleph::List_Graph< _Graph_Node, _Graph_Arc >::insert_arc(), Aleph::Two_Sat< GT >::lit_nodes, Aleph::Two_Sat< GT >::lit_var(), Aleph::Two_Sat< GT >::negate_lit(), and Aleph::Two_Sat< GT >::num_vars.

Referenced by Aleph::Two_Sat< GT >::add_at_most_one(), Aleph::Two_Sat< GT >::add_clause_signed(), Aleph::Two_Sat< GT >::add_implication(), Aleph::Two_Sat< GT >::add_xor(), and Aleph::Two_Sat< GT >::set_true().

◆ add_clause_signed()

template<class GT = List_Digraph<Graph_Node<Empty_Class>, Graph_Arc<Empty_Class>>>

void Aleph::Two_Sat< GT >::add_clause_signed	(	const long	a,
		const long	b
	)

inline

Add a clause using signed 1-based variables.

Parameters

a	First signed variable.
b	Second signed variable.

Definition at line 207 of file Two_Sat.H.

References Aleph::Two_Sat< GT >::add_clause(), ah_domain_error_if, Aleph::divide_and_conquer_partition_dp(), and Aleph::Two_Sat< GT >::signed_to_lit().

◆ add_equiv()

template<class GT = List_Digraph<Graph_Node<Empty_Class>, Graph_Arc<Empty_Class>>>

void Aleph::Two_Sat< GT >::add_equiv	(	const size_t	a,
		const size_t	b
	)

inline

Add equivalence constraint: a <-> b.

Parameters

a	First literal.
b	Second literal.

Definition at line 256 of file Two_Sat.H.

References Aleph::Two_Sat< GT >::add_implication().

◆ add_implication()

template<class GT = List_Digraph<Graph_Node<Empty_Class>, Graph_Arc<Empty_Class>>>

void Aleph::Two_Sat< GT >::add_implication	(	const size_t	a,
		const size_t	b
	)

inline

Add an implication a -> b.

Parameters

a	Antecedent literal.
b	Consequent literal.

Definition at line 221 of file Two_Sat.H.

References Aleph::Two_Sat< GT >::add_clause(), and Aleph::Two_Sat< GT >::negate_lit().

Referenced by Aleph::Two_Sat< GT >::add_equiv().

◆ add_xor()

template<class GT = List_Digraph<Graph_Node<Empty_Class>, Graph_Arc<Empty_Class>>>

void Aleph::Two_Sat< GT >::add_xor	(	const size_t	a,
		const size_t	b
	)

inline

Add XOR constraint: exactly_one(a, b).

Parameters

a	First literal.
b	Second literal.

Definition at line 246 of file Two_Sat.H.

References Aleph::Two_Sat< GT >::add_clause(), and Aleph::Two_Sat< GT >::negate_lit().

◆ implication_graph()

template<class GT = List_Digraph<Graph_Node<Empty_Class>, Graph_Arc<Empty_Class>>>

const GT & Aleph::Two_Sat< GT >::implication_graph ( ) const

inlinenoexcept

Returns: Read-only reference to the internal implication graph.

Definition at line 181 of file Two_Sat.H.

References Aleph::Two_Sat< GT >::ig.

◆ is_pos_lit()

template<class GT = List_Digraph<Graph_Node<Empty_Class>, Graph_Arc<Empty_Class>>>

static constexpr bool Aleph::Two_Sat< GT >::is_pos_lit ( const size_t lit )

inlinestaticconstexprnoexcept

Check if a literal is positive.

Parameters

lit	Literal index.

Returns: true if positive, false if negative.

Definition at line 132 of file Two_Sat.H.

References Aleph::divide_and_conquer_partition_dp().

◆ is_satisfiable()

template<class GT = List_Digraph<Graph_Node<Empty_Class>, Graph_Arc<Empty_Class>>>

bool Aleph::Two_Sat< GT >::is_satisfiable ( )

inline

Check if the formula is satisfiable.

Returns: true if satisfiable.

Definition at line 301 of file Two_Sat.H.

References Aleph::Two_Sat< GT >::solve().

◆ lit_var()

template<class GT = List_Digraph<Graph_Node<Empty_Class>, Graph_Arc<Empty_Class>>>

static constexpr size_t Aleph::Two_Sat< GT >::lit_var ( const size_t lit )

inlinestaticconstexprnoexcept

Get the variable index of a literal.

Parameters

lit	Literal index.

Returns: Variable index.

Definition at line 125 of file Two_Sat.H.

References Aleph::divide_and_conquer_partition_dp().

Referenced by Aleph::Two_Sat< GT >::add_at_most_one(), and Aleph::Two_Sat< GT >::add_clause().

◆ neg_lit()

template<class GT = List_Digraph<Graph_Node<Empty_Class>, Graph_Arc<Empty_Class>>>

static constexpr size_t Aleph::Two_Sat< GT >::neg_lit ( const size_t var )

inlinestaticconstexprnoexcept

Get the negative literal for a variable.

Parameters

var	Variable index (0 to n-1).

Returns: Literal index (odd).

Definition at line 111 of file Two_Sat.H.

Referenced by Aleph::Two_Sat< GT >::signed_to_lit(), and Aleph::Two_Sat< GT >::solve().

◆ negate_lit()

template<class GT = List_Digraph<Graph_Node<Empty_Class>, Graph_Arc<Empty_Class>>>

static constexpr size_t Aleph::Two_Sat< GT >::negate_lit ( const size_t lit )

inlinestaticconstexprnoexcept

Negate a literal.

Parameters

lit	Literal index.

Returns: The opposite literal index.

Definition at line 118 of file Two_Sat.H.

References Aleph::divide_and_conquer_partition_dp().

Referenced by Aleph::Two_Sat< GT >::add_at_most_one(), Aleph::Two_Sat< GT >::add_clause(), Aleph::Two_Sat< GT >::add_implication(), Aleph::Two_Sat< GT >::add_xor(), and Aleph::Two_Sat< GT >::set_false().

◆ num_nodes()

template<class GT = List_Digraph<Graph_Node<Empty_Class>, Graph_Arc<Empty_Class>>>

size_t Aleph::Two_Sat< GT >::num_nodes ( ) const

inlinenoexcept

Returns: Number of nodes in the implication graph (2*n).

Definition at line 178 of file Two_Sat.H.

References Aleph::Two_Sat< GT >::num_vars.

◆ operator=()

template<class GT = List_Digraph<Graph_Node<Empty_Class>, Graph_Arc<Empty_Class>>>

Two_Sat & Aleph::Two_Sat< GT >::operator= ( const Two_Sat< GT > & )

delete

Deleted copy assignment to avoid dangling internal Node* pointers.

◆ pos_lit()

template<class GT = List_Digraph<Graph_Node<Empty_Class>, Graph_Arc<Empty_Class>>>

static constexpr size_t Aleph::Two_Sat< GT >::pos_lit ( const size_t var )

inlinestaticconstexprnoexcept

Get the positive literal for a variable.

Parameters

var	Variable index (0 to n-1).

Returns: Literal index (even).

Definition at line 104 of file Two_Sat.H.

Referenced by Aleph::Two_Sat< GT >::signed_to_lit(), and Aleph::Two_Sat< GT >::solve().

◆ set_false()

template<class GT = List_Digraph<Graph_Node<Empty_Class>, Graph_Arc<Empty_Class>>>

void Aleph::Two_Sat< GT >::set_false ( const size_t a )

inline

Force literal a to be false.

Parameters

a	Literal index.

Definition at line 237 of file Two_Sat.H.

References Aleph::Two_Sat< GT >::negate_lit(), and Aleph::Two_Sat< GT >::set_true().

◆ set_true()

template<class GT = List_Digraph<Graph_Node<Empty_Class>, Graph_Arc<Empty_Class>>>

void Aleph::Two_Sat< GT >::set_true ( const size_t a )

inline

Force literal a to be true.

Parameters

a	Literal index.

Definition at line 229 of file Two_Sat.H.

References Aleph::Two_Sat< GT >::add_clause().

Referenced by Aleph::Two_Sat< GT >::set_false().

◆ signed_to_lit()

template<class GT = List_Digraph<Graph_Node<Empty_Class>, Graph_Arc<Empty_Class>>>

static size_t Aleph::Two_Sat< GT >::signed_to_lit ( const long v )

inlinestatic

Convert a signed 1-based variable to a literal index.

Maps +k to pos_lit(k-1) and -k to neg_lit(k-1).

Parameters

v	Signed variable index (must be non-zero and not LONG_MIN).

Returns: Literal index.

Definition at line 141 of file Two_Sat.H.

References ah_domain_error_if, Aleph::divide_and_conquer_partition_dp(), Aleph::Two_Sat< GT >::neg_lit(), and Aleph::Two_Sat< GT >::pos_lit().

Referenced by Aleph::Two_Sat< GT >::add_clause_signed().

◆ size()

template<class GT = List_Digraph<Graph_Node<Empty_Class>, Graph_Arc<Empty_Class>>>

size_t Aleph::Two_Sat< GT >::size ( ) const

inlinenoexcept

Returns: Number of variables.

Definition at line 175 of file Two_Sat.H.

References Aleph::Two_Sat< GT >::num_vars.

◆ solve()

template<class GT = List_Digraph<Graph_Node<Empty_Class>, Graph_Arc<Empty_Class>>>

std::pair< bool, Array< bool > > Aleph::Two_Sat< GT >::solve ( )

inline

Solve the 2-SAT instance.

Returns: A pair {satisfiable, assignment}.

Definition at line 309 of file Two_Sat.H.

References Aleph::Tarjan_Connected_Components< GT, Itor, SA >::connected_components(), Aleph::Array< T >::create(), Aleph::divide_and_conquer_partition_dp(), GraphCommon< GT, Node, Arc >::get_tgt_node(), Aleph::Digraph_Iterator< GT, Filter >::has_curr(), Aleph::Two_Sat< GT >::ig, Aleph::Two_Sat< GT >::lit_nodes, Aleph::Two_Sat< GT >::neg_lit(), NODE_COUNTER, Aleph::Two_Sat< GT >::num_vars, Aleph::Two_Sat< GT >::pos_lit(), and Aleph::Array< T >::size().

Referenced by Aleph::Two_Sat< GT >::is_satisfiable().

Member Data Documentation

◆ ig

template<class GT = List_Digraph<Graph_Node<Empty_Class>, Graph_Arc<Empty_Class>>>

GT Aleph::Two_Sat< GT >::ig

private

Definition at line 91 of file Two_Sat.H.

Referenced by Aleph::Two_Sat< GT >::Two_Sat(), Aleph::Two_Sat< GT >::add_clause(), Aleph::Two_Sat< GT >::implication_graph(), and Aleph::Two_Sat< GT >::solve().

◆ lit_nodes

template<class GT = List_Digraph<Graph_Node<Empty_Class>, Graph_Arc<Empty_Class>>>

Array<Node *> Aleph::Two_Sat< GT >::lit_nodes

private

Definition at line 92 of file Two_Sat.H.

Referenced by Aleph::Two_Sat< GT >::Two_Sat(), Aleph::Two_Sat< GT >::add_clause(), and Aleph::Two_Sat< GT >::solve().

◆ num_vars

template<class GT = List_Digraph<Graph_Node<Empty_Class>, Graph_Arc<Empty_Class>>>

size_t Aleph::Two_Sat< GT >::num_vars

private

Definition at line 90 of file Two_Sat.H.

Referenced by Aleph::Two_Sat< GT >::add_at_most_one(), Aleph::Two_Sat< GT >::add_clause(), Aleph::Two_Sat< GT >::num_nodes(), Aleph::Two_Sat< GT >::size(), and Aleph::Two_Sat< GT >::solve().

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

Two_Sat.H

Public Types

Public Member Functions

Static Public Member Functions

Private Attributes

Detailed Description

Member Typedef Documentation

◆ Arc

◆ Node

Constructor & Destructor Documentation

◆ Two_Sat() [1/2]

◆ Two_Sat() [2/2]

Member Function Documentation

◆ add_at_most_one()

◆ add_clause()

◆ add_clause_signed()

◆ add_equiv()

◆ add_implication()

◆ add_xor()

◆ implication_graph()

◆ is_pos_lit()

◆ is_satisfiable()

◆ lit_var()

◆ neg_lit()

◆ negate_lit()

◆ num_nodes()

◆ operator=()

◆ pos_lit()

◆ set_false()

◆ set_true()

◆ signed_to_lit()

◆ size()

◆ solve()

Member Data Documentation

◆ ig

◆ lit_nodes

◆ num_vars