  The robustness and correctness of SAT solvers are receiving more and more
attention. In recent SAT competitions, a proof of unsatisfiability emitted by
SAT solvers must be checked. So far, no proof checker has been efficient for
every case. In the SAT competition 2016, some proofs were not verified within
20000 seconds. For this reason, we decided to develop a more efficient proof
checker called TreeRat. This new checker uses a window shifting technique to
improve the level of efficiency at which it verifies proofs of
unsatisfiability. At the same time, we suggest that tree-search-based SAT
solvers should use an equivalent relation encoding to emit proofs of
subproblems. In our experiments, TreeRat was able to verify almost all proofs
within 20000 seconds. On this point, TreeRat is shown to be superior to
gratgen, which is an improved version of DRAT-trim. Also, in most cases,
TreeRat is faster than gratgen. Like DRAT-trim, TreeRat can output also trace
dependency graphs. Its output format is LRAT. The correctness of TreeRat can be
ensured by checking its LRAT output.
