You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
207 lines
6.0 KiB
207 lines
6.0 KiB
#!/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"] = []
|
|
|
|
for clause in self.__clauses:
|
|
tmpClause = []
|
|
|
|
for literal in clause:
|
|
tmpClause.append(int(literal))
|
|
|
|
jsonLike["clauses"].append(tmpClause)
|
|
|
|
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
|