Watch This Space: How Two Simple Heuristics Outsmarted a Whole SAT Solver
A solver can lose time in a very boring place: deciding which internal bookkeeping trick to use. That sounds too small to matter. Business people usually expect optimization performance to come from grand architecture, better mathematical modeling, expensive hardware, or some heroic AI layer sprinkled on top. Researchers know better, though not always loudly enough. Sometimes the expensive part is not the model. It is the tiny repeated decision made millions of times while the solver tries to keep the model logically alive. ...