From Moshe Vardi: implement scalable benchmark formulas from a paper

[MassimoLauria]

During a workshop in Toronto: Theoretical Foundation of SAT Solving 2016, Moshe Vardi suggested to implement some scalable benchmarks from

See http://www.cs.rice.edu/~vardi/papers/sat04rj.pdf