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.
168 lines
4.8 KiB
168 lines
4.8 KiB
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
|