Toward leaner binary-clause reasoning in a satisfiability solver