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.