Hacker News Reader

I experimented with MIPS before, mainly for side projects, and I found them amazing for easily solving optimization problems. Reading this article, I felt the logic used for constructing the Sudoku solver is quite close to what I would have done for MIPS: one constraint for one number per row, one constraint for the columns, one constraint for the 3x3 boxes, etc…

I am wondering if MIPS and SAT relate together somehow?

View on HN

You can solve SAT problems using linear programming, I believe. I don't know if the free SAT solvers would compare to a commercial LP solver like gurobi or cplex.

Integer programming, not linear programming. Linear programming (without the integrality constraint) is in P, so you cannot use it to solve general SAT problems, which are NP-complete (unless a major and highly surprising theoretical breakthrough is found).

The free SAT solvers are very good, and much better than commercial IP solvers at solving problems that are a natural fit for SAT. (Obviously, you can encode any IP as an SAT formula and vice versa, and the IP solvers are better at solving the problems where you actually have meaningful arithmetic.)

Thanks for clearing that up!

Reply on news.ycombinator.com