97 lines
3.2 KiB
Python
97 lines
3.2 KiB
Python
"""
|
||
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))))
|
||
|
||
|
||
|
||
|
||
|