2-SAT helper utilities built on top of the graph wrapper. More...

#include <boost/graph/adjacency_list.hpp>
#include <boost/graph/strong_components.hpp>
#include <utility>
#include <vector>

Include dependency graph for sat.hpp:

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

Functions
int	nxpp::to_2sat_vertex_id (int literal)
	Converts a signed 2-SAT literal into the internal implication-graph vertex ID.

bool	nxpp::two_sat_satisfiable (int num_variables, const std::vector< std::pair< int, int > > &clauses)
	Returns whether a 2-SAT instance is satisfiable.

Detailed Description

2-SAT helper utilities built on top of the graph wrapper.

Function Documentation

bool nxpp::two_sat_satisfiable	(	int	num_variables,
		const std::vector< std::pair< int, int > > &	clauses
	)

inline

Returns whether a 2-SAT instance is satisfiable.

Parameters

num_variables	Number of Boolean variables in the instance.
clauses	Vector of `(x, y)` clauses representing `(x OR y)`.