Comment by nextos
17 hours ago
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.
You'd need a fancy encoding for SAT to use a small DPLL implementation.
Otherwise, customize DPLL for this particular problem.