Two_Sat.H File Reference

2-SAT solver based on Tarjan's SCC algorithm. More...

#include <cassert>
#include <utility>
#include <limits>
#include <ah-errors.H>
#include <tpl_array.H>
#include <tpl_dynArray.H>
#include <tpl_graph.H>
#include <tpl_dynSetTree.H>
#include <Tarjan.H>

Include dependency graph for Two_Sat.H:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	Aleph::Two_Sat< GT >
	2-SAT solver using Tarjan's SCC algorithm. More...

Namespaces
namespace	Aleph
	Main namespace for Aleph-w library functions.

Detailed Description

2-SAT solver based on Tarjan's SCC algorithm.

The 2-satisfiability problem (2-SAT) involves determining if a conjunction of clauses, each with exactly two literals, can be satisfied by a truth assignment.

This implementation uses an implication graph and Tarjan's strongly connected components (SCC) algorithm. A formula is satisfiable if and only if no variable and its negation are in the same SCC.

Literal encoding

Variables are 0-indexed from 0 to n-1. Each variable i has two literals:

• Positive: 2*i
• Negative: 2*i + 1

Signed 1-based indices are also supported: +k for x_{k-1} and -k for ~x_{k-1}.

See also

Tarjan.H

Author

Leandro Rabindranath Leon

Definition in file Two_Sat.H.