4 ms·
Aren't those modeling languages? I believe they hook up to actual solvers which may or may not be SAT solvers.
by sevensor 8y ago
Aren't those modeling languages? I believe they hook up to actual solvers which may or may not be SAT solvers.
- Karrot_Kream 8y agoPiCat seamlessly integrates with solvers. MiniZinc does need a solver capable of processing it, but it's fairly easy to do so. I just thought this kind of problem was a bit easier to describe more generally in a constraint form than SAT (which takes a bit of effort).
- sevensor 8y agoI see your point -- CNF as a modeling language leaves a lot to be desired. What I like about this article is that it uses CNF anyway and takes you through the hard work you'd have to do to express a problem that way. I didn't know about the Tseytin transformation, for instance, so I'd given up on using CNF because of the exponential blowup in my constraints. I probably still won't be using SAT solvers directly, but it's nice to learn how they work. It's like knowing an assembly language for constraint satisfaction.