#
from SAT import *

# Solver object to preform operations on the SAT object
class Solver(object):
    '''
    '''
     
    # Constructor by using data file
    def __init__(self,dataFile):
        #
        self.SAT = SAT.initFromFile(dataFile)
        # Create SAT object from data file
        #self.SAT = .initFromFile(dataFile)
        # Assignment of truth values (0,1=True,False) for SAT object
        self.assignment = {}
        # Lambda function to map only ints in SAT.varDict to assignment 
        isInt = lambda x : x if isinstance(x,int) else False
        # Iterate over just the int keys from SAT.varDict
        for var in map(isInt,self.SAT.varDict.keys()):
            # Initiate each variable assignment with no assignment (None)
            self.assignment[var] = None

    # Assign assignment varaible a truth value
    #
    # Input: (int) var, (None,0,1) truthValue
    def assignVar(self,var,truthValue):
        self.assignment[var] = truthValue

    # Check if assignment has solved SAT object
    def isSolved(self):
        # Some variables are not yet assigned
        if None in self.assignment.values():
            return False
        # Check the all clauses to see if assignment is consistent
        for clause in self.SAT.clauses:
            # Return False if any clause is inconsistent with assignment
            if not self.isClauseConsistent(clause):
                return False
        # All clauses passed the check so SAT object is solved 
        return True 

    # Check that the clause is consistent with assignment
    def isClauseConsistent(self,clause):
        #
        isTrue = 0 # Only greater than 0 if at least a one literal is true
        for literal in clause:
            # Get variable from literal
            var = self.SAT.getVar(literal)
            # Assignment is None, 0 (False) or 1 (True)
            value = self.assignment[var]
            # Check that variable has been assigned
            if value == None:
            	return False
            # Add value assigned to testing sum (isTrue)
            else:
                # Negate value if literal in clause is negated
            	isTrue += value ^ self.SAT.isNeg(literal) #bitwise-XOR
        # Test if at least one literal evaluated is True (1)
        return True if (isTrue > 0) else False

    # Create a watchlist to make algorithms simple
    def createWatchlist(self):
        # Creat a 2*numOfVars sized watchlist of empty lists
        self.watchlist = [ [] for i in range(2*self.SAT.numOfVars) ]
        # Watch the first literal in each clause
        for clause in self.SAT.clauses:
            self.watchlist[ list(clause)[0] ].append(clause) #clause set to list

    # Updates the watchlist 
    def updateWatchlist(self,falseLiteral):
		# Loop until there's nothing in list of clauses watching this literal
        while self.watchlist[falseLiteral]:
            clause = self.watchlist[falseLiteral][0] #get first watched clause
            # Default to say no alternative was found
            foundAlt = False
            # Look for alternative literal for the clause to watch           
            for alt in clause:
            	# Get the variable and negation piece of the literal in clause
                v = self.SAT.getVar(alt)
                a = self.SAT.isNeg(alt)
                # Get the current assignment of this variable
                varAssignment = self.assignment[v]
                # See that the newly watched literal has the correct property
                # The variable assignment is None or evaluates to True (1)
                if varAssignment is None or varAssignment == self.SAT.negate(a):
                    foundAlt = True
                    # Get rid of this clause since literal is now True
                    del self.watchlist[falseLiteral][0]
                    # Have this clause watch the alt literal now
                    self.watchlist[alt].append(clause)
                    break
            # No alternative has been found after looking through clause
            if not foundAlt:
                return False
        # Alternative is found (or loop condition fails?)
        return True


    # Basic SAT solver alogrithm that uses recursion
    def simpleSolve(self,var):
        # Check if this is the last assignment to end function call
        if var == self.SAT.numOfVars:
            return True #self.assignment
        
        # Check over all possible assignments
        for truthValue in [0,1]:
            self.assignment[var] = truthValue
            # Update the watchlist with the variable's literal with given value
            if self.updateWatchlist( var << 1 | truthValue ):
                # Check if the next variable is solved with all the assignments done
                if self.simpleSolve(var+1):
                    return True
        
        # Reset and return False since there was a conflict        
        self.assignment[var] = None
        return False
            





@@ -5005,11 +5005,1403 @@
       %0A%0A
+    # SAT solver to find all solutions that uses simpleSolver()%0A    def simpleSolveAll(self):%0A        # Once one solution is found, add the negative of this clause and find%0A        # the next solution. If no new solution can be found, stop and return%0A        # soltions in a list%0A%0A        # List of solutions%0A        solutions = %5B%5D%0A%0A        # Search for all solutions until exhausted%0A        searching = True%0A        while True:%0A            # Reset the watchlist%0A            self.createWatchlist()%0A%0A            # Will tell us if all solutions have been found%0A            searching = self.simpleSolve(0)%0A%0A            # Break out since we found all solutions%0A            if not searching:%0A                return solutions%0A%0A            # Save the resulting solution%0A            solutions.append(self.assignment.copy())%0A%0A            # New clause of negated solution%0A            tempNegSol = set()%0A            for var in self.assignment:%0A                # Get if variable was negated and reverse it%0A                negTemp = self.assignment%5Bvar%5D #self.SAT.negate( self.assignment%5Bvar%5D )%0A                # Add the literal equivalent to the clause%0A                tempNegSol.add( var %3C%3C 1 %7C negTemp )%0A            # Add new clause %0A            self.SAT.clauses.append(tempNegSol)%0A%0A            # Reset the assignments%0A            for key in self.assignment:%0A                self.assignment%5Bkey%5D = None
 %0A%0A%0A

Update Solver class - Add simpleSolveAll() to find all solutions to a SAT object by using simpleSolve(). Solves SAT by solving with simpleSolver() after adding the negation of the previous solution to the set of clauses to solve. Note that this is clearly inefficient but will always return a complete solution.