Satisfiability (SAT) solvers have become complex tools, which raises the question of whether we can trust their results. This question is particularly important when the solvers are used to determine the correctness of hardware and software and when they are used to produce mathematical results. To deal with this issue, solvers can provide proofs of unsatisfiability to certify the correctness of their answers. This chapter presents the history and state-of-the-art of producing and validating proofs of unsatisfiability. The chapter covers the most popular proof formats with and without hints to speed up certification. Hints in proofs make validation easy, which resulted in several efficient formally-verified checkers. Various proof systems are discussed, ranging from resolution to the recent propagation redundancy system. The chapter also describes techniques to compress and optimize proofs.
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
Tel.: +1 703 830 6300
Fax: +1 703 830 2300 firstname.lastname@example.org
(Corporate matters and books only) IOS Press c/o Accucoms US, Inc.
For North America Sales and Customer Service
West Point Commons
Lansdale PA 19446
Tel.: +1 866 855 8967
Fax: +1 215 660 5042 email@example.com