Как заставить z3 генерировать доказательства неудовлетворенности?

Question

Я пытаюсь использовать z3 из командной строки в качестве решателя SAT, но не могу понять, как заставить его генерировать доказательство неудовлетворенности. Независимо от того, что я делаю, он просто печатает «unsat» без объяснения причин, и ничего, что я могу найти онлайн, не помогло. Я попытался передать proof=true в командной строке, но ничего не изменилось.

../z3-4.8.6-x64-ubuntu-16.04/bin/z3 proof=true unsat_core=true test_tx.cnf 
unsat

Answer 1

z3 может генерировать доказательства в режиме SMTLib (хотя формат доказательства довольно неопределен.) Я не уверен, что он вообще может генерировать доказательства в режиме CNF, хотя это, безусловно, должно быть возможно. Лучше всего подать вопрос на https://github.com/Z3Prover/z3/issues и посмотреть, поддерживается ли он.