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.
Remove a constraint returned by one of the add method from the solver
that is subsumed by a constraint already in the solver or to be added to
the solver.
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