sentence1: they typically require solving a mixed integer problem or satisfiability modulo theory solvers .
sentence2: these typically employ either satisfiability modulo theories solvers or integer programming approaches .