"""TwoSatisfiability.py

Algorithms for solving 2-satisfiability problems.
For theory and references, see http://en.wikipedia.org/wiki/2-satisfiability

All instances should be represented as a directed implication graph in which
the vertices represent variables and (via Not.py) their negations. A variable
may be represented by any hashable Python object, and its negation should
be represented by the object Not(x). For instance, the implication graph
    {1:[2,3], 2:[Not(1),3]}
from the unit tests of this module represents the system of implications
among three logical variables v1, v2, and v3:
    v1 => v2, v1 => v3;  v2 => ~v1, v2 => v3.
An instance is satisfiable if it is possible to assign the Boolean values
True and False to these variables in order to make all implications become
logically correct. These problems have many applications involving problems
in which variables may take on either of two values and pairs of variables
are subject to arbitrary constraints; see the Wikipedia article for details.

If G is a graph of this type,
- Symmetrize(G) extends G by adding the contrapositive of each implication
- Satisfiable(G) returns True or False according to whether the
  2SAT instance can be satisfied. It takes linear time in the size of G.
- Forced(G) returns a dictionary mapping a subset of variables of G to
  values that they are forced to hold in any satisfying assignment.
  The empty dictionary is returned if all variables are free to take either
  truth value, and None is returned if the instance is unsatisfiable.
  Because this uses a reachability algorithm in directed acyclic graphs,
  it is not truly linear time but is still polynomial.

D. Eppstein, April 2009.
"""

import unittest
from Not import Not,SymbolicNegation
from Graphs import copyGraph
from StrongConnectivity import Condensation
from AcyclicReachability import Reachability

def Symmetrize(G):
    """Expand implication graph to a larger symmetric form.
    
    If the 2SAT instance includes an implication A=>B, then
    it is also valid to conclude that ~B => ~A, and our 2SAT solver
    needs to have that second implication made explicit.
    But we do not want to force users to supply the contrapositives
    for each of the implications they include, so we use this routine
    to fill in any missing implications.
    """
    H = copyGraph(G)
    for v in G:
        H.setdefault(Not(v),set())  # make sure all negations are included
        for w in G[v]:
            H.setdefault(w,set())   # as well as all implicants
            H.setdefault(Not(w),set()) # and negated implicants
    for v in G:
        for w in G[v]:
            H[Not(w)].add(Not(v))
    return H

def Satisfiable(G):
    """Does this 2SAT instance have a satisfying assignment?"""
    G = Condensation(Symmetrize(G))
    for C in G:
        for v in C:
            if Not(v) in C:
                return False
    return True

def Forced(G):
    """Find forced values for variables in a 2SAT instance.
    
    A variable's value is forced to x if every satisfying assignment
    assigns the same value x to that variable. We return a dictionary
    (possibly empty) in which the keys are the forced variables
    and their values are the values they are forced to.
    
    If the given instance is unsatisfiable, we return None."""
    Force = {}
    Sym = Symmetrize(G)
    Con = Condensation(Sym)
    Map = {}
    for SCC in Con:
        for v in SCC:
            Map[v] = SCC
    Reach = Reachability(Con)
    for v in Sym:
        if Reach.reachable(Map[v],Map[Not(v)]): # v implies not v?
            value = False
            if isinstance(v,SymbolicNegation):
                v = Not(v)
                value = True
            if v in Force:  # already added by negation?
                return None
            Force[v] = value
    return Force

# Unit tests
# Run python TwoSatisfiability.py to perform these tests.

class TwoSatTest(unittest.TestCase):
    T1 = {1:[2,3], 2:[Not(1),3]}
    T2 = {1:[2], 2:[Not(1)], Not(1):[3], 3:[4,2], 4:[1]}

    def testTwoSat(self):
        """Check that the correct problems are satisfiable."""
        self.assertEqual(Satisfiable(self.T1),True)
        self.assertEqual(Satisfiable(self.T2),False)

    def testForced(self):
        """Check that we can correctly identify forced variables."""
        self.assertEqual(Forced(self.T1),{1:False})
        self.assertEqual(Forced(self.T2),None)

if __name__ == "__main__":
    unittest.main()