main instance

main_instance.py

@@ -0,0 +1,96 @@
+"""
+This script is written for running Uwe Schöning's WalkSAT algorithm
+    [Uwe Schöning:
+    A probabilistic algorithm for k-SAT and constraint satisfaction problems.
+    In: Proceedings of FOCS 1999, IEEE, pages 410–414.]
+via the command line
+by specifying the instance to solve, and the seed to use.
+Uwe Schöning's WalkSAT algorithm can be seen as a special case of the probSAT algorithm
+    [Adrian Balint, Uwe Schöning:
+    Choosing Probability Distributions for Stochastic Local Search and the Role of Make versus Break.    
+    In: Lecture Notes in Computer Science, 2012, Volume 7317, Theory and Applications of Satisfiability Testing - SAT 2012, pages 16-29.
+    https://www.uni-ulm.de/fileadmin/website_uni_ulm/iui.inst.190/Mitarbeiter/balint/SAT2012.pdf]
+with exponential function (break-only-exp-algorithm) and c_b = 1.
+
+The script will record the number of flips, the time used, and the seed used.
+"""
+
+import argparse
+from subprocess import Popen, PIPE
+from time import sleep
+from os.path import exists
+import sys
+from timeit import default_timer as timer
+import pathlib as pl
+
+def run_alg(instance):
+    solve_instance_path = pl.Path(__file__).absolute().parent / "util" / "solve_instance.sh"
+    
+    p = Popen(["bash", str(solve_instance_path), instance], stdin = PIPE, stdout = PIPE, stderr=PIPE)
+
+    output, err = p.communicate()
+    rc = p.returncode
+    err = err.decode("utf-8") if err else ""
+    if err != "":
+        print(err, file=sys.stderr)
+
+    return output.decode("utf-8")
+
+def parse_result(res_str):
+    res = {}
+    
+    for line in res_str.splitlines():
+        if line.startswith("c restarts"):
+            res["restarts"] = int(line.split(":")[1].strip().split(" ")[0])
+        elif line.startswith("c conflicts"):
+            res["conflicts"] = int(line.split(":")[1].strip().split(" ")[0])
+        elif line.startswith("c decisions"):
+            res["decisions"] = int(line.split(":")[1].strip().split(" ")[0])
+        elif line.startswith("c propagations"):
+            res["propagations"] = int(line.split(":")[1].strip().split(" ")[0])
+        elif line.startswith("c nb reduced Clauses"):
+            res["reduced_clauses"] = int(line.split(":")[1])
+        elif line.startswith("c CPU time"):
+            res["cpu_time"] = float(line.split(":")[1].strip().split(" ")[0])
+        elif line.startswith("s"):
+            res["result"] = line.split(" ")[1].strip()
+
+    return res
+
+def parse_instance_path(ipath):
+    name = pl.Path(ipath).name.strip()
+
+    instance = name[:-len(".cnf.bz2")]
+
+    return instance
+
+
+
+if __name__ == '__main__':
+    parser = argparse.ArgumentParser()
+    parser.add_argument("-s", "--seed", type=int, default=1909, help="The seed.")
+    parser.add_argument("-i", "--instance", help="The instance.")
+
+    args = parser.parse_args()
+
+    res_str = run_alg(str(pl.Path(args.instance).absolute()))
+
+    iname = parse_instance_path(args.instance)
+
+    res = parse_result(res_str)
+    
+    res_vals = [ iname
+                ,res["restarts"]
+                ,res["conflicts"]
+                ,res["decisions"]
+                ,res["propagations"]
+                ,res["reduced_clauses"]
+                ,res["cpu_time"]
+                ,res["result"]] 
+
+    print(','.join(list(map(str, res_vals))))
+
+    
+    
+
+    

util/solve_instance.sh

@@ -0,0 +1,6 @@
+#!/bin/bash
+
+dir_path=$(dirname $(realpath $0))
+glucose_bin="${dir_path}/glucose"
+
+bzip2 -d < ${1} | ${glucose_bin}