116 ms·
Definitely agree that they are criminally underused. I used to work for a large virtualization company, and used a SAT solver to walk an extremely complex depe
by Patrick_Devine 8y ago
Definitely agree that they are criminally underused. I used to work for a large virtualization company, and used a SAT solver to walk an extremely complex dependency graph. We had originally been using a simple hill climbing algorithm and the SAT solver absolutely trounced it in terms of performance.
The biggest problem though, was when I would describe how we were using SAT to solve the graph, I generally would get extremely puzzled looks. Most other engineers have no exposure to them whatsoever.
- AlphaSite 8y agoSolvers in general are an amazing piece of tech.
- analognoise 8y agoA hill climbing algorithm doesn't make any sense to me for a dependency graph, it doesn't fit the domain at all. Is there a canonical reference you'd recommend to understand this problem or a paper I could look at that was similar to this implementation?
- Jugglerofworlds 8y agoSometimes discrete graph theory problems can be relaxed into a continuous space where gradient descent can be used. If you want a concrete example of how this happens, take a look at the "Continuous Optimization" section in the "Thirty Years of Graph Matching in Pattern Recognition" paper (graph/subgraph isomorphism).
- analognoise 8y agoThank you, I will investigate this.