This encoding adds (n-1)*k variables (n is the number of variables in the
at most constraint and k is the degree of the constraint) and 2nk+n-3k-1
clauses.
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.
That method is designed to be used to retrieve the real model of the
current set of constraints, i.e. to provide the truth value of boolean
variables used internally in the solver (for encoding purposes for
instance).
Declare howmany variables in the problem (and thus in the
vocabulary), that will be represented using the Dimacs format by integers
ranging from 1 to howmany.
To know the number of variables used in the solver as declared by
newVar()
In case the method newVar() has not been used, the method returns the
number of variables used in the solver.
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