qubo_lab/util/kSAT.py

#!/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 writeJSONLike(self):
        jsonLike = {}

        jsonLike["clauses"] = self.__clauses

        return jsonLike

    def readJSONLike(self, jsonLike):
        self.reset()

        for clause in jsonLike["clauses"]:
            self.addClause(clause)

    
    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