I am trying to implement an ILP solver based on ASTLogicSolver. However, I realize the Tnorm transformation generates non-linear constraints by using * to implement and and or. It should be possible to implement these ops in linear form, such that these constraints can be used in ILP.