Understanding SAT by Implementing a Simple SAT Solver in Python (2014)(sahandsaba.com)
sahandsaba.com
Understanding SAT by Implementing a Simple SAT Solver in Python (2014)
https://sahandsaba.com/understanding-sat-by-implementing-a-simple-sat-solver-in-python.html
4 comments
And even with CDCL and 2-WL a new implementation won't come anywhere near the performance of the best. The engineering precision involved in 3k core lines of minisat/Glucose is astounding: pre-processing, in-processing, optimalisations, multiple heuristics (VSIDS, LBD, agressive restarts), domain specific cache-aware generational garbage collection...
Competitive SAT solvers are little diamonds of engineering.
Competitive SAT solvers are little diamonds of engineering.
I feel like I both agree and disagree. It is true that beating glucose or lingeling at the SAT competition would require a lot more engineering than just plain CDCL + 2 literal watching. At the same time, I think a lot of the new stuff (which in my book is everything that's happened in SAT post 2007ish) is primarily focused on winning the SAT competition by taking a sort of kitchen-sink approach.
For instance, CryptoMinisat first implemented XOR detection along with Gaussian elimination. They were using SAT on cryptographic problems, so it made sense to specialize for that domain. But now there's a bunch of crypto-based problems in the SAT competition and many of the other solvers also implement Gaussian elimination. But I'd guess that most users of SAT solvers wouldn't see a noticeable performance difference if you got rid of Gaussian elimination from the solvers.
Another good example is Alan Mischenko's ABC which wins the hardware model checking competition every year but uses a fairly ancient version of MiniSAT as its SAT solving engine. It's not that a faster solver wouldn't make ABC faster, but that the real smarts in model checking are in what queries you send to the solver, not in squeezing an extra 2X or 3X performance out of the SAT solver using the same old dumb queries.
For instance, CryptoMinisat first implemented XOR detection along with Gaussian elimination. They were using SAT on cryptographic problems, so it made sense to specialize for that domain. But now there's a bunch of crypto-based problems in the SAT competition and many of the other solvers also implement Gaussian elimination. But I'd guess that most users of SAT solvers wouldn't see a noticeable performance difference if you got rid of Gaussian elimination from the solvers.
Another good example is Alan Mischenko's ABC which wins the hardware model checking competition every year but uses a fairly ancient version of MiniSAT as its SAT solving engine. It's not that a faster solver wouldn't make ABC faster, but that the real smarts in model checking are in what queries you send to the solver, not in squeezing an extra 2X or 3X performance out of the SAT solver using the same old dumb queries.
Most things I listed are pre-2007, minisat 2.2 had all but literal block distance. Which, I think, has proven itself since glucose replaced minisat in the hack thread.
You're probably right about the kitchen sink approach, however without it we probably wouldn't have MapleSat. MapleSat uses machine learning to replace the VSIDS heuristic. A bold move, but it has been replicated this year.
I checked (got curious about what ABC does): ABC uses minisat 2.2 as default and satoko (for 3 years) and glucose 3.0 (for 2 years) as options. I don't know which configuration they used for the competitions. I think I saw "bmc -g" in some of the slides which would indicate glucose. However I also saw "abc super_solve" for which the name gives no information. (Maybe not the same years)
Indeed, smart applications of SAT solvers do more than raw performance. Though, every little bit helps. Are you going to tell scientists what they should research? :)
You're probably right about the kitchen sink approach, however without it we probably wouldn't have MapleSat. MapleSat uses machine learning to replace the VSIDS heuristic. A bold move, but it has been replicated this year.
I checked (got curious about what ABC does): ABC uses minisat 2.2 as default and satoko (for 3 years) and glucose 3.0 (for 2 years) as options. I don't know which configuration they used for the competitions. I think I saw "bmc -g" in some of the slides which would indicate glucose. However I also saw "abc super_solve" for which the name gives no information. (Maybe not the same years)
Indeed, smart applications of SAT solvers do more than raw performance. Though, every little bit helps. Are you going to tell scientists what they should research? :)
Do you think it could be used by an AI? Use cases for natural language understanding?
[deleted]
Correct 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...
Internally we use SAT solvers to schedule resources on medical devices which makes the device look "smart", but this is not AI...
Yes, 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!
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!
It 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?
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?
SAT 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)
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)
There are also probabilistic SAT solvers for cases where there isn't just one true logical answer, e.g., https://github.com/MatthiasNickles/delSAT
I am trying to implement a natural language (English) logic checker.
It would detect https://en.m.wikipedia.org/wiki/Formal_fallacy
How could a SAT/SMT help me in this task? I know it's already used for math theorem checking.
E.g All men are mortal. Socrates is a man. Therefore Socrate is mortal. I have currently two way to solve syllogisms
One hard-coded Disjonction of cases (but not flexible enough for non canonical forms of syllogisms)
And a flexible one that generate a graph of transitivity.
Both are 100% accurate.
Could SAT/SMT give me a third way of determining if the conclusion is logically valid? (not non sequitur)
How could a SAT/SMT help me in this task? I know it's already used for math theorem checking.
E.g All men are mortal. Socrates is a man. Therefore Socrate is mortal. I have currently two way to solve syllogisms
One hard-coded Disjonction of cases (but not flexible enough for non canonical forms of syllogisms)
And a flexible one that generate a graph of transitivity.
Both are 100% accurate.
Could SAT/SMT give me a third way of determining if the conclusion is logically valid? (not non sequitur)
This is exactly what SAT and SMT are for.
SMT is some extra stuff on top of SAT. There are a few frameworks which extend SAT. I'd look at minizinc, it is a fairly easy to use language which can produce SAT (and SMT, and others) as output. Often encoding things in SAT directly gets arkward.
SMT is some extra stuff on top of SAT. There are a few frameworks which extend SAT. I'd look at minizinc, it is a fairly easy to use language which can produce SAT (and SMT, and others) as output. Often encoding things in SAT directly gets arkward.
Thank you but as you say, encoding is limiting.
SMT are a progress versus SAT.
But I believe I would need an SMT that take a graph and rules as input and verify if the graph or parts of the graph satisfy the rules/constraints.
And output me the indexes of the satisfied parts of the graph.
I believe such a thing does not yet exist.
This is what model checkers are for. They internally (might) use SAT solvers to reason over transition graphs.
The general problem for model checkers is of this form:
System description: Transition system like automata or a guarded command language which induces a graph.
System Property: Stated in some logic, CTL/LTL
Output: Satisfied, or Unsatisfied with a counter example (usually a path in the graph which is false).
If your problem can fit into such a framework, have a look at model checkers: https://en.wikipedia.org/wiki/List_of_model_checking_tools
System description: Transition system like automata or a guarded command language which induces a graph.
System Property: Stated in some logic, CTL/LTL
Output: Satisfied, or Unsatisfied with a counter example (usually a path in the graph which is false).
If your problem can fit into such a framework, have a look at model checkers: https://en.wikipedia.org/wiki/List_of_model_checking_tools
Deep neural networks don't help with problems where there is no solution; neural networks approximate functions where the explicit form of the function is unknown. For example nobody knows how to implement isCat(animal) without using machine learning, but we have enough data on cats to approximate said function without much trouble.
SAT solvers work out if it is possible to satisfy a logical model (hence the name).
In theory a neural network could approximate a function that solves SAT. In practice it is a much better idea to use a SAT solver. Neural networks aren't that powerful at solving logic puzzles.
SAT solvers work out if it is possible to satisfy a logical model (hence the name).
In theory a neural network could approximate a function that solves SAT. In practice it is a much better idea to use a SAT solver. Neural networks aren't that powerful at solving logic puzzles.
There are many ways to see differences between the two.
One is heuristic vs algorithm. If SAT solver finds a solution, it's correct. If ANN finds a solution, it might be correct.
ANN is suitable for pattern recognition, statistical learning and representation learning. Learning continuous functions for example. SAT solvers work best for discrete problems.
One is heuristic vs algorithm. If SAT solver finds a solution, it's correct. If ANN finds a solution, it might be correct.
ANN is suitable for pattern recognition, statistical learning and representation learning. Learning continuous functions for example. SAT solvers work best for discrete problems.
I 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
Feel free to ask any questions.
Feel free to ask any questions.
Thanks! 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).
I'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.
I 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...
Also: have you looked at the poly-algorithm for 4-coloring? I rather write the SAT instance by hand...
If 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#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%93L...
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%93L...
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 while 2-literal watching is from the Chaff solver: https://www.princeton.edu/~chaff/publication/DAC2001v56.pdf.