5 ms·
Understanding SAT by Implementing a Simple SAT Solver in Python (2014)
- grecht 7y agoI'm confused why he brings up the four color theorem, since a 4-coloring of a planar graph can be determined in polynomial time. And he also makes it sound like the theorem hasn't been proven yet.
- maweki 7y agoI think it's fine taking this as a constraint problem. It just means, you know beforehand that there is a solution. Also, if the underlying problem is in P, chances are the SAT instance is not that hard. Also: have you looked at the poly-algorithm for 4-coloring? I rather write the SAT instance by hand...
- maxmunzel 7y agoI wrote a dpll (the standard algorithm for SAT) Implementation in Haskell, that’s also pretty straight forward: https://github.com/maxmunzel/dpll/blob/master/README.md https://github.com/maxmunzel/dpll/blob/master/README.md Feel free to ask any questions.
- hwwc 7y agoThanks! I did a port of it and this could be my way in to discovering more about SAT solvers. (Doing ports is one of my preferred means of jumpstarting my motivation for more complex areas of study).
- wsxcde 7y agoThe practical significance of SAT is that almost all modern verification techniques are based on SAT solvers. The algorithm he describes is not very interesting because it doesn't even implement unit-propagation. The idea with unit propagation is that if my current assignment has set a variable A=True and I also have a clause (~A + B) then B must be true for the instance to be satisfiable. Unit propagation is about propagating such implied constraints. If he'd implemented unit propagation along with his brute force search he'd have ended up with what is called the DPLL algorithm for SAT. Modern SAT solvers are actually even smarter and have two important improvements over DPLL: (i) Conflict-Driven Clause Learning (CDCL) which introduced a very cool technique called non-chronological backtracking, and (ii) 2-literal watching which is an extremely clever data structure for efficient unit propagation. Both of these ideas are generalizable to many other versions of constraint solving (e.g. sudoko, router search, etc.) so they are well worth learning. CDCL was introduced by this paper: https://dl.acm.org/citation.cfm?id=244560 https://dl.acm.org/citation.cfm?id=244560 while 2-literal watching is from the Chaff solver: https://www.princeton.edu/~chaff/publication/DAC2001v56.pdf https://www.princeton.edu/~chaff/publication/DAC2001v56.pdf.
- The_rationalist 7y agoDo you think it could be used by an AI? Use cases for natural language understanding?
- deleted 7y ago[deleted]
- milsebg 7y agoCorrect me if I'm wrong, but this is usually not handled by SAT solvers, is it? Internally we use SAT solvers to schedule resources on medical devices which makes the device look "smart", but this is not AI...
- The_rationalist 7y agoYes, the idea of using SAT/SMT for solving/helping AI tasks is far from mainstream. But I was wondering if there is a potential, if so for what tasks? I said on another comment that I work on a logic checker for English, detecting automatically logical fallacies from text. I consider such a task to be AI and how could SAT help to check if the conclusion of a syllogism follow? "Internally we use SAT solvers to schedule resources on medical devices" this is cool!
- The_rationalist 7y agoIt is said that SAT is very useful for automatically solving complex problem where you don't know the solution. But deep learning neural network are also said to be used when there's no good solution known. It's the first time I see the symmetry. When should I use a SAT vs an ANN? Other than SAT and ANN, are there other kind or technology that automatically solve/approximate solutions?
- CJefferson 7y agoSAT is best when there is one true logical answer. ANN are best when you want "best advice". A good guide (in my experience) -- with SAT while the answer is hard to find it's easy to check (like a Sudoku, or building a timetable with no clashes), while ANN give answers where verifying the answer isn't easy to perform computstionally (if I give you a translation of a text into Latin, verifying it is about as hard as just making a new one from scratch)
- carapace 7y agoIf you liked that you might like this. It's a DPLL† SAT Solver based on George Spencer-Brown's Laws of Form implemented in Python. http://joypy.osdn.io/notebooks/Correcet_Programming.html#Davis%E2%80%93Putnam%E2%80%93Logemann%E2%80%93Loveland-(DPLL)-algorithm-SAT-Solver http://joypy.osdn.io/notebooks/Correcet_Programming.html#Dav... One of the interesting things about it is that you don't have to put formulas into conjunctive normal form. † https://en.wikipedia.org/wiki/Davis%E2%80%93Putnam%E2%80%93Logemann%E2%80%93Loveland_algorithm https://en.wikipedia.org/wiki/Davis%E2%80%93Putnam%E2%80%93L...