9 ms·
SATisfying Solutions to Difficult Problems
- zkmon 11mo agoProblems, including NP-complete ones, are only a product of the way you look at them and the reference frame from where you look at them. They get their incarnation only out of the observer's context.
- ViscountPenguin 11mo agoI love SAT solvers, but way more underappreciated by software engineers are MILP solvers. MILPs (Mixed Integer Linear Programs) are basically sets of linear constraints, along with a linear optimization functions, where your variables can either be reals or ints. Notably, you can easily encode any SAT problem as a MILP, but it's much easier to encode optimization problems, or problems with "county" constraints as MILPs.
- muragekibicho 11mo agoSATs are cool but MILPs are cooler IMO. Lol I've been trying to train a neural network over a finite field, not the reals and oh my god MILPs are God's gift to us.
- ViscountPenguin 11mo agoHuh, that's an interesting idea. If you get sick of MILPs, maybe you could use a representation of your finite field instead of the field itself? That way you could do everything in C^n, and preserve differentiability to use SGD or something like it.
- sirwhinesalot 11mo agoBoth are severely underused for sure. But it didn't help that for a long time open source MILP solvers were pretty mediocre. HiGHS didn't exist, SCIP was "non-commercial", CBC was ok but they've been having development struggles for awhile, GLPK was never even remotely close to commercial offerings. I think if something like Gurobi or Hexaly were open source, you'd see a lot more use since both their capabilities and performance are way ahead of the open source solutions, but it was the commercial revenue that made them possible in the first place. Using CP-SAT from Google OR-Tools as a fake MILP solver by scaling the real variables is pretty funny though and works unreasonably well (specially if the problem is highly combinatorial since there's a SAT solver powering the whole thing)
- FreakLegion 11mo agoSCIP going Apache definitely improved the landscape, but Couenne (global MINLP), Bonmin (local MINLP), and IPOPT (local NLP, but e.g. [1] gets you MINLP) are solid and have been around for a long time. And anecdotally, I've seen a lot more issues with SCIP (presolvers and tolerances, mostly) than with other solvers. Still it's replaced Couenne in my toolbox, and Minotaur has replaced Bonmin, but IPOPT remains king of its domain. 1. E.g. https://en.wikipedia.org/wiki/Randomized_rounding https://en.wikipedia.org/wiki/Randomized_rounding.
- sirwhinesalot 11mo agoDidn't know about Randomized rounding. Is there any solver with built-in support for that? To turn a strong NLP solver into a fast but approximate MINLP solver?
- FreakLegion 11mo agoNot necessarily randomized rounding in particular, but many solvers use rounding methods internally e.g. as part of a feasibility pump. Minotaur and SCIP definitely do this.
- zvr 11mo agoMany thanks to you and the parent comment for providing names to search when looking for implementations. A basic question, before searching these: are they "input compatible"? I mean, can a problem be formulated once and then be solved by a variety of solvers? Or does each one of them use its own input language?
- sirwhinesalot 11mo agoFor MILP there isn't one single standard, but multiple competing solutions. Nearly every solver supports the MPS format, but that's a really old format straight from the era of punchcards, it sucks. Many solvers support the nl format, which is a low level format spat out by the AMPL tool (commercial software for mathematical modeling). Many solvers support the CPLEX lp format, which is a nice human readable and writable format. Google OR-Tools includes an API for mathematical modeling that supports the relevant open source MIP solvers plus Gurobi I think and its own CP solver. There are Python and Julia packages that try to do the same (rather than calling the solver APIs directly they usually spit out a problem in nl format though). MiniZinc supports various open source MILP solvers plus various CP solvers. Very nice language, very high level. For MINLP the only standard I know of is OSiL but support for it is spotty, mostly supported by open source tools I think.
- roenxi 11mo agoI've always been fascinated by how linear programming seems to be applicable to every problem under the sun but SAT solvers only really seem to be good at Sudoku. In practice that are a bunch of problems that seem to be SAT, but they are either SAT at a scale where the solver still can't find a solution in any reasonable time or they turn out to not really be SAT because there is that one extra constraint that is quite difficult to encode in simple logic. And it is unrewarding experimenting because it ends up being a day or so remembering how to use a SAT solver, then rediscovering how horrible raw sat solver interfaces are and trying to find a library that builds SAT problems from anything other than raw boolean algebra (the intros really undersell how bad the experience of using SAT solvers directly is, the DIMACS sat file format makes me think of the year 1973), then discovering that a SAT solver can't actually solve the alleged-SAT problem. Although if anyone is ever looking for a Clojure library I can recommend rolling-stones [0] as having a pleasant API to work with. [0] https://github.com/Engelberg/rolling-stones https://github.com/Engelberg/rolling-stones
- emil-lp 11mo ago> ... SAT solvers only really seem to be good at Sudoku. This is really not true. SAT solvers are really good these days, and many (exact) algorithms (for NP-hard problems) simply use some SOTA SAT solvers and are automatically competitive.
- roenxi 11mo agoAt doing what, though? Why are they solving the SAT problem?
- emil-lp 11mo agoBecause 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 11mo ago
- fjfaase 11mo agoIf you convert a sudoku to an exact cover you can usually solve it by finding colums that are a subset from another column and remove all rows that are only in one of them. Sudokus that can be solved with reasoning alone, can be solved in polynomial time. I recently discovered that solving exact covers, and probably also with SAT, using a generic strategy, does not always result in the most efficient way for finding solutions. There are problems that have 10^50 solutions, yer finding a solution can take a long time.
- eru 11mo ago> Sudokus that can be solved with reasoning alone, [...] Is 'reasoning alone' actually well defined in the context of Sudoku? Sudoku's are finite, so I can solve all of them with just a lookup table in constant time..
- muragekibicho 11mo agoI coded the paper Sinkhorn Solves Sudoku. Lol the most bizarre algorithms can solve sudoku. https://github.com/MurageKibicho/Sinkhorn-Solves-Sudoku https://github.com/MurageKibicho/Sinkhorn-Solves-Sudoku
- fjfaase 11mo agoThe link https://leetarxiv.substack.com/sinkhorn-solves-sudoku https://leetarxiv.substack.com/sinkhorn-solves-sudoku reports 'Page not found'.
- muragekibicho 11mo agoI've not yet published the writeup. Only the C code is available atm. I solo run a thing called LeetArxiv. It's a successor to Papers with Code since the latter shut down.
- mxkopy 11mo agoSlightly related, there’s ways to differentiate linear programs (https://github.com/cvxpy/cvxpylayers https://github.com/cvxpy/cvxpylayers), which might allow one to endow deep neural networks with some similar reasoning capabilities as these sorts of solvers.
- js8 11mo agoI don't understand why SAT solvers don't use gaussian elimination more. Every SAT problem can be represented as an intersection of linear (XORSAT) and 2SAT clauses, and the linear system can resolve some common contradictions, propagate literals, etc. Also Grobner basis algorithm over polynomials in Z_2 can be used to solve SAT. A SAT problem can be encoded as a set of quadratic polynomials, and if the generated ideal is all polynomials, the system is unsatisfiable (that's Nullstellenansatz). I don't understand how we can get high degree polynomials when running Grobner basis algorithm that specifically prefers low degree polynomials. It intuitively doesn't make sense.
- dooglius 11mo agoSAT is NP-complete, and both gaussian elimination and 2SAT are polynomial-time, so this would suggest either you're mistaken or there is some hidden catch here (like the size of one or the other being exponential-sized).
- js8 11mo agoThere is no catch - I even describe the reduction in another comment below. You can convert a 3SAT clause to a combination of XORSAT and 2SAT clauses. I am not mistaken, either, I used this reduction many times on practical problems, so I know it works. I encourage you to try it. Unfortunately, putting the algorithms for XORSAT and 2SAT together is not trivial at all, they are quite different (but Grobner bases over GF(2) seem very promising in that). But I agree that the fact that both XORSAT and 2SAT have polynomial algorithms is quite a strong indicator that full SAT has a one too. :-) (On the other hand, there is IMHO only very little actual evidence for P!=NP.)
- sirwhinesalot 11mo agoI have no idea about most of the words you wrote but I'd love to see alternative approaches to SAT solving. CryptoMiniSAT has native support for Gaussian Elimination but it has to put a lot of effort into recovering XORs from the CNF. A different format (XORSAT + 2SAT) plus an efficient algorithm to exchange information from the two sides of the problem would be interesting.
- isolay 11mo agoThis is interesting, but techniques like CDCL seem to only ever find any one valuation that makes a proposition true. My homegrown solver finds all valuations that make a proposition true and then can eliminate redundancies, such that `X or not X and Y` gets simplified to `X or Y`, just to mention one example (proof: truth tables are identical). Are there any other SAT solvers out there that do something like that? My own one suffers from combinatorial explosion in the simplification stage when expressions get "complex" enough. But then, the simplification is NP-complete, AFAICT.
- emil-lp 11mo agoIt's not very difficult to turn a CDCL solver into an ALL-SAT solver, and there are many publications available doing exactly that.
- fcholf 11mo agoI would also add that #SAT solvers, aiming at counting the number of solutions, are often implicitly solving the ALL-SAT in a more efficient manner than what you would have with modified CDCL solvers because they use other caching and decomposability techniques. Check knowledge compiler d4 for example https://github.com/crillab/d4v2 https://github.com/crillab/d4v2 that can build some kind of circuits representing every solution in a factorized yet tractable way.
- thesz 11mo ago> This is interesting, but techniques like CDCL seem to only ever find any one valuation that makes a proposition true. Most, if not all, current SAT solvers are incremental. They allow you to add clauses on the fly. So, when you find the solution, you can add a (long!) clause that blocks that solution from appearing again and then run solver again. Most, if not all, SAT solvers have a command line option for that enumeration done behind the scenes, for picosat it is "picosat --all".
- sirwhinesalot 11mo agoFor problems with a very large number of solutions this quickly becomes inefficient. The blocking clauses will bog down the solver hard and waste tons of memory. A more clever approach is to emulate depth-first search using a stack of assumption literals. The solver still retains learned conflict clauses so it's more efficient than naive DPLL.
- jgalt212 11mo agoAt PyCon 2019, Raymond Hettinger did a nice talk on Python interfaces to a variety of solvers. https://www.youtube.com/watch?v=_GP9OpZPUYc https://www.youtube.com/watch?v=_GP9OpZPUYc