#

# SAT object that will have work done onto
class SATObject(object):
    """
    """
    # SATObject has only a list of variables (for refrence) and a clause list
    def __init__(self):
        # Dictionary in case variable is greater than total number of variables
        self.varDict = {} 
        # List of clauses represented with tuples of literals
        self.clauses = []

    # Reads in clause from a line, but assumes every line ends with zero and 
    # full clause is listed on this line
    def getClauseFromLine(self,clauseLine):
        # Clause won't contain repeating literals (CNF) 
        clause = set()
        # Go over each literal in clause (ignore zero at end)
        for literal in clauseLine.split()[:-1]:
            # Save whether negation (is either 0 or 1)
            isNeg = 1 if (literal[0]=='-') else 0
            # Variable is a literal with (possible) negation removed
            # Add variable to dict as the next integer available for reference
            if literal[isNeg:] not in self.varDict:
                self.varDict[literal[isNeg:]] = len(self.varDict) 
            # Get recasted variable
            var = self.varDict[literal[isNeg:]]
            # Reform literal from new variable notation (2*v or 2*v+1 if neg) 
            literal = var << 1 | isNeg
            # Append to the list for this clas
            clause.add(literal)
        # Add this clause into the group of clauses
        self.clauses.append(clause)

@@ -76,24 +76,25 @@
 %22%22%22%0A    %22%22%22%0A
+%0A
     # SATObj
@@ -208,15 +208,10 @@
 ary 
-in case
+of
  var
@@ -220,49 +220,52 @@
 ble 
-is greater than total number of variables
+strings (keys) to refernce variable (values)
 %0A   
@@ -335,13 +335,11 @@
 ith 
-tuple
+set
 s of
@@ -993,16 +993,17 @@
         
+#
 if liter
@@ -1042,24 +1042,25 @@
             
+#
     self.var
@@ -1323,25 +1323,18 @@
  # A
-ppend to the list
+dd literal
  for
@@ -1342,17 +1342,19 @@
 this cla
-s
+use
 %0A       
@@ -1466,8 +1466,929 @@
 clause)%0A
+%0A    # Takes in an integer and creates dictionary of that number%0A    # Ex: setVarDict(3) -%3E %7B'1':0, '2':1, '3':2%7D%0A    def setVarDict(self,numOfVars):%0A        for v in range(numOfVars):%0A            self.varDict%5Bstr(v+1)%5D = v%0A%0A    def getFromFile(self,cnfFile,hasSet=True):%0A        # Create instance of this object%0A        # satInstance = cls%0A        # Get lines from CNF data and then close file%0A        with open(cnfFile) as f:%0A            cnfLines = f.readlines()%0A        # First line gives us information of data format%0A        metaData = cnfLines.pop(0).split()%0A        # Get the number of varaibles and clauses specified by file%0A        numOfVars, numOfClauses = metaData%5B2%5D, metaData%5B3%5D%0A        # Add variables to dictionary for reference%0A        self.setVarDict(int(numOfVars))%0A        # Add clauses from file (skip the first line of metadata)%0A        for line in cnfLines:%0A            self.getClauseFromLine(line)%0A

Update SAT object