Code: Select all
Traceback (most recent call last):
File "./lls", line 195, in <module>
indent = indent, verbosity = verbosity
File "/home/ionma/logic-life-search/src/LLS.py", line 61, in preprocess_solve_and_postprocess
indent = indent, verbosity = verbosity
File "/home/ionma/logic-life-search/src/LLS.py", line 175, in preprocess_and_solve
indent = indent, verbosity = verbosity)
File "/home/ionma/logic-life-search/src/LLS.py", line 246, in solve
DIMACS_string, solver=solver, parameters=parameters, timeout=timeout, save_dimacs = save_dimacs, dry_run = dry_run, indent = indent + 1, verbosity = verbosity)
File "/home/ionma/logic-life-search/src/LLS_SAT_solvers.py", line 48, in SAT_solve
solution, time_taken = use_solver(solver, dimacs_file, parameters = parameters, timeout = timeout, indent = indent, verbosity = verbosity)
File "/home/ionma/logic-life-search/src/LLS_SAT_solvers.py", line 86, in use_solver
stdout=subprocess.PIPE, stdin=subprocess.PIPE, stderr=subprocess.PIPE)
File "/usr/lib/python2.7/subprocess.py", line 390, in __init__
errread, errwrite)
File "/usr/lib/python2.7/subprocess.py", line 1025, in _execute_child
raise child_exception
OSError: [Errno 13] Permission denied
I've also tried setting the solver to lingeling.exe instead of just lingeling, which just says it can't find the solver:
Code: Select all
Traceback (most recent call last):
File "./lls", line 195, in <module>
indent = indent, verbosity = verbosity
File "/home/ionma/logic-life-search/src/LLS.py", line 61, in preprocess_solve_and_postprocess
indent = indent, verbosity = verbosity
File "/home/ionma/logic-life-search/src/LLS.py", line 175, in preprocess_and_solve
indent = indent, verbosity = verbosity)
File "/home/ionma/logic-life-search/src/LLS.py", line 246, in solve
DIMACS_string, solver=solver, parameters=parameters, timeout=timeout, save_dimacs = save_dimacs, dry_run = dry_run, indent = indent + 1, verbosity = verbosity)
File "/home/ionma/logic-life-search/src/LLS_SAT_solvers.py", line 32, in SAT_solve
assert solver in solvers, "Solver not found"
AssertionError: Solver not found