On Sat, May 5, 2012 at 1:49 AM, Andrew Makhorin
<address@hidden> wrote:
See also Tseitin's transformations:
http://en.wikipedia.org/wiki/Tseitin-Transformation
These transformations can be used to describe any Boolean function in a
more or less efficient way, in particular, to model any digital circuit
logic like adders, multipliers, dividers, etc.
The mip preprocessor implemented in glpk uses these transformations to
reduce the mip instance to the satisfiablity problem in order to find an
integer feasible solution with the Minisat solver (--minisat).