我正在尝试使用command line中的z3作为SAT求解器,但我不知道如何使它生成不满足的证明。不管我做什么,它只会打印出“ unsat”,没有任何解释,我在网上找不到任何帮助。我尝试在命令行上传递proof=true
,但没有任何改变。
../z3-4.8.6-x64-ubuntu-16.04/bin/z3 proof=true unsat_core=true test_tx.cnf
unsat
z3可以在SMTLib模式下生成证明(尽管尚未指定证明格式。)我不确定它是否甚至可以在CNF模式下生成证明,尽管肯定可以。您最好的选择是在https://github.com/Z3Prover/z3/issues提交问题,看看是否支持。