We present a proof-producing search engine for solving the Boolean
satisfiability problem. We show how the proof-producing
infrastructure can be used to track the dependency information needed
to implement important optimizations found in modern SAT solvers. We
also describe how the same search engine can be extended to work with
decision procedures for quantifier-free first-order logic. Initial
results indicate that it is possible to extend a state-of-the-art SAT
solver with proof production in a way that both preserves the
algorithmic performance (e.g. the number of decisions to solve a
problem) and does not incur unreasonable overhead for the proofs.