Hacker News Reader

Second paragraph of 382 of http://facta.junis.ni.ac.rs/eae/fu2k73/7wille.pdf mentions how SAT solvers create BDD. I’m not super familiar with using the proofs of unsat from a solver, but I think it’s basically the BDD that shows there is no satisfying assignment.

View on HN

Well this is true but CDCL SAT solvers do not materialize this BDD and they stop as soon as they find a satisfying assignment. If they do not find any satisfying assignment, they do not return the BDD as unsat proof but roughly the list of learnt clause. If these clauses have been learnt using vanilla CDCL solver technique, one can check from this that the formula is indeed unsat. See the (D)RAT proof format (check e.g., references listed for this tool https://www.cs.utexas.edu/~marijn/drat-trim/).

Reply on news.ycombinator.com