Hacker News new | past | comments | ask | show | jobs | submit login

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!




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: