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.
112 lines
3.4 KiB
112 lines
3.4 KiB
#!/usr/bin/env python3
|
|
|
|
from util import SATquboResult
|
|
import argparse
|
|
from util.kSAT import kSAT
|
|
from util import minisat as mSatU
|
|
from util import SATquboResult
|
|
import os
|
|
import json
|
|
|
|
def main():
|
|
args = __parseArguments()
|
|
|
|
|
|
comparison = __compare(args["instancePath"],
|
|
args["minisatResult"],
|
|
args["quboResult"])
|
|
|
|
outputFilePath = os.path.join(args["outputDir"],
|
|
args["instanceFileName"] + ".cmp")
|
|
|
|
__writeComparison(comparison, outputFilePath)
|
|
|
|
|
|
def __parseArguments():
|
|
parser = argparse.ArgumentParser()
|
|
parser.add_argument("-i", "--instance", help="instance file, has to be in DIMACS format", type=str)
|
|
parser.add_argument("-m", "--minisat_result", help="Minisat result file", type=str)
|
|
parser.add_argument("-q", "--qubo_result", help="Qubo result file", type=str)
|
|
parser.add_argument("-o", "--output", help="Directory to store the comparison (optional)", type=str)
|
|
args = parser.parse_args()
|
|
|
|
arguments = {}
|
|
|
|
arguments["instancePath"] = args.instance
|
|
if arguments["instancePath"] == None:
|
|
arguments["instancePath"] = str(input("Instance file: "))
|
|
|
|
#arguments["instancePath"]
|
|
arguments["instanceFileName"] = os.path.basename(arguments["instancePath"])
|
|
|
|
arguments["minisatResult"] = args.minisat_result
|
|
if arguments["minisatResult"] == None:
|
|
arguments["minisatResult"] = str(input("Minisat result file: "))
|
|
|
|
arguments["quboResult"] = args.qubo_result
|
|
if arguments["quboResult"] == None:
|
|
arguments["quboResult"] = str(input("Qubo result file: "))
|
|
|
|
arguments["outputDir"] = args.output
|
|
if arguments["outputDir"] == None:
|
|
arguments["outputDir"] = str(input("Output directory: "))
|
|
|
|
arguments["outputDir"] = os.path.abspath(arguments["outputDir"])
|
|
|
|
|
|
|
|
return arguments
|
|
|
|
def __compare(instancePath, msatResultFile, quboResultFile):
|
|
comparison = {}
|
|
sat = kSAT()
|
|
sat.readDIMACS(instancePath)
|
|
|
|
comparison["instance"] = os.path.basename(instancePath)
|
|
comparison["minisat_satisfiable"] = __getMinisatSatisfiability(msatResultFile)
|
|
comparison["qubo_satisfiable"] = __getQuboSatisfiability(quboResultFile)
|
|
comparison["degrees_of_variables"] = sat.getDegreesOfVariables()
|
|
comparison["conflicts_per_variable"] = __countConflicts(sat.getConflicts())
|
|
|
|
return comparison
|
|
|
|
|
|
def __getMinisatSatisfiability(resultFile):
|
|
minisatResult = mSatU.readMinisatResult(resultFile)
|
|
|
|
return minisatResult["satisfiable"]
|
|
|
|
def __getQuboSatisfiability(resultFile):
|
|
results = SATquboResult.readResultsFromFile(resultFile)
|
|
|
|
for result in results:
|
|
if result.satisfiesInstance():
|
|
return True
|
|
|
|
return False
|
|
|
|
def __writeComparison(comparison, outputFilePath):
|
|
if outputFilePath == None:
|
|
return
|
|
|
|
outputFile = open(outputFilePath, "w+")
|
|
|
|
outputFile.write(json.dumps(comparison) + "\n")
|
|
|
|
outputFile.close()
|
|
|
|
def __countConflicts(conflicts):
|
|
conflictsPerVariable = {}
|
|
|
|
for conflict in conflicts:
|
|
varLabel = abs(conflict[0][1])
|
|
|
|
if varLabel not in conflictsPerVariable:
|
|
conflictsPerVariable[varLabel] = 1
|
|
else:
|
|
conflictsPerVariable[varLabel] += 1
|
|
|
|
return conflictsPerVariable
|
|
|
|
if __name__ == "__main__":
|
|
main()
|