|
|
- """
- 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))))
-
-
-
-
-
|
