Examples of the Two_Sat solver. More...

#include <iostream>
#include <string>
#include <Two_Sat.H>
#include <tpl_sgraph.H>
#include <tpl_agraph.H>

Include dependency graph for two_sat_example.cc:

Functions
void	example_basic_formula ()

void	example_signed_api ()

void	example_2_coloring ()

void	example_team_assignment ()

void	example_graph_backends ()

int	main ()

Detailed Description

Examples of the Two_Sat solver.

Demonstrates four applications of 2-SAT:

Basic formula — solving a simple conjunction of 2-literal clauses.
Graph 2-coloring — deciding if a graph is 2-colorable.
Team assignment — assigning people to teams with constraints.
Using different graph backends — List_SDigraph and Array_Digraph.

What is 2-SAT?

2-SAT is the problem of determining whether a Boolean formula in conjunctive normal form (CNF), where each clause has exactly two literals, is satisfiable.

Example formula: (x0 OR x1) AND (~x0 OR x2) AND (~x1 OR ~x2)

Algorithm

The solver builds an implication graph and uses Tarjan's SCC algorithm. Each clause (a OR b) produces two implications: ~a -> b and ~b -> a. The formula is unsatisfiable iff some variable and its negation lie in the same SCC.

Time: O(n + m) where n = variables, m = clauses
Space: O(n + m)