You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
96 lines
3.2 KiB
96 lines
3.2 KiB
"""
|
|
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))))
|
|
|
|
|
|
|
|
|
|
|