Skip to content

Commit

Permalink
little changes with limits
Browse files Browse the repository at this point in the history
  • Loading branch information
Vikseko committed Apr 8, 2024
1 parent a10c0c7 commit 2bc216d
Showing 1 changed file with 6 additions and 7 deletions.
13 changes: 6 additions & 7 deletions main_p.py
Original file line number Diff line number Diff line change
Expand Up @@ -42,20 +42,19 @@ def create_parser():
seed = namespace.seedinitea
workers = namespace.nofprocesses
bds = namespace.backdoorsize
if namespace.timelimit == 0 and namespace.conflictlimit == 0:
print('None of the hard tasks solution constraints is set. '
'It is necessary to set either --timelimit [SECONDS] or --conflictlimit [INT].')
raise Exception()
lim = max(namespace.timelimit, namespace.conflictlimit)
limtype = 'conflicts' if namespace.conflictlimit > namespace.timelimit else 'time'
timelim = namespace.timelimit
conflictlim = namespace.conflictlimit
if timelim == 0 and conflictlim == 0:
conflictlim = 20000
lim = max(timelim, conflictlim)
limtype = 'conflicts' if conflictlim > timelim else 'time'
measure = measures.get(f'measure:{limtype}')()

data_path = WorkPath('examples', 'data')
# enc_file = data_path.to_file('sgen_150.cnf')
# cnf_file = data_path.to_file('pvs_4_7.cnf')

solver = PySatSolver(sat_name=solver_name)
# TODO надо чекать расширение файла (или читать хэдер) и если это wcnf то работать с wcnf
# problem = encode_problem(formula_file, solver)
if formula_file.endswith('.cnf'):
encoding = CNF(from_file=formula_file)
Expand Down

0 comments on commit 2bc216d

Please sign in to comment.