Out-of-order decisions

This release contains the version of the solver used for the paper titled 'Should Decisions in QCDCL Follow Prefix Order?' In particular, it contains the new feature of being able to make variable decision irrespective of dependencies, whether implicit or learned. This is activated with --out-of-order-decisions off|existential|universal|all. For this, the 3-watched-literal data structure was implemented, and it is automatically used when out-of-order decisions are active. It is also possible to run in ordinary dependencies-respecting mode with 3 watched literals, using --watched-literals 3.