init

util/SAT2QUBO.py

@@ -0,0 +1,105 @@
+#!/usr/bin/env python3
+
+import numpy as np
+import kSAT
+from tqdm import tqdm
+import math
+
+__VERTEX_WEIGHT__ = 1
+__EDGE_WEIGHT__ = -2
+
+def WMISdictQUBO(kSATInstance):
+    quboInstance = {}
+    
+    for clauseIndex in tqdm(range(kSATInstance.getNumberOfClauses())):
+        clause = kSATInstance.getClause(clauseIndex)
+        
+        # build triangles
+        for varIndexInClause in range(len(clause)):
+            label = kSATInstance.getLableOfBinding(clauseIndex,
+                                                   clause[varIndexInClause])
+            quboInstance[(label, label)] = __VERTEX_WEIGHT__
+            
+            for i in range(varIndexInClause + 1, len(clause)):
+                targetLabel = kSATInstance.getLableOfBinding(clauseIndex,
+                                                             clause[i])
+                
+                quboInstance[(label, targetLabel)] = __EDGE_WEIGHT__
+        
+    # connect conflicts
+    for conflict in kSATInstance.getConflicts():
+        quboInstance[(conflict[0], conflict[1])] = __EDGE_WEIGHT__
+    
+    return quboInstance
+    
+class QuboWriter:
+    def __init__(self, qubo):
+        self.__labelIndexDict = {}
+        self.__qubo = qubo
+        
+        self.__initLabelIndexDict(self.__qubo)
+        
+        print(self.__labelIndexDict)
+    
+    def __initLabelIndexDict(self, qubo):
+        indexCount = 0
+        
+        for coupler in qubo:
+            
+            label1 = coupler[0]
+            label2 = coupler[1]
+            
+            if label1 not in self.__labelIndexDict:
+                self.__labelIndexDict[label1] = indexCount
+                indexCount += 1
+            
+            if label2 not in self.__labelIndexDict:
+                self.__labelIndexDict[label2] = indexCount
+                indexCount += 1
+    
+    def write(self, filePath):
+        quboFile = open(filePath, "w")
+    
+        self.__writeQuboFileHeader(quboFile)
+        self.__writeQuboFileNodes(quboFile)
+        self.__writeQuboFileCouplers(quboFile)
+    
+        quboFile.close()
+    
+    def __writeQuboFileHeader(self, quboFile):
+        numberOfNodes = len(self.__labelIndexDict)
+        numberOfCouplers = len(self.__qubo) - numberOfNodes
+    
+        quboFile.write("c\n")
+        quboFile.write("c this is a generated qubo file\n")
+        quboFile.write("c\n")
+    
+        quboFile.write("p qubo 0 %d %d %d\n" %(numberOfNodes,
+                                               numberOfNodes,
+                                               numberOfCouplers))
+                                               
+    def __writeQuboFileNodes(self, quboFile):
+        for label in self.__labelIndexDict:
+            self.__writeCoupler(quboFile, (label, label))
+            
+    def __writeCoupler(self, quboFile, coupler):
+            indices = self.__getNodeIndicesFromCoupler(coupler)
+    
+            quboFile.write("%d %d  %d\n" % (indices[0],
+                                            indices[1],
+                                            self.__qubo[coupler]))
+
+    def __getNodeIndicesFromCoupler(self, coupler):
+        index1 = self.__labelIndexDict[coupler[0]]
+        index2 = self.__labelIndexDict[coupler[1]]
+        
+        if index1 <= index2:
+            return [index1, index2]
+        else:
+            return [index2, index1]
+            
+    def __writeQuboFileCouplers(self, quboFile):
+        for coupler in self.__qubo:
+            if coupler[0] != coupler[1]:
+                self.__writeCoupler(quboFile, coupler)
+

util/SATquboResult.py

@@ -0,0 +1,168 @@
+import json
+from kSAT import kSAT
+
+class SATquboResult:
+    
+    def __init__(self):
+        self.__assignments = set()
+        self.__activeBindings = {}
+        self.__hasConflicts = False
+        self.__occurrences = 1
+        self.__satisfiesInstance = False
+        self.__assignmentsUpToDate = True
+        
+    
+    def satisfiesInstance(self):
+        return self.__satisfiesInstance
+        
+    def setSatisfiesInstance(self, satInstance):
+        evaluation = satInstance.checkAssignment(self.getAssignmentsWithoutPositionIndex())
+        self.__satisfiesInstance = evaluation
+        
+        
+    def addBinding(self, binding, isActive):
+        self.__assignmentsUpToDate = False
+        clause = binding[0]
+        assignment = binding[1]
+        varLabel = abs(assignment)
+        
+        if varLabel not in self.__activeBindings:
+            self.__activeBindings[varLabel] =  []
+        
+        if not isActive:
+            return
+            
+        bindingSign = -1 if assignment < 0 else 1
+        
+        self.__activeBindings[varLabel].append((clause, bindingSign))
+        self.__checkForConflictAtVar(varLabel)
+        
+    
+    def __checkForConflictAtVar(self, varLabel):
+        if varLabel not in self.__activeBindings:
+            return
+        
+        sign = None
+        
+        for assignment in self.__activeBindings[varLabel]:
+            if sign != None:
+                if sign * assignment[1] < 0:
+                    self.__hasConflicts = True
+                    return
+            sign = assignment[1]
+                    
+    def getAssignments(self):
+        if not self.__assignmentsUpToDate:
+            self.__updateAssignments()
+            
+        return self.__assignments
+    
+    def __updateAssignments(self):
+        self.__assignments = set()
+        
+        for varLabel in self.__activeBindings:
+            bindings = self.__activeBindings[varLabel]
+            
+            if not bindings:
+                self.__assignments.add(-1 * varLabel)
+                
+            for binding in bindings:
+                sign = binding[1]
+                self.__assignments.add(sign * varLabel)
+        
+        self.__assignmentsUpToDate = True
+    
+    def getAssignmentsSortedByVarIndex(self):
+        return sorted(self.getAssignments(), key=abs)
+        
+    def getAssignmentsWithoutPositionIndex(self):
+        assignments = self.getAssignmentsSortedByVarIndex()
+
+        for i in range(len(assignments)):
+            assignments[i] = 0 if assignments[i] < 0 else 1
+        
+        return assignments
+        
+    def getActiveBindings(self):
+        return self.__activeBindings
+    
+    def hasConflicts(self):
+        return self.__hasConflicts
+    
+    def setOccurrences(self, occurrences):
+        self.__occurrences = occurrences
+    
+    def getOccurrences(self):
+        return self.__occurrences
+    
+    def toPrimitive(self):
+        primitive = {}
+        
+        primitive["assignments"] = self.getAssignmentsSortedByVarIndex()
+        primitive["hasConflicts"] = self.__hasConflicts
+        primitive["activeBindings"] = self.getActiveBindings()
+        primitive["satisfiesInstance"] = self.__satisfiesInstance
+        
+        return primitive
+        
+    def fromPrimitive(self, primitive):
+        
+        for varLabel in primitive["activeBindings"]:
+            bindings = primitive["activeBindings"][varLabel]
+            
+            if not bindings:
+                self.addBinding((-1, int(varLabel)), False)
+                
+            for binding in bindings:
+                clause = binding[0]
+                sign = binding[1]
+                
+                self.addBinding((clause, sign * int(varLabel)), True)
+            
+        self.__satisfiesInstance = primitive["satisfiesInstance"]
+
+
+def readAssignmentsFromFile(resultFilePath):
+        resultFile = open(resultFilePath, "r")
+    
+        assignments = []
+    
+        line = resultFile.readline()
+        while line:
+        
+            if line.strip():
+                assignments.append(__parseAssignmentFromLine(line))
+            
+            
+            line = resultFile.readline()
+        
+        resultFile.close()
+    
+        return assignments
+
+def __parseAssignmentFromLine(line):
+    result = json.loads(line)
+    
+    assignment = [None] * abs(max(result["assignments"], key=abs))
+    
+    for varAssignment in result["assignments"]:
+        assignment[abs(varAssignment) - 1] = 0 if varAssignment < 0 else 1
+    
+    return assignment
+    
+def readResultsFromFile(resultFilePath):
+    resultFile = open(resultFilePath, "r")
+    
+    results = []
+    
+    line = resultFile.readline()
+    while line:
+        
+        if line.strip():
+            result = SATquboResult()
+            result.fromPrimitive(json.loads(line))
+            results.append(result)
+            
+        line = resultFile.readline()
+    
+    return results

util/compare.py

@@ -0,0 +1,23 @@
+
+SATISFIABLE = 0
+UNSATISFIABLE = 1
+FALSE_NEGATIVE = 2
+FALSE_POSITIVE = 3
+
+def getComparisonStatus(comparison):
+    if (comparison["minisat_satisfiable"] and
+        comparison["qubo_satisfiable"]):
+        return SATISFIABLE
+        
+    elif (not comparison["minisat_satisfiable"] and
+          not comparison["qubo_satisfiable"]):
+        return UNSATISFIABLE
+        
+    elif (comparison["minisat_satisfiable"] and
+          not comparison["qubo_satisfiable"]):
+        return FALSE_NEGATIVE
+        
+    elif (not comparison["minisat_satisfiable"] and
+          comparison["qubo_satisfiable"]):
+        return FALSE_POSITIVE
+    

util/kSAT.py

@@ -0,0 +1,186 @@
+#!/usr/bin/env python3
+
+import numpy as np
+
+class kSAT:
+    def __init__(self):
+        self.__clauses = []
+        self.__numVariables = 0
+        
+    def getBindings(self):
+        return self.__clauses
+        
+    def getNumberOfClauses(self):
+        return len(self.__clauses)
+        
+    def getClause(self, clauseIndex):
+        return self.__clauses[clauseIndex]
+        
+    def addClause(self, clause):
+        #counting variables (assuming variables are assigned
+        #                    consistently from 1 to numTotalVars)
+        for varBinding in clause:
+            if np.absolute(varBinding) > self.__numVariables:
+                self.__numVariables = np.absolute(varBinding)
+                
+        self.__clauses.append(clause)
+    
+    def getDegreesOfVariables(self):
+        degrees = {}
+        
+        for clause in self.__clauses:
+            for binding in clause:
+                varLabel = abs(binding)
+                
+                if varLabel not in degrees:
+                    degrees[varLabel] = 1
+                else:
+                    degrees[varLabel] += 1
+        
+        return degrees
+                
+    
+    def evaluate(satInstance, assignments):    
+        evaluations = []
+    
+        for assignment in assignments:
+            evaluations.append(satInstance.checkAssignment(assignment))
+        
+        return evaluations
+        
+    def checkAssignment(self, assignment):
+        
+        if not self.__assignmentIsComplete(assignment):
+            print("wrong number of variables in assignment")
+            return False
+
+        for clause in self.__clauses:
+            clauseResult = False
+
+            for binding in clause:
+                
+                varIndex = np.absolute(binding) - 1
+                
+                if ((binding > 0 and assignment[varIndex] == True) or
+                    (binding < 0 and assignment[varIndex] == False)):
+                    clauseResult = True
+
+            if clauseResult == False:
+                return False
+
+        return True
+        
+    def __assignmentIsComplete(self, assignment):
+        if (len(assignment) != self.getNumberOfVariables() or
+            None in assignment):
+            return False
+        
+        return True
+        
+    def getNumberOfVariables(self):
+        return self.__numVariables
+        
+    def toString(self):
+        kSATString = ""
+
+        for clauseIndex in range(len(self.__clauses) - 1):
+            kSATString += self.__kSATClauseToString(clauseIndex)
+            kSATString += " * "
+
+        kSATString += self.__kSATClauseToString(len(self.__clauses) - 1)
+
+        return kSATString
+        
+    def getLableOfBinding(self, clauseIndex, binding):
+        #return  label = "%d%d" % (clauseIndex
+        #                           self.__clauses[clauseIndex][varInClauseIndex])
+        return (clauseIndex, binding)
+        
+    def getConflicts(self):
+        conflicts = []
+        
+        for clauseIndex in range(len(self.__clauses)):
+            clause = self.__clauses[clauseIndex]
+            
+            for binding in clause:
+                
+                clauseToCheckIndex = 0
+                
+                #search for conflict with binding
+                for clauseToCheckIndex in range(clauseIndex, len(self.__clauses)):
+                    
+                    for bindingToCheck in self.__clauses[clauseToCheckIndex]:
+                        if binding == bindingToCheck * -1:
+                            conflLable1 = self.getLableOfBinding(clauseIndex,
+                                                                 binding)
+                            conflLable2 = self.getLableOfBinding(clauseToCheckIndex,
+                                                                bindingToCheck)
+                            conflicts.append((conflLable1, conflLable2))
+                            
+                    
+        return conflicts
+                  
+    def writeDIMACS(self, path):
+        outputFile = open(path, "w")
+        outputFile.write("c A SAT instance\n")
+        outputFile.write("p cnf %d %d \n" % (self.getNumberOfVariables(),
+                                             self.getNumberOfClauses()))
+    
+        for clause in self.getBindings():
+            for binding in clause:
+                outputFile.write("%d " % binding)
+        
+            outputFile.write("0\n")
+        
+        outputFile.close()
+    
+    def readDIMACS(self, path):
+        inputFile = open(path, "r")
+        
+        line = inputFile.readline()
+        
+        self.reset()
+        
+        while line != "":
+            if line[0] != "c" and line[0] != "p":
+                bindings = [int(binding) for binding in line.split()]
+                
+                self.addClause(bindings[:len(bindings) -1])
+            
+            line = inputFile.readline()
+        
+        inputFile.close()
+                
+    
+    def reset(self):
+        self.__clauses = []
+        self.__numVariables = 0
+        
+    def __kSATClauseToString(self, clauseIndex):
+        clause = self.__clauses[clauseIndex]
+        varCount = 0
+        isFirstVar = True;
+    
+        clauseString = "(";
+
+        for weight in clause:
+            varCount += 1
+            
+            if not isFirstVar:
+                clauseString += " + "
+
+            clauseString += self.__kSATVariableToString(weight)
+
+            isFirstVar = False
+
+        clauseString += ")"
+
+        return clauseString
+
+    def __kSATVariableToString(self, weight):
+        name = "x%d" % np.absolute(weight)
+        
+        if weight < 0:
+            return "!" + name
+        else:
+            return name

util/minisatUtils.py

@@ -0,0 +1,34 @@
+def readMinisatResult(path):
+    result = {"assignments": [], "satisfiable": False}
+
+    resultFile = open(path)
+
+    line = resultFile.readline()
+    
+    if line.strip() == "SAT":
+        result["satisfiable"] = True
+        
+        result["assignments"] = __parseVarAssignments(resultFile.readline())
+    
+    resultFile.close()
+    
+    return result
+    
+def __parseVarAssignments(line):
+    assignmentStrings = line.split()
+    
+    trailer = assignmentStrings.pop()
+    
+    assignments = []
+    
+    if trailer == "0":
+        for assignmentStr in assignmentStrings:
+            
+            assignment = True if int(assignmentStr) > 0 else False
+            
+            assignments.append(assignment)
+    else:
+        print("Bad format of assignment string:\n %s", line)
+    
+    return assignments
+            

util/randomSAT.py

@@ -0,0 +1,66 @@
+#!/usr/bin/env python3
+
+import numpy as np
+import random
+import kSAT
+
+def generateRandomKSAT(numberOfClauses,
+                       numberOfVariables,
+                       numberOfVariablesPerClause):
+    
+    instance = kSAT.kSAT()
+    
+    clauses = [[] for i in range(numberOfClauses)]
+    
+    #make sure every variable is bound to at least one clause
+    for varIndex in range(numberOfVariables):
+        
+        clauseIndex = random.choice(range(numberOfClauses))
+        
+        while (len(clauses[clauseIndex]) >= numberOfVariablesPerClause or
+               varIndex + 1 in clauses[clauseIndex]):
+            clauseIndex = random.choice(range(numberOfClauses))
+        
+        clauses[clauseIndex].append(varIndex + 1)
+    
+    #fill in the missing bindings
+    for clause in clauses:
+        tmpClause = []
+        
+        clauseIsUnique = False
+        while not clauseIsUnique:
+        
+            tmpClause = clause.copy()
+        
+            numRemainingBindings = numberOfVariablesPerClause - len(tmpClause)
+            variablesNotYetInClause = __getVariablesNotYetInClause(tmpClause,
+                                                                   numberOfVariables)
+        
+            remainingBindings = random.sample(variablesNotYetInClause,
+                                              numRemainingBindings)
+        
+            tmpClause += remainingBindings
+        
+            for i in range(len(tmpClause)):
+                tmpClause[i] *= random.choice([-1, 1])
+        
+            if tmpClause not in clauses:
+                clauseIsUnique = True
+                
+        instance.addClause(tmpClause)
+                                        
+    return instance
+
+
+def __getVariablesNotYetInClause(clause, numberOfTotalVars):
+    missingVariables = []
+    
+    prevVar = 1;
+    for currVar in clause:
+        missingVariables += list(range(prevVar, currVar))
+        
+        prevVar = currVar + 1
+        
+    missingVariables += list(range(prevVar, numberOfTotalVars + 1))
+    
+    return missingVariables

util/scriptUtils.py

@@ -0,0 +1,86 @@
+import configparser
+import os
+import argparse
+
+def readConfig(configFilePath):
+    config = configparser.ConfigParser()
+    
+    if os.path.isfile(configFilePath):
+        config.read(configFilePath)
+
+    return config
+
+class ArgParser:
+    def __init__(self):
+        self.__flags = {}
+        self.__parser = argparse.ArgumentParser()
+        self.__instanceDirArgSet = False
+        self.__config = None
+        self.__parsedArgs = {}
+        
+    def addArg(self, alias,
+                     shortFlag,
+                     longFlag,
+                     help,
+                     type,
+                     default=None,
+                     ignoreDatabaseConfig=False):
+                         
+        self.__flags[alias] = {"longFlag": longFlag,
+                               "hasDefault": False,
+                               "ignoreDatabaseConfig": ignoreDatabaseConfig}
+        
+        if default != None:
+            self.__flags[alias]["hasDefault"] = True
+            
+        self.__parser.add_argument("-%s" % shortFlag,
+                                   "--%s" % longFlag,
+                                   help=help,
+                                   type=type,
+                                   default=default)
+    
+    def addInstanceDirArg(self):
+        self.__instanceDirArgSet = True
+        
+        self.addArg(alias="datasetDir", shortFlag="d", longFlag="dataset_dir",
+                    help="the base direcotry of the dataset; if this flag is given the others can be omitted",
+                    type=str, ignoreDatabaseConfig=True)
+        
+    
+    def parse(self):
+        self.__parsedArgs = {}
+        args = vars(self.__parser.parse_args())
+        
+        if self.__instanceDirArgSet:
+            self.__config = readConfig(os.path.join(args["dataset_dir"],
+                                                    "dataset.config"))
+        
+        self.__parseDatasetConfig()
+        
+        for alias, flag in self.__flags.items():
+            self.__parsedArgs[alias] = self.__processFlag(args, flag)
+        
+        self.__config = None
+        
+        return self.__parsedArgs
+    
+    def __parseDatasetConfig(self):
+        for flag, value in self.__config["STRUCTURE"].items():
+            self.__parsedArgs[flag] = value
+    
+    def __processFlag(self, args, flag):
+        longFlag = flag["longFlag"]
+        
+        tmpValue = self.__parsedArgs[longFlag] if longFlag in self.__parsedArgs else None
+        
+        if flag["ignoreDatabaseConfig"] == True:
+            tmpValue = None
+        
+        if args[longFlag]:
+            tmpValue = args[longFlag]
+        
+        if tmpValue == None:
+            tmpValue == input("pass arguement %s: " % longFlag)
+        
+        return tmpValue
+