Comment by nextos
FWIW, the OP's problem is not linear. It's an integer programming problem.
A trick if you can't do a custom algorithm and using a library is not allowed during interview could be to be ready to roll your own DPLL-based solver (can be done in 30 LOC).
Less elegant, but it's a one-size-fits-all solution.
You can implement DPLL in 30 lines of code? Not for SMT, I assume.