From bc5de0c9945445c70a4a7577ba7e6f2d960296d9 Mon Sep 17 00:00:00 2001 From: Tom Date: Wed, 19 Dec 2018 21:41:19 +0100 Subject: [PATCH] init --- balanceDataset.py | 1 + collectCmpStatus.py | 121 +++++++++++ compareMinisatAndWMISresult.py | 112 +++++++++++ compareRuns.py | 40 ++++ comparisonStats.py | 141 +++++++++++++ createEmptyDataset.py | 51 +++++ generateRandomKsatDataSet.py | 61 ++++++ runWMISquboOnSatInstance.py | 115 +++++++++++ satUnsatConflictsPerVariableStats.py | 290 +++++++++++++++++++++++++++ satUnsatDegreeStats.py | 256 +++++++++++++++++++++++ testMinisatResults.py | 47 +++++ testRandomSat.py | 22 ++ testSAT2QUBO.py | 13 ++ util/SAT2QUBO.py | 105 ++++++++++ util/SATquboResult.py | 168 ++++++++++++++++ util/compare.py | 23 +++ util/kSAT.py | 186 +++++++++++++++++ util/minisatUtils.py | 34 ++++ util/randomSAT.py | 66 ++++++ util/scriptUtils.py | 86 ++++++++ verifyWMISresult.py | 38 ++++ 21 files changed, 1976 insertions(+) create mode 100644 balanceDataset.py create mode 100755 collectCmpStatus.py create mode 100755 compareMinisatAndWMISresult.py create mode 100755 compareRuns.py create mode 100755 comparisonStats.py create mode 100755 createEmptyDataset.py create mode 100755 generateRandomKsatDataSet.py create mode 100755 runWMISquboOnSatInstance.py create mode 100755 satUnsatConflictsPerVariableStats.py create mode 100755 satUnsatDegreeStats.py create mode 100755 testMinisatResults.py create mode 100755 testRandomSat.py create mode 100755 testSAT2QUBO.py create mode 100644 util/SAT2QUBO.py create mode 100644 util/SATquboResult.py create mode 100644 util/compare.py create mode 100644 util/kSAT.py create mode 100644 util/minisatUtils.py create mode 100644 util/randomSAT.py create mode 100644 util/scriptUtils.py create mode 100755 verifyWMISresult.py diff --git a/balanceDataset.py b/balanceDataset.py new file mode 100644 index 0000000..8b13789 --- /dev/null +++ b/balanceDataset.py @@ -0,0 +1 @@ + diff --git a/collectCmpStatus.py b/collectCmpStatus.py new file mode 100755 index 0000000..a951c2b --- /dev/null +++ b/collectCmpStatus.py @@ -0,0 +1,121 @@ +#!/usr/bin/env python3 + +import argparse +import os +import glob +import json +import numpy as np +import matplotlib.pyplot as plt +import configparser +import scriptUtils + +def main(): + args = __parseArguments() + + __stats(args["comparisonDir"], args["outputDir"]) + + +def __parseArguments(): + parser = scriptUtils.ArgParser() + + parser.addInstanceDirArg() + + parser.addArg(alias="comparisonDir", shortFlag="c", longFlag="comparison_dir", + help="the direcotry with all comparison files", type=str) + + parser.addArg(alias="outputDir", shortFlag="s", longFlag="comparison_stats_dir", + help="Directory to store the stats", type=str) + + arguments = parser.parse() + + arguments["datasetDir"] = os.path.abspath(arguments["datasetDir"]) + + arguments["comparisonDir"] = os.path.join(arguments["datasetDir"], + arguments["comparisonDir"]) + + arguments["outputDir"] = os.path.join(arguments["datasetDir"], + arguments["outputDir"]) + + return arguments + +def __stats(comparisonDir, outputDir): + runs = glob.glob(os.path.join(comparisonDir, "run*")) + + for run in runs: + + stats = __collectStats(run) + + runOutputDir = os.path.join(outputDir, os.path.basename(run)) + + __writeStats(stats, runOutputDir) + +def __collectStats(comparisonDir): + files = glob.glob(os.path.join(comparisonDir, "*.cmp")) + + stats = {} + stats["match"] = 0 + stats["false_positive"] = 0 + stats["false_negative"] = 0 + stats["unsat"] = 0 + + for path in files: + + comparison = __readComparison(path) + + minisat_satisfiable = comparison["minisat_satisfiable"] + qubo_satisfiable = comparison["qubo_satisfiable"] + + if minisat_satisfiable == qubo_satisfiable: + stats["match"] += 1 + elif minisat_satisfiable == False and qubo_satisfiable == True: + stats["false_positive"] += 1 + elif minisat_satisfiable == True and qubo_satisfiable == False: + stats["false_negative"] += 1 + + if not minisat_satisfiable: + stats["unsat"] += 1 + + return stats + +def __readComparison(path): + cmpFile = open(path, "r") + comparison = json.load(cmpFile) + cmpFile.close() + + return comparison + + +def __writeStats(stats, outputDir): + if not os.path.exists(outputDir): + os.makedirs(outputDir) + + + fig = plt.figure() + ax = fig.add_subplot(111) + + numInstances = stats["match"] + stats["false_negative"] + stats["false_positive"] + + matchBar = ax.bar(x=0, height=stats["match"]) + + falsePositiveBar = ax.bar(x=1, height=stats["false_positive"]) + falseNegativeBar = ax.bar(x=1, + height=stats["false_negative"], + bottom=stats["false_positive"]) + + ax.axhline(y=stats["match"], linestyle="--", color="gray") + ax.axhline(y=stats["false_negative"], linestyle="--", color="gray") + + + plt.ylabel("SAT Instanzen") + plt.title("Verlgeich Minisat / WMIS qubo mit qbsolv") + plt.xticks([0, 1], ("Gleiches Ergebnis", "Unterschiedliches Ergebnis")) + plt.yticks([0, stats["match"], stats["false_negative"], numInstances]) + plt.legend((matchBar, falsePositiveBar, falseNegativeBar), + ("Gleiches Ergebnis", + "False Positive", + "False Negative")) + + plt.savefig(os.path.join(outputDir, "stats.png")) + +if __name__ == "__main__": + main() diff --git a/compareMinisatAndWMISresult.py b/compareMinisatAndWMISresult.py new file mode 100755 index 0000000..c500cc7 --- /dev/null +++ b/compareMinisatAndWMISresult.py @@ -0,0 +1,112 @@ +#!/usr/bin/env python3 + +import SATquboResult +import argparse +from kSAT import kSAT +import minisatUtils as mSatU +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() diff --git a/compareRuns.py b/compareRuns.py new file mode 100755 index 0000000..57915ca --- /dev/null +++ b/compareRuns.py @@ -0,0 +1,40 @@ +#!/usr/bin/env python3 + +import scriptUtils +import compare +import glob +import os + +def __main(): + args = __parseArguments() + + __compareRuns(args) + +def __parseArguments(): + parser = scriptUtils.ArgParser() + + parser.addInstanceDirArg() + + return parser.parse() + +def __compareRuns(args): + instancePaths = glob.glob(os.path.join( + os.path.join(args["dataset_dir"], + args["instance_dir"]), + "*.dimacs")) + runDirs = glob.glob(os.path.join( + os.path.join(args["dataset_dir"], + args["wmis_result_dir"]), + "run*")) + + for path in instancePaths: + __compareRunsOfInstance(path, runDirs) + +def __compareRunsOfInstance(instancePath, runDirs): + instanceName = os.path.basename(instancePath) + + with open(instancePath) as instanceFile: + + +if __name__ == "__main__": + __main() diff --git a/comparisonStats.py b/comparisonStats.py new file mode 100755 index 0000000..f0d476f --- /dev/null +++ b/comparisonStats.py @@ -0,0 +1,141 @@ +#!/usr/bin/env python3 + +import argparse +import os +import glob +import json +import numpy as np +import matplotlib.pyplot as plt +import configparser +import scriptUtils + +def main(): + args = __parseArguments() + + __stats(args["comparisonDir"], args["outputDir"]) + + +def __parseArguments(): + parser = scriptUtils.ArgParser() + + parser.addInstanceDirArg() + + parser.addArg(alias="comparisonDir", shortFlag="c", longFlag="comparison_dir", + help="the direcotry with all comparison files", type=str) + + parser.addArg(alias="outputDir", shortFlag="s", longFlag="comparison_stats_dir", + help="Directory to store the stats", type=str) + + arguments = parser.parse() + + arguments["datasetDir"] = os.path.abspath(arguments["datasetDir"]) + + arguments["comparisonDir"] = os.path.join(arguments["datasetDir"], + arguments["comparisonDir"]) + + arguments["outputDir"] = os.path.join(arguments["datasetDir"], + arguments["outputDir"]) + + return arguments + +def __stats(comparisonDir, outputDir): + runs = glob.glob(os.path.join(comparisonDir, "run*")) + + for run in runs: + + stats = __collectStats(run) + + print(stats) + + runOutputDir = os.path.join(outputDir, os.path.basename(run)) + + __writeStats(stats, runOutputDir) + +def __collectStats(comparisonDir): + files = glob.glob(os.path.join(comparisonDir, "*.cmp")) + + stats = {} + stats["match"] = {"count": 0, + "instances": []} + stats["false_positive"] = {"count": 0, + "instances": []} + stats["false_negative"] = {"count": 0, + "instances": []} + stats["unsat"] = {"count": 0, + "instances": []} + + for path in files: + + comparison = __readComparison(path) + + minisat_satisfiable = comparison["minisat_satisfiable"] + qubo_satisfiable = comparison["qubo_satisfiable"] + + instanceName = str(os.path.basename(path)).split(".")[0] + + if minisat_satisfiable == qubo_satisfiable: + stats["match"]["count"] += 1 + stats["match"]["instances"].append(instanceName) + + elif minisat_satisfiable == False and qubo_satisfiable == True: + stats["false_positive"]["count"] += 1 + stats["false_positive"]["instances"].append(instanceName) + + elif minisat_satisfiable == True and qubo_satisfiable == False: + stats["false_negative"]["count"] += 1 + stats["false_negative"]["instances"].append(instanceName) + + if not minisat_satisfiable: + stats["unsat"]["count"] += 1 + stats["unsat"]["instances"].append(instanceName) + + return stats + +def __readComparison(path): + cmpFile = open(path, "r") + comparison = json.load(cmpFile) + cmpFile.close() + + return comparison + + +def __writeStats(stats, outputDir): + if not os.path.exists(outputDir): + os.makedirs(outputDir) + + with open(os.path.join(outputDir,"statusCollection"), "w+") as statusFile: + statusFile.write(json.dumps(stats)) + + fig = plt.figure() + ax = fig.add_subplot(111) + + matchCount = stats["match"]["count"] + falseNegativeCount = stats["false_negative"]["count"] + falsePositiveCount = stats["false_positive"]["count"] + + numInstances = matchCount + falseNegativeCount + falsePositiveCount + + matchBar = ax.bar(x=0, height=matchCount) + + falsePositiveBar = ax.bar(x=1, height=falsePositiveCount) + falseNegativeBar = ax.bar(x=1, + height=falseNegativeCount, + bottom=falsePositiveCount) + + ax.axhline(y=matchCount, linestyle="--", color="gray") + ax.axhline(y=falseNegativeCount, linestyle="--", color="gray") + + + plt.ylabel("SAT Instanzen") + plt.title("Verlgeich Minisat / WMIS qubo mit qbsolv") + plt.xticks([0, 1], ("Gleiches Ergebnis", "Unterschiedliches Ergebnis")) + plt.yticks([0, matchCount, falseNegativeCount, numInstances]) + plt.legend((matchBar, falsePositiveBar, falseNegativeBar), + ("Gleiches Ergebnis", + "False Positive", + "False Negative")) + + plt.savefig(os.path.join(outputDir, "stats.png")) + +if __name__ == "__main__": + main() diff --git a/createEmptyDataset.py b/createEmptyDataset.py new file mode 100755 index 0000000..dfb04a5 --- /dev/null +++ b/createEmptyDataset.py @@ -0,0 +1,51 @@ +#!/usr/bin/env python3 + +import os +import configparser +import argparse + +def main(): + args = __parseArguments(); + + config = configparser.ConfigParser() + + dirs = {"INSTANCE_DIR": "instances", + "MINISAT_RESULT_DIR": "minisatResults", + "WMIS_RESULT_DIR": "wmisResults", + "COMPARISON_DIR": "comparison"} + + dirs["COMPARISON_STATS_DIR"] = os.path.join(dirs["COMPARISON_DIR"], + "stats") + + config["STRUCTURE"] = dirs + + os.mkdir(args["dir"]) + os.mkdir(os.path.join(args["dir"], dirs["INSTANCE_DIR"])) + os.mkdir(os.path.join(args["dir"], dirs["MINISAT_RESULT_DIR"])) + os.mkdir(os.path.join(args["dir"], dirs["WMIS_RESULT_DIR"])) + os.mkdir(os.path.join(args["dir"], dirs["COMPARISON_DIR"])) + os.mkdir(os.path.join(args["dir"], dirs["COMPARISON_STATS_DIR"])) + + with open(os.path.join(args["dir"], "dataset.config"), "w") as configfile: + config.write(configfile) + configfile.close() + + +def __parseArguments(): + parser = argparse.ArgumentParser() + parser.add_argument("-d", "--directory", help="the direcotry for the new dataset", type=str) + args = parser.parse_args() + + arguments = {} + print(args) + + arguments["dir"] = args.directory + if arguments["dir"] == None: + arguments["dir"] = str(input("Directory: ")) + + arguments["dir"] = os.path.abspath(arguments["dir"]) + return arguments + + +if __name__ == "__main__": + main() diff --git a/generateRandomKsatDataSet.py b/generateRandomKsatDataSet.py new file mode 100755 index 0000000..9d28e14 --- /dev/null +++ b/generateRandomKsatDataSet.py @@ -0,0 +1,61 @@ +#!/usr/bin/env python3 + +import randomSAT +import kSAT +import argparse +import configparser +import os + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument("-d", "--base_directory", help="the base directorey of the new dataset; should contain a dataset.config file", type=str) + parser.add_argument("-i", "--instances", help="number of random kSAT instances", type=int) + parser.add_argument("-v", "--variables", help="number of variables in ksat instances", type=int) + parser.add_argument("-c", "--clauses", help="number of clauses in ksat instances", type=int) + parser.add_argument("--variables_per_clause", help="variables per clause in ksat instances", type=int, default=3) + parser.add_argument("-o", "--output", help="output directory", type=str) + args = parser.parse_args() + + baseDir = args.base_directory + if baseDir != None: + config = __readConfig(os.path.join(baseDir, "dataset.config")); + + numberOfVariables = args.variables + if numberOfVariables == None: + numberOfVariables = int(input("Number of variables per instance: ")) + + numberOfClauses = args.clauses + if numberOfClauses == None: + numberOfClauses = int(input("Number of clauses per instance: ")) + + numberOfInstances = args.instances + if numberOfInstances == None: + numberOfInstances = int(input("Number of instances: ")) + + instanceDir = None + if "instance_dir" in config["STRUCTURE"]: + instanceDir = os.path.join(baseDir, config["STRUCTURE"]["instance_dir"]) + elif args.output != None: + instanceDir = args.output + elif args.output == None: + instanceDir = str(input("output directory: ")) + + for i in range(numberOfInstances): + ksatInstance = randomSAT.generateRandomKSAT(numberOfClauses, + numberOfVariables, + args.variables_per_clause) + + instanceFilePath = os.path.join(instanceDir, "instance_%d.dimacs" % (i)) + + ksatInstance.writeDIMACS(instanceFilePath) + +def __readConfig(configFilePath): + config = configparser.ConfigParser() + + if os.path.isfile(configFilePath): + config.read(configFilePath) + + return config + +if __name__ == "__main__": + main() diff --git a/runWMISquboOnSatInstance.py b/runWMISquboOnSatInstance.py new file mode 100755 index 0000000..e49ebb2 --- /dev/null +++ b/runWMISquboOnSatInstance.py @@ -0,0 +1,115 @@ +#!/usr/bin/env python3 + +import kSAT +import SAT2QUBO +from SATquboResult import SATquboResult +import argparse +from dwave_qbsolv import QBSolv +import os +import collections +import json +from tqdm import tqdm +import scriptUtils + +def main(): + arguments = __parseArguments() + + satInstance = kSAT.kSAT() + + print("reading ksat...") + satInstance.readDIMACS(arguments["instancePath"]) + + print() + result = __runWMISquboOnSatInstance(satInstance) + + resultPath = os.path.join( + os.path.join(arguments["resultDir"], + "run%d" % arguments["run"]), + "%s.out" % arguments["instanceFileName"]) + + print() + print("writing results to file...") + __writeResult(result, resultPath) + +def __parseArguments(): + parser = scriptUtils.ArgParser() + + parser.addInstanceDirArg() + parser.addArg(alias="instancePath", shortFlag="i", longFlag="instance", + help="instance file, has to be in DIMACS format", type=str) + + parser.addArg(alias="resultDir", shortFlag="o", longFlag="wmis_result_dir", + help="the wmis result directory", type=str, + ignoreDatabaseConfig=False) + + parser.addArg(alias="run", shortFlag="r", longFlag="run", + help="results will get saved unter [instance]_[run].out", type=int) + + arguments = parser.parse() + + arguments["instanceFileName"] = os.path.basename(arguments["instancePath"]) + + return arguments + + + +def __runWMISquboOnSatInstance(satInstance): + print("generating wmis qubo...") + qubo = SAT2QUBO.WMISdictQUBO(satInstance) + + print() + print("running gbsolv...") + qbresult = QBSolv().sample_qubo(Q=qubo, find_max=True) + + print() + print("packing results...") + results = __packResults(satInstance, qbresult) + + return results + +def __packResults(satInstance, qbresult): + results = [] + + samples = list(qbresult.samples()) + occurrences = qbresult.data_vectors["num_occurrences"] + + for i in tqdm(range(len(samples))): + quboResult = __satQuboResultFromSample(samples[i]) + quboResult.setOccurrences(occurrences[i]) + quboResult.setSatisfiesInstance(satInstance) + + results.append(quboResult) + + return results + + +def __writeResult(results, resultPath): + resultDir = os.path.dirname(resultPath) + + if not os.path.exists(resultDir): + os.makedirs(resultDir) + + resultFile = open(resultPath, "w+") + + for result in tqdm(results): + + resultFile.write(json.dumps(result.toPrimitive())) + resultFile.write("\n\n") + + resultFile.close() + +def __satQuboResultFromSample(sample): + result = SATquboResult() + + for binding in sample: + isActive = True if sample[binding] == 1 else False + + result.addBinding(binding, isActive) + #if sample[binding] == 1: + #result.addActiveBinding(binding) + + return result + + +if __name__ == "__main__": + main() diff --git a/satUnsatConflictsPerVariableStats.py b/satUnsatConflictsPerVariableStats.py new file mode 100755 index 0000000..5a30d4e --- /dev/null +++ b/satUnsatConflictsPerVariableStats.py @@ -0,0 +1,290 @@ +#!/usr/bin/env python3 + +import argparse +import os +import glob +import json +import numpy as np +import matplotlib.pyplot as plt +import collections +import scriptUtils + +def main(): + args = __parseArguments() + + print(args) + + __stats(args["comparisonDir"], args["outputDir"]) + + +def __parseArguments(): + argParser = scriptUtils.ArgParser() + + argParser.addInstanceDirArg(); + argParser.addArg(alias="comparisonDir", shortFlag="c", longFlag="comparison_dir", + help="the direcotry with all comparison files", type=str) + + argParser.addArg(alias="outputDir", shortFlag="o", longFlag="comparison_stats_dir", + help="Directory to store the stats", type=str) + + return argParser.parse() + +def __stats(comparisonDir, outputDir): + stats = __collectStats(comparisonDir) + + __writeStats(stats, outputDir) + +def __collectStats(comparisonDir): + files = glob.glob(os.path.join(comparisonDir, "*.cmp")) + + stats = [] + + for path in files: + + comparison = __readComparison(path) + + stats.append(__processSingleInstance(comparison)) + + return stats + + +def __processSingleInstance(comparison): + instanceStats = {} + + conflicts = comparison["conflicts_per_variable"] + conflictArr = np.array(list(conflicts.values())) + + instanceStats["conflicts_per_variable_mean"] = conflictArr.mean() + instanceStats["conflicts_per_variable_median"] = np.median(conflictArr) + instanceStats["conflicts_per_variable_std_dev"] = np.std(conflictArr) + instanceStats["conflicts_per_variable_max"] = conflictArr.max() + instanceStats["conflicts_per_variable_min"] = conflictArr.min() + instanceStats["conflicts_per_instance"] = np.sum(conflictArr) + instanceStats["raw_conflicts"] = list(conflictArr) + instanceStats["conflicts_to_degree_per_variable"] = __calcConflictsToDegree(conflicts, + comparison["degrees_of_variables"]) + + + if comparison["minisat_satisfiable"]: + if __instanceIsFalseNegative(comparison): + instanceStats["result"] = "false_negative" + else: + instanceStats["result"] = "satisfiable" + else: + instanceStats["result"] = "unsatisfiable" + + return instanceStats + +def __calcConflictsToDegree(degreesPerVariable, conflictsPerVariable): + conflictsToDegreePerVariable = [] + + for varLabel, degree in degreesPerVariable.items(): + conflicts = conflictsPerVariable[varLabel] + cnflToDeg = conflicts / (float(degree) / 2.0)**2 + + if cnflToDeg <= 1: + conflictsToDegreePerVariable.append(cnflToDeg) + + return conflictsToDegreePerVariable + +def __instanceIsFalseNegative(comparison): + return (comparison["minisat_satisfiable"] == True and + comparison["qubo_satisfiable"] == False) + + +def __readComparison(path): + cmpFile = open(path, "r") + comparison = json.load(cmpFile) + cmpFile.close() + + return comparison + + +def __writeStats(stats, outputDir): + + data = __seperateMatchesAndFalseNegatives(stats) + + overviewFig = __createOverviewFig(data) + meanFig = __createSingleStatFig(data["mean"], "Conflicts per variable mean") + medianFig = __createSingleStatFig(data["median"], "Conflicts per variable median") + maxFig = __createSingleStatFig(data["max"], "Conflicts per variable max") + minFig = __createSingleStatFig(data["min"], "Conflicts per variable min") + stdDevFig = __createSingleStatFig(data["std_dev"], "Conflicts per variable\nstandard deviation") + cnflPerInstFig = __createSingleStatFig(data["cnfl_per_inst"], "Conflicts per instance") + cnflDegFig1 = __createSingleStatFig(data["cnflDeg"], "Conflicts in relation to degree", showfliers=False); + cnflDegFig2 = __createSingleStatFig(data["cnflDeg"], "Conflicts in relation to degree", showfliers=True); + + histFig = __createHistogramFig(data, "raw", "Conflict per variable"); + #cnflDegHistFig = __createHistogramFig(data, "cnflDeg", "Conflicts in relation to degree"); + + __setBatchXticks(figures=[overviewFig, + meanFig, + medianFig, + maxFig, + minFig, + stdDevFig, + cnflPerInstFig, + cnflDegFig1, + cnflDegFig2], + ticks=[1, 2, 3], + labels=["satisfiable", + "false negative", + "unsatisfiable"]) + + __setBatchXtickLabelRotation(figures=[overviewFig, + meanFig, + medianFig, + maxFig, + minFig, + stdDevFig, + cnflPerInstFig, + cnflDegFig1, + cnflDegFig2], + rotation=30) + + + overviewFig.savefig(os.path.join(outputDir, "conflicts_overview.png")) + meanFig.savefig(os.path.join(outputDir, "conflicts_mean.png")) + medianFig.savefig(os.path.join(outputDir, "conflicts_median.png")) + maxFig.savefig(os.path.join(outputDir, "conflicts_max.png")) + minFig.savefig(os.path.join(outputDir, "conflicts_min.png")) + stdDevFig.savefig(os.path.join(outputDir, "conflicts_std_dev.png")) + cnflPerInstFig.savefig(os.path.join(outputDir, "conflicts_per_instance.png")) + histFig.savefig(os.path.join(outputDir, "conflicts_per_var_hist.png")) + cnflDegFig1.savefig(os.path.join(outputDir, "conflicts_in_relation_to_degree_1.png")) + cnflDegFig2.savefig(os.path.join(outputDir, "conflicts_in_relation_to_degree_2.png")) + + #plt.show(overviewFig) + +def __createOverviewFig(data): + fig = plt.figure() + + ax0 = fig.add_subplot(141,) + ax0.boxplot([data["mean"]["satisfiable"], + data["mean"]["false_negative"], + data["mean"]["unsatisfiable"]]) + ax0.set_title("mean") + + ax1 = fig.add_subplot(142, sharey=ax0) + ax1.boxplot([data["median"]["satisfiable"], + data["median"]["false_negative"], + data["median"]["unsatisfiable"]]) + ax1.set_title("median") + + ax2 = fig.add_subplot(143, sharey=ax0) + ax2.boxplot([data["max"]["satisfiable"], + data["max"]["false_negative"], + data["max"]["unsatisfiable"]]) + ax2.set_title("max degree") + + ax3 = fig.add_subplot(144, sharey=ax0) + ax3.boxplot([data["min"]["satisfiable"], + data["min"]["false_negative"], + data["min"]["unsatisfiable"]]) + ax3.set_title("min degree") + + + fig.set_size_inches(12, 8) + fig.suptitle("Conflicts per variable overview", fontsize=16) + + return fig + +def __createHistogramFig(data, subDataSet, title): + fig = plt.figure() + + bins = int(max(data[subDataSet]["satisfiable"]) / 5) + + ax0 = fig.add_subplot(321) + ax0.hist(data[subDataSet]["satisfiable"], bins=bins) + ax0_2 = fig.add_subplot(322) + ax0_2.boxplot(data[subDataSet]["satisfiable"], vert=False) + + ax1 = fig.add_subplot(323, sharex=ax0) + ax1.hist(data[subDataSet]["false_negative"], bins=bins) + ax1_2 = fig.add_subplot(324, sharex=ax0_2) + ax1_2.boxplot(data[subDataSet]["false_negative"], vert=False) + + ax2 = fig.add_subplot(325, sharex=ax0) + ax2.hist(data[subDataSet]["unsatisfiable"], bins=bins) + ax2_2 = fig.add_subplot(326, sharex=ax0_2) + ax2_2.boxplot(data[subDataSet]["unsatisfiable"], vert=False) + + fig.set_size_inches(14, 10) + fig.suptitle(title, fontsize=16) + + return fig + +def __createSingleStatFig(subDataset, title, showfliers=True): + fig = plt.figure() + + ax = fig.add_subplot(111) + ax.boxplot([subDataset["satisfiable"], + subDataset["false_negative"], + subDataset["unsatisfiable"]], showfliers=showfliers) + + fig.set_size_inches(3.5, 8) + fig.suptitle(title, fontsize=16) + + return fig + +def __setBatchXticks(figures, ticks, labels): + for fig in figures: + plt.setp(fig.get_axes(), xticks=ticks, xticklabels=labels) + +def __setBatchXtickLabelRotation(figures, rotation): + for fig in figures: + for ax in fig.get_axes(): + plt.setp(ax.get_xticklabels(), rotation=rotation) + + + +def __seperateMatchesAndFalseNegatives(stats): + data = {} + data["mean"] = {"false_negative": [], + "satisfiable": [], + "unsatisfiable": []} + + data["median"] = {"false_negative": [], + "satisfiable": [], + "unsatisfiable": []} + + data["std_dev"] = {"false_negative": [], + "satisfiable": [], + "unsatisfiable": []} + + data["max"] = {"false_negative": [], + "satisfiable": [], + "unsatisfiable": []} + + data["min"] = {"false_negative": [], + "satisfiable": [], + "unsatisfiable": []} + + data["cnfl_per_inst"] = {"false_negative": [], + "satisfiable": [], + "unsatisfiable": []} + + data["raw"] = {"false_negative": [], + "satisfiable": [], + "unsatisfiable": []} + + data["cnflDeg"] = {"false_negative": [], + "satisfiable": [], + "unsatisfiable": []} + + for instance in stats: + target = instance["result"] + + data["mean"][target].append(instance["conflicts_per_variable_mean"]) + data["median"][target].append(instance["conflicts_per_variable_median"]) + data["std_dev"][target].append(instance["conflicts_per_variable_std_dev"]) + data["max"][target].append(instance["conflicts_per_variable_max"]) + data["min"][target].append(instance["conflicts_per_variable_min"]) + data["cnfl_per_inst"][target].append(instance["conflicts_per_instance"]) + data["raw"][target].extend(instance["raw_conflicts"]) + data["cnflDeg"][target].extend(instance["conflicts_to_degree_per_variable"]) + + return data + +if __name__ == "__main__": + main() diff --git a/satUnsatDegreeStats.py b/satUnsatDegreeStats.py new file mode 100755 index 0000000..e1804b0 --- /dev/null +++ b/satUnsatDegreeStats.py @@ -0,0 +1,256 @@ +#!/usr/bin/env python3 + +import argparse +import os +import glob +import json +import numpy as np +import matplotlib.pyplot as plt +import collections + +def main(): + args = __parseArguments() + + __stats(args["comparisonDir"], args["outputDir"]) + + +def __parseArguments(): + parser = argparse.ArgumentParser() + parser.add_argument("-d", "--directory", help="the direcotry with all comparison files", type=str) + parser.add_argument("-o", "--output", help="Directory to store the stats", type=str) + args = parser.parse_args() + + arguments = {} + print(args) + + arguments["comparisonDir"] = args.directory + if arguments["comparisonDir"] == None: + arguments["comparisonDir"] = str(input("Comparison directory: ")) + + arguments["comparisonDir"] = os.path.abspath(arguments["comparisonDir"]) + + arguments["outputDir"] = args.output + if arguments["outputDir"] == None: + arguments["outputDir"] = str(input("Output directory: ")) + + arguments["outputDir"] = os.path.abspath(arguments["outputDir"]) + + return arguments + +def __stats(comparisonDir, outputDir): + stats = __collectStats(comparisonDir) + + __writeStats(stats, outputDir) + +def __collectStats(comparisonDir): + files = glob.glob(os.path.join(comparisonDir, "*.cmp")) + + stats = [] + + for path in files: + + comparison = __readComparison(path) + + stats.append(__processSingleInstance(comparison)) + + return stats + + +def __processSingleInstance(comparison): + instanceStats = {} + + degrees = comparison["degrees_of_variables"] + degreeArr = np.array(list(degrees.values())) + + instanceStats["degree_of_variables_mean"] = degreeArr.mean() + instanceStats["degree_of_variables_median"] = np.median(degreeArr) + instanceStats["degree_of_variables_std_dev"] = np.std(degreeArr) + instanceStats["degree_of_variables_max"] = degreeArr.max() + instanceStats["degree_of_variables_min"] = degreeArr.min() + instanceStats["variables_per_degree"] = __getVarsPerDegree(degreeArr) + + if comparison["minisat_satisfiable"]: + if __instanceIsFalseNegative(comparison): + instanceStats["result"] = "false_negative" + else: + instanceStats["result"] = "satisfiable" + else: + instanceStats["result"] = "unsatisfiable" + + return instanceStats + +def __instanceIsFalseNegative(comparison): + return (comparison["minisat_satisfiable"] == True and + comparison["qubo_satisfiable"] == False) + +def __getVarsPerDegree(degreeArr): + degCount = collections.Counter(degreeArr) + + varsPerDegree = {} + + for degree in degCount: + varsPerDegree[degree] = degCount[degree] + + return varsPerDegree + + +def __readComparison(path): + cmpFile = open(path, "r") + comparison = json.load(cmpFile) + cmpFile.close() + + return comparison + + +def __writeStats(stats, outputDir): + + fig1 = plt.figure() + + data = __seperateMatchesAndFalseNegatives(stats) + + ax0 = fig1.add_subplot(141,) + ax0.boxplot([data["mean"]["satisfiable"], + data["mean"]["false_negative"], + data["mean"]["unsatisfiable"]]) + ax0.set_title("mean") + + ax1 = fig1.add_subplot(142, sharey=ax0) + ax1.boxplot([data["median"]["satisfiable"], + data["median"]["false_negative"], + data["median"]["unsatisfiable"]]) + ax1.set_title("median") + + ax2 = fig1.add_subplot(143, sharey=ax0) + ax2.boxplot([data["max"]["satisfiable"], + data["max"]["false_negative"], + data["max"]["unsatisfiable"]]) + ax2.set_title("max degree") + + ax3 = fig1.add_subplot(144, sharey=ax0) + ax3.boxplot([data["min"]["satisfiable"], + data["min"]["false_negative"], + data["min"]["unsatisfiable"]]) + ax3.set_title("min degree") + + + fig2 = plt.figure() + ax4 = fig2.add_subplot(111) + ax4.boxplot([data["std_dev"]["satisfiable"], + data["std_dev"]["false_negative"], + data["std_dev"]["unsatisfiable"]]) + ax4.set_title("standard deviation") + + + _BINS_ = 23 + + fig3 = plt.figure() + ax5 = fig3.add_subplot(311) + varsPerDegreeSat = __accumulateVarsPerDegree(data["vars_per_degree"]["satisfiable"]) + ax5.hist(varsPerDegreeSat, density=True, bins=_BINS_) + + ax6 = fig3.add_subplot(312, sharex=ax5) + varsPerDegreeFP = __accumulateVarsPerDegree(data["vars_per_degree"]["false_negative"]) + ax6.hist(varsPerDegreeFP, density=True, bins=_BINS_) + + ax7 = fig3.add_subplot(313, sharex=ax6) + varsPerDegreeUnsat = __accumulateVarsPerDegree(data["vars_per_degree"]["unsatisfiable"]) + ax7.hist(varsPerDegreeUnsat, density=True, bins=_BINS_) + + + plt.setp([ax0, ax1, ax2, ax3, ax4], xticks=[1, 2, 3], xticklabels=["satisfiable", + "false negative", + "unsatisfiable"]) + plt.setp(ax0.get_xticklabels(), rotation=45) + plt.setp(ax1.get_xticklabels(), rotation=45) + plt.setp(ax2.get_xticklabels(), rotation=45) + plt.setp(ax3.get_xticklabels(), rotation=45) + plt.setp(ax4.get_xticklabels(), rotation=45) + fig1.set_size_inches(12, 8) + fig1.suptitle("Degrees of variables", fontsize=16) + + fig2.set_size_inches(4, 8) + + fig3.set_size_inches(5, 12) + + fig1.savefig(os.path.join(outputDir, "degrees1.png")) + fig2.savefig(os.path.join(outputDir, "degrees2.png")) + fig3.savefig(os.path.join(outputDir, "degrees3.png")) + + plt.show() + + +def __accumulateVarsPerDegree(listOfVarsPerDegreeDicts): + accumulated = [] + + for instance in listOfVarsPerDegreeDicts: + for degree in instance: + accumulated += [degree] * instance[degree] + + return accumulated + +def __compressVarsPerDegree(listOfVarsPerDegreeDicts): + compressed = {} + + countOfVars = 0 + + for instance in listOfVarsPerDegreeDicts: + for degree in instance: + if degree in compressed: + compressed[degree] += float(instance[degree]) + else: + compressed[degree] = float(instance[degree]) + + countOfVars += instance[degree] + + check = 0 + for degree in compressed: + compressed[degree] /= countOfVars + + check += compressed[degree] + + + print("check: ", check) + + return compressed + + +def __seperateMatchesAndFalseNegatives(stats): + data = {} + data["mean"] = {"false_negative": [], + "satisfiable": [], + "unsatisfiable": []} + + data["median"] = {"false_negative": [], + "satisfiable": [], + "unsatisfiable": []} + + data["std_dev"] = {"false_negative": [], + "satisfiable": [], + "unsatisfiable": []} + + data["max"] = {"false_negative": [], + "satisfiable": [], + "unsatisfiable": []} + + data["min"] = {"false_negative": [], + "satisfiable": [], + "unsatisfiable": []} + + data["vars_per_degree"] = {"false_negative": [], + "satisfiable": [], + "unsatisfiable": []} + + for instance in stats: + target = instance["result"] + + data["mean"][target].append(instance["degree_of_variables_mean"]) + data["median"][target].append(instance["degree_of_variables_median"]) + data["std_dev"][target].append(instance["degree_of_variables_std_dev"]) + data["max"][target].append(instance["degree_of_variables_max"]) + data["min"][target].append(instance["degree_of_variables_min"]) + data["vars_per_degree"][target].append(instance["variables_per_degree"]) + + return data + +if __name__ == "__main__": + main() diff --git a/testMinisatResults.py b/testMinisatResults.py new file mode 100755 index 0000000..f1c0566 --- /dev/null +++ b/testMinisatResults.py @@ -0,0 +1,47 @@ +#!/usr/bin/env python3 + +import kSAT +import minisatUtils as mSatU +import argparse + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument("-i", "--instance", help="instance file, has to be in DIMACS format", type=str) + parser.add_argument("-r", "--result", help="minisat result file", type=str) + args = parser.parse_args() + + instancePath = args.instance + if instancePath == None: + instancePath = str(input("Instance file: ")) + + minisatResultFile = args.result + if minisatResultFile == None: + minisatResultFile = str(input("Minisat result file: ")) + + print("Checking...") + print("Instance:\t%s" % instancePath) + print("Minisat result:\t%s" % minisatResultFile) + + checkStr = __checkResult(instancePath, minisatResultFile) + + print("check:\t\t%s" % checkStr) + + +def __checkResult(instancePath, minisatResultFile): + sat = kSAT.kSAT() + + sat.readDIMACS(instancePath) + + minisatResult = mSatU.readMinisatResult(minisatResultFile) + + if minisatResult["satisfiable"]: + if sat.checkAssignment(minisatResult["assignments"]): + return "results do match" + else: + return "results do NOT match" + else: + return "unsatisfiable" + +if __name__ == "__main__": + main() diff --git a/testRandomSat.py b/testRandomSat.py new file mode 100755 index 0000000..7d98a05 --- /dev/null +++ b/testRandomSat.py @@ -0,0 +1,22 @@ +#!/usr/bin/env python3 + +import randomSAT as rdSAT + +kSATInstance = rdSAT.generateRandomKSAT(5, 4, 3) + +print(kSATInstance.toString()) + +print("conflicts:") + +for conflict in kSATInstance.getConflicts(): + conflictVerified = False + + clause1 = kSATInstance.getClause(conflict[0][0]) + clause2 = kSATInstance.getClause(conflict[1][0]) + + for binding in clause2: + if binding == conflict[0][1] * -1: + conflictVerified = True + + print(conflict[0], conflict[1], conflictVerified) + diff --git a/testSAT2QUBO.py b/testSAT2QUBO.py new file mode 100755 index 0000000..8fda346 --- /dev/null +++ b/testSAT2QUBO.py @@ -0,0 +1,13 @@ +#!/usr/bin/env python3 + +import SAT2QUBO as s2q +import randomSAT as rs + +ksatInstance = rs.generateRandomKSAT(2, 4, 3) + +qubo = s2q.WMISdictQUBO(ksatInstance) + +print(ksatInstance.toString()) + +for label in qubo: + print(label, qubo[label]) diff --git a/util/SAT2QUBO.py b/util/SAT2QUBO.py new file mode 100644 index 0000000..a87290b --- /dev/null +++ b/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) + diff --git a/util/SATquboResult.py b/util/SATquboResult.py new file mode 100644 index 0000000..942a0e1 --- /dev/null +++ b/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 diff --git a/util/compare.py b/util/compare.py new file mode 100644 index 0000000..89effac --- /dev/null +++ b/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 + diff --git a/util/kSAT.py b/util/kSAT.py new file mode 100644 index 0000000..47ac0a5 --- /dev/null +++ b/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 diff --git a/util/minisatUtils.py b/util/minisatUtils.py new file mode 100644 index 0000000..b4cfc06 --- /dev/null +++ b/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 + diff --git a/util/randomSAT.py b/util/randomSAT.py new file mode 100644 index 0000000..8ce050e --- /dev/null +++ b/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 diff --git a/util/scriptUtils.py b/util/scriptUtils.py new file mode 100644 index 0000000..71e361e --- /dev/null +++ b/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 + diff --git a/verifyWMISresult.py b/verifyWMISresult.py new file mode 100755 index 0000000..820f17e --- /dev/null +++ b/verifyWMISresult.py @@ -0,0 +1,38 @@ +#!/usr/bin/env python3 + +from kSAT import kSAT +import SATquboResult +import argparse + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument("-i", "--instance", help="instance file, has to be in DIMACS format", type=str) + parser.add_argument("-r", "--result", help="WMIS qubo result file", type=str) + args = parser.parse_args() + + instancePath = args.instance + if instancePath == None: + instancePath = str(input("Instance file: ")) + + resultFile = args.result + if resultFile == None: + resultFile = str(input("WMIS qubo result file: ")) + + __verify(instancePath, resultFile) + + +def __verify(instancePath, resultFile): + sat = kSAT() + sat.readDIMACS(instancePath) + + assignments = SATquboResult.readAssignmentsFromFile(resultFile) + + + evaluations = sat.evaluate(assignments) + + for i in range(len(assignments)): + print(assignments[i], evaluations[i]) + + +if __name__ == "__main__": + main()