Naive approach to count the solutions available in
a boolean formula: each time a solution is found,
a new clause is added to prevent it to be found again.
Lazy data structure for clause using the Head Tail data structure from SATO,
The original scheme is improved by avoiding moving pointers to literals but
moving the literals themselves.
Perform some sanity check before constructing a clause a) if a literal is
assigned true, return null (the clause is satisfied) b) if a literal is
assigned false, remove it c) if a clause contains a literal and its
opposite (tautology) return null d) remove duplicate literals e) if the
clause is empty, return null f) if the clause if unit, transmit it to the
object responsible for unit propagation