5 ms·
> ... SAT solvers only really seem to be good at Sudoku. This is really not true. SAT solvers are really good these days, and many (exact) algorithms (for NP-
by emil-lp 1y ago
> ... SAT solvers only really seem to be good at Sudoku.
This is really not true.
SAT solvers are really good these days, and many (exact) algorithms (for NP-hard problems) simply use some SOTA SAT solvers and are automatically competitive.
- roenxi 1y agoAt doing what, though? Why are they solving the SAT problem?
- emil-lp 1y agoBecause you can encode many (actually all) problems as a SAT instance, and the answer to that sat instance can be translated into an answer for the original problem.
- tannhaeuser 1y agoBefore you go and try to encode "all problems as SAT instance", I'd recommend to consider that SAT formulations require a fixed number of (Boolean) variables. Sure, you can use tens of thousands of helper variables to encode a problem, but at a certain point this gets unwieldy and basically all you're doing is working around SAT limitations and spend your time implementing a SAT encoder (and translator for the answer into your original domain language as you say). Even simple goal-directed block's world-like robotic planning problems where the number of moves and the items to pickup/putdown are variable are much easier formulated and solved using Prolog.
- maweki 1y agoIncremental automatic grounding to SAT works fine for ASP.
- pxx 1y ago"All" isn't right. You can only encode decision problems in NP into a SAT instance of polynomially-balanced size. Sure, that's a lot of things, but there are things provably not in this set.