-
Notifications
You must be signed in to change notification settings - Fork 0
/
main_rho_im.py
91 lines (75 loc) · 3.43 KB
/
main_rho_im.py
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
import os
import sys
import argparse
from pipeline.rho_solve_im import solve
from lib_satprob.solver import PySatSolver
from lib_satprob.problem import SatProblem
from lib_satprob.problem import MaxSatProblem
from lib_satprob.encoding import CNF, WCNF
from function.module.budget import TaskBudget
from function.module.measure import Conflicts, SolvingTime
def get_parser():
parser = argparse.ArgumentParser()
parser.add_argument('formula', type=str, help='File with input formula.')
parser.add_argument('-s', '--solvername', nargs='?', type=str, default='cd195',
help='Solver name: cd195, g3, mcb, m22, etc (see PySAT Solvers list).')
parser.add_argument('-nl', '--nofealimit', nargs='?', type=int, default=500,
help='Number of found rho-backdoors after which the algorithm will stop searching.')
parser.add_argument('-ng', '--nofeagroups', nargs='?', type=int, default=4,
help='Number of groups with different rho value that can exist simultaneously.')
parser.add_argument('-np', '--nofprocesses', nargs='?', type=int, default=12,
help='Number of simultaneously running islands in model.')
parser.add_argument('-bds', '--backdoorsize', nargs='?', type=int, default=10,
help='Size of a single rho-backdoor that evolutionary algorithms will find.')
parser.add_argument('-tl', '--timelimit', nargs='?', type=int, default=None,
help='Set limit in seconds to solve one hard task. Use this option OR conflicts limit.')
parser.add_argument('-cl', '--conflictlimit', nargs='?', type=int, default=None,
help='Set limit in conflicts to solve one hard task. Use this option OR time limit.')
parser.add_argument('-rs', '--randomseed', nargs='?', type=int, default=1234,
help='Random seed which is used to search for rho-backdoors')
return parser
def get_encoding(filepath: str):
if not os.path.isfile(filepath):
raise Exception(f'File {filepath} is not exist.')
if filepath.endswith('.cnf'):
return CNF(from_file=filepath)
elif filepath.endswith('.wcnf'):
return WCNF(from_file=filepath)
else:
with open(filepath) as f:
header = f.readline()
if 'p cnf' in header:
return CNF(from_file=filepath)
elif 'p wcnf' in header:
return WCNF(from_file=filepath)
else:
print('Wrong file extension:', filepath)
print('Only CNF or WCNF encodings supported.')
raise Exception('Wrong file extension.')
if __name__ == '__main__':
args = get_parser().parse_args(
sys.argv[1:]
)
encoding = get_encoding(args.formula)
solver = PySatSolver(sat_name=args.solvername)
problem = SatProblem(solver, encoding) \
if encoding.slug == 'encoding:cnf' \
else MaxSatProblem(solver, encoding)
if args.timelimit is not None:
limit = args.timelimit
measure = SolvingTime()
else:
limit = args.conflictlimit
limit = limit or 20000
measure = Conflicts()
budget = TaskBudget(limit)
report = solve(
budget=budget,
problem=problem,
measure=measure,
bd_count=args.nofealimit,
bd_size=args.backdoorsize,
random_seed=args.randomseed,
group_count=args.nofeagroups,
max_workers=args.nofprocesses,
)