From 2aaf89d01f151c3bd90d3735a102323ec8430454 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tom=20Kr=C3=BCger?= Date: Thu, 21 Jan 2021 02:20:10 +0100 Subject: [PATCH] scripts --- .gitignore | 1 + extend.py | 42 +++++++++++++++++++++++++ gen_eq_instances.py | 12 +++---- main.py | 77 +++++++++++++++++++++++++++++++++++++++++++++ main.py.backup | 52 ++++++++++++++++++++++++++++++ solve_extended.sh | 3 ++ 6 files changed, 180 insertions(+), 7 deletions(-) create mode 100755 extend.py create mode 100644 main.py create mode 100644 main.py.backup create mode 100755 solve_extended.sh diff --git a/.gitignore b/.gitignore index a803088..118c0cd 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,2 @@ extended/* +*.swp diff --git a/extend.py b/extend.py new file mode 100755 index 0000000..d07d986 --- /dev/null +++ b/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() diff --git a/gen_eq_instances.py b/gen_eq_instances.py index 865620f..40a5604 100755 --- a/gen_eq_instances.py +++ b/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() diff --git a/main.py b/main.py new file mode 100644 index 0000000..cf1c5ca --- /dev/null +++ b/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()))) + + + + + diff --git a/main.py.backup b/main.py.backup new file mode 100644 index 0000000..9608090 --- /dev/null +++ b/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))) + + + + + + diff --git a/solve_extended.sh b/solve_extended.sh new file mode 100755 index 0000000..9bd0007 --- /dev/null +++ b/solve_extended.sh @@ -0,0 +1,3 @@ +#!bash + +bzip2 -d < ${1} | python3 ./extend.py | glucose