"""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()