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). _______________________________________________ Help-glpk mailing list [email protected] https://lists.gnu.org/mailman/listinfo/help-glpk
