3 ms·
Because 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 pro
by emil-lp 1y ago
Because 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.