Remix.run Logo
YetAnotherNick 5 days ago

General constraint solver would be terribly inefficient for problems like these. It's a linear problem and constraint solver just can't handle O(10^6) variables without some beefy machine.

OutOfHere 5 days ago | parent | next [-]

Okay, but who says you need to use a simple constraint solver? There are various sophisticated constraint solvers that know how to optimize.

At this point, job interviews are so far removed from actual relevance. Experience and aptitude still matter a lot, but too much experience at one employer can ground people in rigid and limiting ways of thinking and solving problems.

nextos 5 days ago | parent | prev | next [-]

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.

NoahZuniga 5 days ago | parent | prev [-]

O(10^6) = O(1)

dekhn 5 days ago | parent [-]

no, the "O" here is "on the order of", not Big O notation.

harperlee 5 days ago | parent | next [-]

I believe NoahZuniga is perfectly aware of the intent and denouncing an abuse of (unneeded) notation.

anonymars 5 days ago | parent | prev [-]

What is "Big O" if not literally "order of"?

NoahZuniga 5 days ago | parent | next [-]

The O stands for "Ordnung", the German word for order. So it does literally mean that, except mathematicians think that the order of f(x)=1 is the same as the order of f(x)=10^6, because "clearly" f(x)=x gets way bigger than any constant function.

dekhn 5 days ago | parent | prev [-]

In physics "order of" means "approximately" using something like a taylor series, which typically start with a constant, then move to higher polynomial terms which add smaller and smaller corrections. Similar, but different, I think...