diff --git a/.gitignore b/.gitignore index 118c0cd..625fbd7 100644 --- a/.gitignore +++ b/.gitignore @@ -1,2 +1,2 @@ -extended/* +extensions/* *.swp diff --git a/README.md b/README.md index e69de29..1696f2f 100644 --- a/README.md +++ b/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! diff --git a/cores/Problem14_label14_false-unreach-call.c.cores.bz2 b/cores/Problem14_label14_false-unreach-call.c.cores.bz2 index d363d52..78a8d87 100644 Binary files a/cores/Problem14_label14_false-unreach-call.c.cores.bz2 and b/cores/Problem14_label14_false-unreach-call.c.cores.bz2 differ diff --git a/cores/Problem14_label19_true-unreach-call.c.cores.bz2 b/cores/Problem14_label19_true-unreach-call.c.cores.bz2 index 330ad3a..8ef1f3c 100644 Binary files a/cores/Problem14_label19_true-unreach-call.c.cores.bz2 and b/cores/Problem14_label19_true-unreach-call.c.cores.bz2 differ diff --git a/cores/Problem14_label48_true-unreach-call.c.cores.bz2 b/cores/Problem14_label48_true-unreach-call.c.cores.bz2 index ffef7d8..74bd806 100644 Binary files a/cores/Problem14_label48_true-unreach-call.c.cores.bz2 and b/cores/Problem14_label48_true-unreach-call.c.cores.bz2 differ diff --git a/cores/Problem14_label57_false-unreach-call.c.cores.bz2 b/cores/Problem14_label57_false-unreach-call.c.cores.bz2 index 00d835b..18a2cb4 100644 Binary files a/cores/Problem14_label57_false-unreach-call.c.cores.bz2 and b/cores/Problem14_label57_false-unreach-call.c.cores.bz2 differ diff --git a/cores/dist10.c.cores.bz2 b/cores/dist10.c.cores.bz2 index 02356a7..e3cd904 100644 Binary files a/cores/dist10.c.cores.bz2 and b/cores/dist10.c.cores.bz2 differ diff --git a/cores/dist9.c.cores.bz2 b/cores/dist9.c.cores.bz2 index 1ecc1ec..98c3b20 100644 Binary files a/cores/dist9.c.cores.bz2 and b/cores/dist9.c.cores.bz2 differ diff --git a/cores/ecarev-110-1031-23-40-2.cores.bz2 b/cores/ecarev-110-1031-23-40-2.cores.bz2 index 0321782..5cb26a6 100644 Binary files a/cores/ecarev-110-1031-23-40-2.cores.bz2 and b/cores/ecarev-110-1031-23-40-2.cores.bz2 differ diff --git a/cores/ecarev-110-1031-23-40-3.cores.bz2 b/cores/ecarev-110-1031-23-40-3.cores.bz2 index da77d1a..0b97a1f 100644 Binary files a/cores/ecarev-110-1031-23-40-3.cores.bz2 and b/cores/ecarev-110-1031-23-40-3.cores.bz2 differ diff --git a/cores/ecarev-110-1031-23-40-5.cores.bz2 b/cores/ecarev-110-1031-23-40-5.cores.bz2 index 42e9b50..1c17ba5 100644 Binary files a/cores/ecarev-110-1031-23-40-5.cores.bz2 and b/cores/ecarev-110-1031-23-40-5.cores.bz2 differ diff --git a/cores/ecarev-110-1031-23-40-7.cores.bz2 b/cores/ecarev-110-1031-23-40-7.cores.bz2 index e5fe2fc..8d0f566 100644 Binary files a/cores/ecarev-110-1031-23-40-7.cores.bz2 and b/cores/ecarev-110-1031-23-40-7.cores.bz2 differ diff --git a/cores/ecarev-110-4099-22-30-2.cores.bz2 b/cores/ecarev-110-4099-22-30-2.cores.bz2 index 172b047..b8cd31e 100644 Binary files a/cores/ecarev-110-4099-22-30-2.cores.bz2 and b/cores/ecarev-110-4099-22-30-2.cores.bz2 differ diff --git a/cores/ecarev-110-4099-22-30-4.cores.bz2 b/cores/ecarev-110-4099-22-30-4.cores.bz2 index 220e2a5..2091eba 100644 Binary files a/cores/ecarev-110-4099-22-30-4.cores.bz2 and b/cores/ecarev-110-4099-22-30-4.cores.bz2 differ diff --git a/cores/ecarev-110-4099-22-30-5.cores.bz2 b/cores/ecarev-110-4099-22-30-5.cores.bz2 index 9e3f798..45498d7 100644 Binary files a/cores/ecarev-110-4099-22-30-5.cores.bz2 and b/cores/ecarev-110-4099-22-30-5.cores.bz2 differ diff --git a/cores/ecarev-110-4099-22-30-7.cores.bz2 b/cores/ecarev-110-4099-22-30-7.cores.bz2 index 339de0f..561867e 100644 Binary files a/cores/ecarev-110-4099-22-30-7.cores.bz2 and b/cores/ecarev-110-4099-22-30-7.cores.bz2 differ diff --git a/cores/factoring87654321x12345678.cores.bz2 b/cores/factoring87654321x12345678.cores.bz2 index d12c136..5ae6eab 100644 Binary files a/cores/factoring87654321x12345678.cores.bz2 and b/cores/factoring87654321x12345678.cores.bz2 differ diff --git a/cores/filter1_true-unreach-call.c.cores.bz2 b/cores/filter1_true-unreach-call.c.cores.bz2 index 7fe8ebd..196d4fa 100644 Binary files a/cores/filter1_true-unreach-call.c.cores.bz2 and b/cores/filter1_true-unreach-call.c.cores.bz2 differ diff --git a/cores/gto_p60c233.cores.bz2 b/cores/gto_p60c233.cores.bz2 index 873848d..986a89a 100644 Binary files a/cores/gto_p60c233.cores.bz2 and b/cores/gto_p60c233.cores.bz2 differ diff --git a/cores/gto_p60c234.cores.bz2 b/cores/gto_p60c234.cores.bz2 index 3d398ae..e890fc5 100644 Binary files a/cores/gto_p60c234.cores.bz2 and b/cores/gto_p60c234.cores.bz2 differ diff --git a/cores/gto_p60c235.cores.bz2 b/cores/gto_p60c235.cores.bz2 index 0b6702e..a9c4bea 100644 Binary files a/cores/gto_p60c235.cores.bz2 and b/cores/gto_p60c235.cores.bz2 differ diff --git a/cores/gto_p60c238.cores.bz2 b/cores/gto_p60c238.cores.bz2 index 6a9af24..7fe8e6b 100644 Binary files a/cores/gto_p60c238.cores.bz2 and b/cores/gto_p60c238.cores.bz2 differ diff --git a/cores/gto_p60c243.cores.bz2 b/cores/gto_p60c243.cores.bz2 index 0973903..f66e85d 100644 Binary files a/cores/gto_p60c243.cores.bz2 and b/cores/gto_p60c243.cores.bz2 differ diff --git a/cores/newton_3_4_true-unreach-call.i.cores.bz2 b/cores/newton_3_4_true-unreach-call.i.cores.bz2 index 58044a4..86cafe9 100644 Binary files a/cores/newton_3_4_true-unreach-call.i.cores.bz2 and b/cores/newton_3_4_true-unreach-call.i.cores.bz2 differ diff --git a/cores/newton_3_6_false-unreach-call.i.cores.bz2 b/cores/newton_3_6_false-unreach-call.i.cores.bz2 index 5a97ba0..7e8246c 100644 Binary files a/cores/newton_3_6_false-unreach-call.i.cores.bz2 and b/cores/newton_3_6_false-unreach-call.i.cores.bz2 differ diff --git a/cores/pals_lcr-var-start-time.5_true-unreach-call.ufo.UNBOUNDED.pals.c.cores.bz2 b/cores/pals_lcr-var-start-time.5_true-unreach-call.ufo.UNBOUNDED.pals.c.cores.bz2 index cb5f19c..5fd9872 100644 Binary files a/cores/pals_lcr-var-start-time.5_true-unreach-call.ufo.UNBOUNDED.pals.c.cores.bz2 and b/cores/pals_lcr-var-start-time.5_true-unreach-call.ufo.UNBOUNDED.pals.c.cores.bz2 differ diff --git a/cores/quadratic_tight_error.c.cores.bz2 b/cores/quadratic_tight_error.c.cores.bz2 index 9a03398..c290d6b 100644 Binary files a/cores/quadratic_tight_error.c.cores.bz2 and b/cores/quadratic_tight_error.c.cores.bz2 differ diff --git a/gen_core_extensions.py b/gen_core_extensions.py new file mode 100755 index 0000000..55edb64 --- /dev/null +++ b/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() diff --git a/gen_eq_instances.py b/gen_eq_instances.py deleted file mode 100755 index 40a5604..0000000 --- a/gen_eq_instances.py +++ /dev/null @@ -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() diff --git a/inspect_cores.py b/inspect_cores.py new file mode 100755 index 0000000..6efa7d8 --- /dev/null +++ b/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() diff --git a/main.py b/main.py index 5a5bb66..a949ea7 100644 --- a/main.py +++ b/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", "./solve_extended.sh", instance], stdin = PIPE, stdout = PIPE, stderr=PIPE) + p = Popen(["bash", str(solve_extended_path), 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())) - - print(','.join(res_vals)) + res_vals = [ iname + ,str(ext_nr) + ,res["restarts"] + ,res["conflicts"] + ,res["decisions"] + ,res["propagations"] + ,res["reduced_clauses"] + ,res["cpu_time"] + ,res["result"]] + + print(','.join(list(map(str, res_vals)))) diff --git a/main.py.backup b/main.py.backup deleted file mode 100644 index 9608090..0000000 --- a/main.py.backup +++ /dev/null @@ -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))) - - - - - - diff --git a/solve_extended.sh b/solve_extended.sh deleted file mode 100755 index 9bd0007..0000000 --- a/solve_extended.sh +++ /dev/null @@ -1,3 +0,0 @@ -#!bash - -bzip2 -d < ${1} | python3 ./extend.py | glucose diff --git a/extend.py b/util/extend.py similarity index 95% rename from extend.py rename to util/extend.py index d07d986..ecf2ed1 100755 --- a/extend.py +++ b/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() diff --git a/util/glucose b/util/glucose new file mode 100755 index 0000000..ddf9725 Binary files /dev/null and b/util/glucose differ diff --git a/util/solve_extended.sh b/util/solve_extended.sh new file mode 100755 index 0000000..7c3f3fe --- /dev/null +++ b/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} diff --git a/util/test.sh b/util/test.sh new file mode 100644 index 0000000..3eca584 --- /dev/null +++ b/util/test.sh @@ -0,0 +1,5 @@ +#!/bin/bash + +echo $0 + +echo $(dirname $0)