【发布时间】:2019-09-14 20:15:35
【问题描述】:
我正在尝试对我的程序生成的一堆 cnf 编码运行 SAT 求解器。我已经通过自制软件在我的笔记本电脑(MacOS)上安装了 minisat,我可以在终端上运行 minisat:
$ minisat INPUT_FILE.cnf OUTPUT_FILE.txt
但是因为我有数百个编码,所以我使用subprocess 编写了一个自定义命令。编码在for 循环内生成。该循环还包含 subprocess 命令,理想情况下,SAT 求解器 (minisat) 会在每个循环中对每个文件运行。
cnf 编码生成良好,我可以在终端上单独运行它们,但是当我尝试运行使用 subprocess 命令时,它会抛出错误:
FileNotFoundError: [Errno 2] No such file or directory: 'minisat': 'minisat'
这是我的代码(它只是我代码的一部分,我省略了不相关的部分):
solver = 'minisat'
for i in range...:
encoding = generate_encoding()
cnf = 'generated_cnf_encoding'+ str(i) +'.cnf'
#write encoding to cnf
...
sol = 'empty_output_file'+ str(i) +'.txt'
cmd = [solver, cnf, sol]
p = subprocess.Popen(cmd, stdout=subprocess.PIPE, stderr=subprocess.PIPE)
output, err = p.communicate()
print(err)
编辑:在此处提到的其他几个解决方案中,建议添加 shell=True,但在打印 err 时会抛出 minisat: command not found
【问题讨论】:
标签: python subprocess popen sat sat-solvers