scripts, cores and docs

.gitignore

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

README.md

@@ -0,0 +1,27 @@
+# dependencies
+
+* pysat
+* [glucose](https://www.labri.fr/perso/lsimon/glucose/)
+...version 4.1
+...put binary in ***util*** directory
+* bzip2
+
+## gen_core_extensions.py
+
+Script to generate core extensions.
+
+| arg | arg long | default | description |
+|----|---------|-------|--|
+| -i | --instance_dir | ./instances | directory containing the instances |
+| -c | --cores_dir | ./cores_dir | directory containing the cores |
+| -e | --extensions_dir | ./extensions | target directory to store the generated core extensions |
+| -n | --nr_per_instance | 1 | number of extensions per instance |
+| -v | --verbosity | 1 | **1** to print progress, **0** for silent mode |
+
+Just call with:
+```bash
+$ ./gen_core_extensions.py -n 5000
+```
+## main.py
+
+Does **NOT** have to be called from any specific directory!

gen_core_extensions.py

@@ -0,0 +1,139 @@
+#!python3
+
+from pysat.formula import CNF
+from pysat.solvers import Glucose4
+
+import pathlib as pl
+import random
+import bz2
+import sys
+import argparse 
+
+CORE_DIR = pl.Path("./cores")
+EXTENDED_DIR = pl.Path("./extensions")
+
+
+def main():
+    args = parse_args()
+
+    instances = get_instance_paths(pl.Path(args.instance_dir))
+    
+    CORE_DIR = pl.Path(args.cores_dir)
+    EXTENDED_DIR = pl.Path(args.extensions_dir)
+    
+    for instance in instances:
+        run(instance, args.nr_per_instance, args.verbosity > 0)
+
+def parse_args():
+    parser = argparse.ArgumentParser()
+    parser.add_argument( "-i"
+                        ,"--instance_dir"
+                        ,type=str
+                        ,default="./instances"
+                        ,help="directory containing the instances")
+    parser.add_argument( "-c"
+                        ,"--cores_dir"
+                        ,type=str
+                        ,default="./cores"
+                        ,help="directory containing the cores")
+    parser.add_argument( "-e"
+                        ,"--extensions_dir"
+                        ,type=str
+                        ,default="./extensions"
+                        ,help="directory target directory to store the generated core extensions")
+    parser.add_argument( "-n"
+                        ,"--nr_per_instance"
+                        ,type=int
+                        ,default=1
+                        ,help="number of extensions per instance")
+    parser.add_argument( "-v"
+                        ,"--verbosity"
+                        ,type=int
+                        ,default=1
+                        ,help="1 to print progress, 0 for silent mode")
+
+    return parser.parse_args()
+
+def get_instance_paths(instances_dir):
+    instances = []
+
+    for p in instances_dir.iterdir():
+        if str(p).endswith(".cnf.bz2"):
+            instances.append(p)
+
+    return instances 
+
+def run(instance, calls_per_instance, verb):
+    ipath = pl.Path(instance)
+    iname = ipath.stem[:-4]
+
+    f = CNF(str(ipath))
+    
+    cores = parse_cores(iname)
+    
+
+    for i in range(calls_per_instance):
+        extension = gen_extension(cores)
+        
+        if verb and i % 20 == 0:
+            print("instance: {}".format(iname))
+
+        if verb:
+            print("extension: {} | #cores: {} ({:2.2f}%)".format(i+1, len(extension), 100 * len(extension) / len(cores)))
+
+        ext_f = CNF()
+        ext_f.extend(extension)
+        
+        fpath, nr = next_file_path(iname)
+        
+        if not EXTENDED_DIR.exists():
+            EXTENDED_DIR.mkdir(parents=True)
+
+        ext_f.to_file(fpath,
+                      comments=["c extending:{} nr:{}".format(iname, nr),
+                                "c number of cores: {}".format(len(extension))],
+                      compress_with="bzip2")
+
+    if verb:
+        print()
+
+def gen_extension(cores):
+
+    p = (len(cores) / 10 ) / len(cores)
+   
+    extension = []
+    while len(extension) == 0:
+        for core in cores:
+            if p >= random.random():
+                extension.append(core)
+
+
+    return extension
+
+def parse_cores(instance):
+    cores = []
+    
+    with bz2.open(CORE_DIR / (instance + ".cores.bz2"), "tr") as cores_file:
+        cores = list(map(lambda l: l.strip(), cores_file.readlines()))
+    
+    cores = list(map(lambda l: l.split(","), cores))
+    
+    for i in range(len(cores)):
+        cores[i] = list(map(int, cores[i]))
+        cores[i] = list(map(lambda lit: -1 * lit, cores[i]))
+
+    return cores
+
+def next_file_path(name):
+    counter = 0
+
+    ext_file_path = EXTENDED_DIR / ("{}_{:04}.cnf.bz2".format(name, counter))
+
+    while ext_file_path.exists():
+        counter += 1
+        ext_file_path = EXTENDED_DIR / ("{}_{:04}.cnf.bz2".format(name, counter))
+        
+    return ext_file_path, counter 
+
+if __name__ == "__main__":
+    main()

gen_eq_instances.py

@@ -1,115 +0,0 @@
-#!python3
-
-from pysat.formula import CNF
-from pysat.solvers import Glucose4
-
-import pathlib as pl
-import random
-import bz2
-import sys
-
-CORE_DIR = pl.Path("./cores")
-EXTENDED_DIR = pl.Path("./extended")
-
-usage_str = "usage: gen_eq_instance.py [instance dir] [num per instance]"
-
-def main():
-    instances_dir = None
-
-    try:
-        instances_dir = pl.Path(sys.argv[1])
-    except:
-        print(usage_str)
-        return
-    else:
-        if not instances_dir.is_dir():
-            print(usage_str)
-            return
-
-    num_per_instance = 0
-    try:
-        num_per_instance = int(sys.argv[2])
-    except:
-        print(usage_str)
-        return
-
-
-    instances = get_instance_paths(instances_dir)
-    
-    for instance in instances:
-        run(instance, num_per_instance)
-
-def get_instance_paths(instances_dir):
-    instances = []
-
-    for p in instances_dir.iterdir():
-        if str(p).endswith(".cnf.bz2"):
-            instances.append(p)
-
-    return instances 
-
-def run(instance, calls_per_instance):
-    ipath = pl.Path(instance)
-    iname = ipath.stem[:-4]
-
-    f = CNF(str(ipath))
-    
-    for i in range(calls_per_instance):
-        extension = gen_extension(iname, len(f.clauses) / 10)
-        
-        ext_f = CNF()
-        ext_f.extend(extension)
-
-        print(iname)
-        print(len(f.clauses))
-        print()
-        
-        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")
-
-def gen_extension(instance, expected_num_of_core):
-    cores = parse_cores(instance)
-
-    p = expected_num_of_core / len(cores)
-    
-    extension = []
-    
-    print((expected_num_of_core * 10) / len(cores))
-    print(expected_num_of_core * 10, len(cores))
-
-    for core in cores:
-        if p >= random.random():
-            extension.append(core)
-
-    return extension
-
-def parse_cores(instance):
-    cores = []
-    
-    with bz2.open(CORE_DIR / (instance + ".cores.bz2"), "tr") as cores_file:
-        cores = list(map(lambda l: l.strip(), cores_file.readlines()))
-    
-    cores = list(map(lambda l: l.split(","), cores))
-    
-    for i in range(len(cores)):
-        cores[i] = list(map(int, cores[i]))
-        cores[i] = list(map(lambda lit: -1 * lit, cores[i]))
-
-    return cores
-
-def next_file_path(name):
-    counter = 0
-
-    ext_file_path = EXTENDED_DIR / ("{}_{:04}.cnf.bz2".format(name, counter))
-
-    while ext_file_path.exists():
-        counter += 1
-        ext_file_path = EXTENDED_DIR / ("{}_{:04}.cnf.bz2".format(name, counter))
-        
-    return ext_file_path, counter 
-
-if __name__ == "__main__":
-    main()

inspect_cores.py

@@ -0,0 +1,104 @@
+#!python3
+
+from pysat.formula import CNF
+from pysat.solvers import Glucose4
+
+import pathlib as pl
+import random
+import bz2
+import sys
+import argparse 
+
+
+def main():
+    args = parse_args()
+
+    instances = get_instance_paths(pl.Path(args.instance_dir))
+    
+    global CORE_DIR
+    CORE_DIR = pl.Path(args.cores_dir)
+
+    global EXTENDED_DIR 
+    EXTENDED_DIR = pl.Path(args.extensions_dir)
+   
+    print(CORE_DIR)
+
+    for instance in instances:
+        run(instance, args.nr_per_instance)
+
+def parse_args():
+    parser = argparse.ArgumentParser()
+    parser.add_argument( "-i"
+                        ,"--instance_dir"
+                        ,type=str
+                        ,default="./instances"
+                        ,help="directory containing the instances")
+    parser.add_argument( "-c"
+                        ,"--cores_dir"
+                        ,type=str
+                        ,default="./cores"
+                        ,help="directory containing the cores")
+    parser.add_argument( "-e"
+                        ,"--extensions_dir"
+                        ,type=str
+                        ,default="./extensions"
+                        ,help="directory containing the core extensions")
+    parser.add_argument( "-n"
+                        ,"--nr_per_instance"
+                        ,type=int
+                        ,default=1
+                        ,help="number of extensions per instance")
+
+    return parser.parse_args()
+
+def get_instance_paths(instances_dir):
+    instances = []
+
+    for p in instances_dir.iterdir():
+        if str(p).endswith(".cnf.bz2"):
+            instances.append(p)
+
+    return instances 
+
+def run(instance, calls_per_instance):
+    ipath = pl.Path(instance)
+    iname = ipath.stem[:-4]
+
+    f = CNF(str(ipath))
+
+    for i in range(calls_per_instance):
+        cores = parse_cores(iname)
+
+        print(iname)
+        print(len(f.clauses), len(cores))
+        print("{0:.3g}".format(len(cores) * 100 / len(f.clauses)))
+
+        print()
+
+def parse_cores(instance):
+    cores = []
+    
+    with bz2.open(CORE_DIR / (instance + ".cores.bz2"), "tr") as cores_file:
+        cores = list(map(lambda l: l.strip(), cores_file.readlines()))
+    
+    cores = list(map(lambda l: l.split(","), cores))
+    
+    for i in range(len(cores)):
+        cores[i] = list(map(int, cores[i]))
+        cores[i] = list(map(lambda lit: -1 * lit, cores[i]))
+
+    return cores
+
+def next_file_path(name):
+    counter = 0
+
+    ext_file_path = EXTENDED_DIR / ("{}_{:04}.cnf.bz2".format(name, counter))
+
+    while ext_file_path.exists():
+        counter += 1
+        ext_file_path = EXTENDED_DIR / ("{}_{:04}.cnf.bz2".format(name, counter))
+        
+    return ext_file_path, counter 
+
+if __name__ == "__main__":
+    main()

main.py

@@ -24,10 +24,9 @@ from timeit import default_timer as timer
 import pathlib as pl
 
 def run_alg(instance):
-    solve_ext_path = pl.Path("./solve_extended.sh").absolute()
+    solve_extended_path = pl.Path(__file__).absolute().parent / "util" / "solve_extended.sh"
 
-    #p = Popen([solve_ext_path, instance])
+    p = Popen(["bash", str(solve_extended_path), instance], stdin = PIPE, stdout = PIPE, stderr=PIPE)
-    p = Popen(["bash", "./solve_extended.sh", instance], stdin = PIPE, stdout = PIPE, stderr=PIPE)
 
     output, err = p.communicate()
     rc = p.returncode
@@ -70,20 +69,28 @@ def parse_instance_path(ipath):
 
 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(args.instance)
+    res_str = run_alg(str(pl.Path(args.instance).absolute()))
-
 
     iname, ext_nr = parse_instance_path(args.instance)
 
     res = parse_result(res_str)
     
-    res_vals = [iname, str(ext_nr)] + list(map(str, res.values()))
+    res_vals = [ iname
+                ,str(ext_nr)
+                ,res["restarts"]
+                ,res["conflicts"]
+                ,res["decisions"]
+                ,res["propagations"]
+                ,res["reduced_clauses"]
+                ,res["cpu_time"]
+                ,res["result"]] 
 
-    print(','.join(res_vals))
+    print(','.join(list(map(str, res_vals))))
 
     
     

main.py.backup

@@ -1,52 +0,0 @@
-"""
-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

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

util/extend.py

@@ -27,7 +27,6 @@ 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()

util/solve_extended.sh

@@ -0,0 +1,7 @@
+#!/bin/bash
+
+dir_path=$(dirname $(realpath $0))
+extend_script="${dir_path}/extend.py"
+glucose_bin="${dir_path}/glucose"
+
+bzip2 -d < ${1} | python3 ${extend_script} -i "${dir_path}/../instances"| ${glucose_bin}

util/test.sh

@@ -0,0 +1,5 @@
+#!/bin/bash
+
+echo $0
+
+echo $(dirname $0)