CODEWITHSUNDEEP
z3sat
Antimony
Antimony

Reputation: 39501

How to make z3 generate proof of unsatisfiability?

I am trying to use z3 from the command line as a SAT solver, but I can't figure out how to make it generate a proof of unsatisfiability. No matter what I do, it just prints "unsat" with no explanation, and nothing I can find online has helped. I tried passing proof=true on the command line, but nothing changed.

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

Upvotes: 2

Views: 384

Answers (1)

alias
alias

Reputation: 30475

z3 can generate proofs in SMTLib mode (though the proof format is rather unspecified.) I'm not sure if it can even generate proofs in the CNF mode at all, though it certainly should be possible. Your best bet might be to file an issue at https://github.com/Z3Prover/z3/issues and see if this is supported.

Upvotes: 1

Related Questions