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.

▲

kragen 4 days ago | parent [-]

You can implement DPLL in 30 lines of code? Not for SMT, I assume.

	▲	nextos 4 days ago \| parent [-]
		You'd need a fancy encoding for SAT to use a small DPLL implementation. Otherwise, customize DPLL for this particular problem.