# Source code for tryalgo.two_sat

#!/usr/bin/env python3
# -*- coding: utf-8 -*-
"""\
Solving 2-SAT boolean formulas
jill-jenn vie et christoph durr - 2015-2019
"""

from tryalgo.strongly_connected_components import tarjan

# snip{
def _vertex(lit):  # integer encoding of a litteral
if lit > 0:
return 2 * (lit - 1)
return 2 * (-lit - 1) + 1

[docs]def two_sat(formula):
"""Solving a 2-SAT boolean formula

:param formula: list of clauses, a clause is pair of literals
over X1,...,Xn for some n.
a literal is an integer, for example -1 = not X1, 3 = X3
:returns: table with boolean assignment satisfying the formula or None
:complexity: linear
"""
# num_variables is the number of variables
num_variables = max(abs(clause[p])
for p in (0, 1) for clause in formula)
graph = [[] for node in range(2 * num_variables)]
for x_idx, y_idx in formula:                           # x_idx or y_idx
graph[_vertex(-x_idx)].append(_vertex(y_idx))     # -x_idx => y_idx
graph[_vertex(-y_idx)].append(_vertex(x_idx))     # -y_idx => x_idx
sccp = tarjan(graph)
comp_id = [None] * (2 * num_variables)  # each node's component ID
assignment = [None] * (2 * num_variables)
for component in sccp:
rep = min(component)             # representative of the component
for vtx in component:
comp_id[vtx] = rep
if assignment[vtx] is None:
assignment[vtx] = True
assignment[vtx ^ 1] = False    # complementary literal
for i in range(num_variables):
if comp_id[2 * i] == comp_id[2 * i + 1]:
return None                        # insatisfiable formula
return assignment[::2]
# snip}