scripts

.gitignore

@@ -1 +1,2 @@
 extended/*
+*.swp

extend.py

@@ -0,0 +1,42 @@
+#!python3
+
+import sys
+from pysat.formula import CNF
+import argparse
+import pathlib as pl
+import bz2
+
+def main():
+    f_ext= CNF(from_fp=sys.stdin)
+    
+    instance_dir = pl.Path(parse_args())
+
+    instance, core_nr = parse_header(f_ext.comments[0])
+
+    ipath = instance_dir / (instance + ".cnf.bz2")
+
+    f = CNF(ipath)    
+
+    f.extend(f_ext)
+    f.comments = []
+
+    f.to_fp(sys.stdout,
+            comments=["c extension_of:{} nr:{}".format(instance, core_nr)])
+
+def parse_args():
+    parser = argparse.ArgumentParser()
+    parser.add_argument("-i", "--instance_dir",
+                        type=str,
+                        default="./instances",
+                        help="path to the directoy containing all instances")
+
+    args = parser.parse_args()
+
+    return args.instance_dir
+def parse_header(header):
+    tokens = header.split(' ')[1:]
+
+    return tokens[0].split(':')[1], int(tokens[1].split(':')[1])
+    
+if __name__ == "__main__":
+    main()

gen_eq_instances.py

@@ -57,18 +57,16 @@ def run(instance, calls_per_instance):
     for i in range(calls_per_instance):
         extension = gen_extension(iname, len(f.clauses) / 10)
         
-        #tmp_f = f.copy()
-        #tmp_f.extend(extension)
-        
         ext_f = CNF()
         ext_f.extend(extension)
 
         print(iname)
         print(len(f.clauses))
         print()
-
-        ext_f.to_file(next_file_path(iname),
-                      comments=["c {} core extended".format(iname),
+        
+        fpath, nr = next_file_path(iname)
+        ext_f.to_file(fpath,
+                      comments=["c extending:{} nr:{}".format(iname, nr),
                                 "c number of cores: {}".format(len(extension))],
                       compress_with="bzip2")
 
@@ -111,7 +109,7 @@ def next_file_path(name):
         counter += 1
         ext_file_path = EXTENDED_DIR / ("{}_{:04}.cnf.bz2".format(name, counter))
         
-    return ext_file_path 
+    return ext_file_path, counter 
 
 if __name__ == "__main__":
     main()

main.py

@@ -0,0 +1,77 @@
+"""
+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_ext_path = pl.Path("./solve_extended.sh").absolute()
+
+    #p = Popen([solve_ext_path, instance])
+    p = Popen(["bash", "./solve_extended.sh", 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
+
+if __name__ == '__main__':
+    parser = argparse.ArgumentParser()
+    parser.add_argument("-i", "--instance", help="The instance.")
+
+    args = parser.parse_args()
+
+
+    res_str = run_alg(args.instance)
+
+    res = parse_result(res_str)
+
+    print(','.join(map(str, res.values())))
+
+    
+    
+
+    

main.py.backup

@@ -0,0 +1,52 @@
+"""
+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
+
+
+def run_alg(instance, seed):
+    p = Popen(['./uweAlg', '--cb', '1.0', '--fct', str(1), instance, str(abs(seed))], stdin = PIPE, stdout = PIPE, stderr=PIPE)
+    output, err = p.communicate()
+    rc = p.returncode
+    err = err.decode("utf-8")
+    if err != "":
+        print(err, file=sys.stderr)
+    return output.decode("utf-8").replace(" 1\n","").replace("\n","")
+    
+
+if __name__ == '__main__':
+    parser = argparse.ArgumentParser()
+    parser.add_argument("-s", "--seed", type=int, default=1909, help="The seed.")
+    parser.add_argument("-i", "--instance", default='./instances/uf250-01.cnf', help="The instance.")
+
+    args = parser.parse_args()
+
+    start = timer()
+    flips = run_alg(args.instance, args.seed)
+    end = timer()
+    print(flips, end-start, str(abs(args.seed)))
+
+
+    
+    
+
+    

solve_extended.sh

@@ -0,0 +1,3 @@
+#!bash
+
+bzip2 -d < ${1} | python3 ./extend.py | glucose