Use a specific data structure for binary clauses compatible with reason simplification
The support for binary clauses as proposed by Lawrence Ryan in his thesis was removed because not compatible with reason simplification.
There are many cases where the amount of memory is huge and the unit propagation is slow because the instance is mainly composed of binary clauses.
We should add back such data structure in order to reduce the memory footprint of the solver on such problems. It will only happen if we find a nice solution compatible with reason simplification.