11 ms·

What would be a concrete problem you could solve with SAT solvers, besides the obvious "satisfy this boolean expression" (which doesn't exactly come up every da

• maxmunzel 7y ago
  As its applicable to all discrete Problems (think of Sudoku), its a really neat skill to have. Reductions are pretty easy to write and modern SAT solvers are crazy fast.
• thanatropism 7y ago
  It's not difficult to reduce scheduling problems that are usually done with dynamic programming etc. to SAT. Then there's SATPLAN. If I had VC money I would be seeking young'uns trying to change the world with SATPLAN, of course in a way that's married to machine learning. (Machine learning doesn't "think", it "learns"; logic-based AI "thinks" but can't "learn"). E: part 1 says at the outset: > As an example, the often-talked-about dependency management problem, is also NP-Complete and thus translates into SAT[2][3], and SAT could be translated into dependency manager. The problem our group worked on, generating key and lock cuttings based on user-provided lock-chart and manufacturer-specified geometry, is also NP-complete.< Part 3 is already deep in the rabbit hole of comparing heuristics. People like me just write something that "compiles" to DIMACS and fires Minisat.
  • 6gvONxR4sf7o 7y ago
    A primary problem in marrying logic to ML is doing so in a differentiable way. i.e. when your SAT part of the system is suboptimal, how do you know which parameters of the learned part to change, and in which direction?
    • nl 7y ago
      We propose Differentiable Satisfiability and Differentiable Answer Set Programming (Differentiable SAT/ASP) for multi-model optimization. Models (answer sets or satisfying truth assignments) are sampled using a novel SAT/ASP solving approach which uses a gradient descent-based branching mechanism. https://arxiv.org/abs/1812.11948 https://arxiv.org/abs/1812.11948
    • smallnamespace 7y ago
      From the article, a lot of the heuristics seems to revolve around and 1) which variables to try first 2) which learned clauses to keep in your set. Assign scores and differentiate on those scores. This is (very loosely) how AlphaGo also works - you take a tree-based algorithm (MCTS) and then use neural nets to score the next node to expand.
    • mlevental 7y ago
      you don't need differentiability you just need a learning rule. there are learning algorithms that don't use gradient ascent.
• sudhirj 7y ago
  I’ve had a supply demand problem that I couldn’t figure out how to use a SAT solver for - thousands of demands ( movies have to reach thousands of theatres) with tens of possible paths (fedex, satellite, download) - each at different costs, some impossible and costs will change with volume and consideration of other similar deliveries. Have a solution that models each choice of supply demand tuples as nodes in a tree and doing depth first search on it. Any ideas on how to switch to an SAT solver? How would I even write such a large SAT Boolean expression, and how would I tell the SAT solver that the costs will change for each choice depending on business rules and other choices made? It seemed impossible with a SAT system but I assume I’m not familiar enough with the concepts.
  • ahmedalsudani 7y ago
    What are you trying to do? Show that deliveries can be made or minimize the cost? If you’re minimizing the cost, shouldn’t this be formulated as an optimization problem?
    • jvanderbot 7y ago
      Yes. That's a MILP. And if we think SAT solvers are useful and underused, wait till you start working with MILP solvers.
      • nickpsecurity 7y ago
        I think it was this year I learned they exist. They told me a few to check out. I still don't have a list of applications. What areas were you thinking about when you said underused?
      • shaklee3 7y ago
        Yes, yes, yes. I've made this comment a few times on here but tools like MIP solvers are vastly unknown since they didn't take on a sexy name when they started out. However, they can outperform most heuristic based algorithms, and even solve some of the largest problems. It's how the NFL makes their schedules oh, and you can imagine how complicated that is.
• yissp 7y ago
  IIRC the dpkg package manager in Debian uses a SAT solver for dependency resolution.
  • kiliankoe 7y ago
    As do many language package managers, e.g. Dart's pub.
  • Conan_Kudo 7y ago
    Debian does not have a SAT solver powered package manager. That said, DNF package manager in Fedora, Mageia, OpenMandriva, and Yocto uses a SAT solver. As does the Zypper package manager in (open)SUSE.
• __s 7y ago
  Minesweeper: https://yurichev.com/blog/minesweeper_SAT_SN https://yurichev.com/blog/minesweeper_SAT_SN Hexiom: https://github.com/hugomg/hexiom https://github.com/hugomg/hexiom
  • travisjungroth 7y ago
    Those are games, not practical problems. I find SAT solvers exciting, but at the same time I’m so disappointed by how few problems they solve. So far it seems to be dependency management and key cutting.
    • __s 7y ago
      Why fund DeepMind? Blink stalker micro & beating some old board game can't possibly be useful. Yes, we should also ignore Game Theory because it's just games, nothing practical The complaint was having to compile problems into boolean satisifiability problems. Here we see one need only describe their problems as puzzles. These examples are nice in that they include code that shows how straight forward description of these problems can be
      • travisjungroth 7y ago
        I called those out as not practical problems because the commenter specifically asked for that. I’m all for research, but there’s this bait and switch that goes on with SMT solvers. They’re presented as useful (TFA says “underused”) and when someone asks for real life use cases, people show minesweeper.
    • thanatropism 7y ago
      The beautiful thing about this line of research is that if you have a problem that can be reduced to key cutting, you're set. Particularly if you can learn the lock-charts (or whatever the data looks like in your higher-level problem domain) from data. The magic sauce is in being able to combine these things. Chuck a bag full of keys, sans known tumblers (those are embedded in doors, you don't steal doors) into a machine and learn with eg. stochastic gradient descent what are tumblerset-candidates that satisfy the entire system. Sensor arrays + AI that thinks + machine learning = wow.
• teraflop 7y ago
  Not sure how concrete/practical you'd consider this, but here's one: In last year's Advent of Code programming contest, one of the trickier problems involved taking a collection of points in 3D space, each of which has a "range" defined by Manhattan distance, and finding the location that is "in range" of the maximum number of them. Now, this isn't a theoretically intractable problem. Each point defines the center of an octahedral volume of space, and by repeatedly slicing each volume using the others' boundaries, you can partition the entire space into something like O(N^3) disjoint pieces. You can then enumerate these pieces to determine which one is contained in the largest number of octahedra. But actually implementing this is tricky; each piece ends up having an irregular polyhedral shape, and calculating the geometry of their boundaries would be non-trivial. Instead, some of the participants noticed out that you could represent the constraints as a formula: find (x,y,z) that maximize sum((|x-xi| + |y-yi| + |z-zi|) < ri) and then just feed it to a SAT/SMT solver such as Z3. This is probably less computationally efficient, but in practice it runs reasonably quickly, and it's vastly easier to code. (The Advent of Code scoring system is based almost entirely on the time taken to come up with a correct solution, so it strongly favors solutions that are quick to implement.) Here's one such solution: https://www.reddit.com/r/adventofcode/comments/a8s17l/2018_day_23_solutions/ecdbux2/ https://www.reddit.com/r/adventofcode/comments/a8s17l/2018_d...
  • forrestthewoods 7y ago
    Day 23, that was a fun one! It’s pretty easy to solve with an octree. My goal was run-time speed rather than quickest solution. My octree solution runs in ~3 milliseconds. If memory serves, the Z3 solver took around 17 seconds on the same machine. I made a nifty (imho) video that shows the octree traversal order. There’s no need to create irregular shapes. https://www.forrestthewoods.com/blog/solving-advent-of-code-in-under-a-second/ https://www.forrestthewoods.com/blog/solving-advent-of-code-...
• CJefferson 7y ago
  Surprisingly, for many problems (including travelling salesman), Sat solvers are very competitive. I research in this area and it is a constant source of annoyance when you come up with a clever special algorithm which then gets beaten by translation to SAT. SAT particularly exceeds when you have side constraints. Imagine travelling salesman where you have to top up petrol only in cities, or where you need to sleep at night, or some roads are slower at rush hour, or you have a particular place you want to be at a particular time/date. A specialised travelling salesman solver would be useless for any of these. Adding side constraints to SAT is simple. In general, I wouldn't try to write sat models directly unless you are writing a logic problem. Consider looking at conjure ( https://github.com/conjure-cp/conjure https://github.com/conjure-cp/conjure ) which adds a nice language on top, and get target various NP complete solvers, including Sat (which often is the best). (I'm one of the minor conjure developers)
  • codeflo 7y ago
    That's really interesting. But how does it actually work, in practice, to find an optimal TSP path given a SAT solver? I know there's a reduction proof, but if I remember correctly, the proof I learned involved transforming TSP from an optimization problem into a series of multiple decision problems of the form "Is there a path with length less than k?". That would mean running the SAT solver multiple times to get the right path length. Is that efficient enough, or is there a better way to do this?
    • hugomg 7y ago
      Some SAT solvers allow you to add additional constraints while they are running. So you can find a solution and then add additional constraints to try to get it to find a better one.
    • prutschman 7y ago
      It's more than just a SAT solver, but Microsoft's Z3 SMT solver has an option to minimize a quantity of interest. I haven't worked with it much, but it seemed faster than a binary search on 'k' when I was playing around with a non-TSP problem. https://rise4fun.com/Z3/tutorialcontent/optimization https://rise4fun.com/Z3/tutorialcontent/optimization
• andrepd 7y ago
  I'm working in first-order logic theorem proving (which obviously has far greater applications than propositional SAT: from mathematical proof checking, to software and hardware verification, e.g. compiler optimisation checking, to integration in higher-order solvers, etc.). Our algorithm is based on the idea of abstracting the first-order problem to a propositional one, which is then passed to a SAT solver! If it is inconsistent, so is the first order problem and we're done. If not, the SAT problem is satisfiable and we can use the solution to guide a "refinement" of the propositional abstraction, which is again passed to the SAT solver, and so on. If no "refinement" can be made, the first-order problem is satisfiable. We do reasonably well on the annual CASC competition of theorem provers (we're iprover), even winning a division where this approach is particularly strong! [1]: http://www.tptp.org/CASC/27/ http://www.tptp.org/CASC/27/
  • est31 7y ago
    Great talk by Kathleen Fisher on this topic. Also mentions SAT solvers. https://youtu.be/TH0tDGk19_c https://youtu.be/TH0tDGk19_c
  • Footpost 7y ago
    Our algorithm ... Unless I completely misunderstand what you write, the approach you describe is the standard way of setting up SMT-solvers by interaction between a SAT solver with a theory solver. I think it is called lazy SMT or DPLL(T) in [1] where this approach seems to have been described first. [2] is also an interesting description of the phenomenon. [1] H. Ganzinger, G. Hagen, R. Nieuwenhuis, A. Oliveras, C. Tinelli, DPLL(T): Fast Decision Procedures. https://www.cs.upc.edu/~oliveras/espai/papers/dpllt.pdf https://www.cs.upc.edu/~oliveras/espai/papers/dpllt.pdf [1] R. Nieuwenhuis, A. Oliveras, C. Tinelli, Abstract DPLL and Abstract DPLL Modulo Theories. http://www.cs.upc.edu/~roberto/papers/lpar04.pdf http://www.cs.upc.edu/~roberto/papers/lpar04.pdf
    • andrepd 7y ago
      I read both those papers ;) I guess that you can think of our algorithm as lazy SAT modulo quantified first order logic, with the crucial difference that first order logic is undecidable. But anyway in this case the "decision procedure for T" would just be checking whether any two complementary literals which are true in the model are unifiable, which is decidable. Paper: http://www.cs.man.ac.uk/~korovink/my_pub/inst_gen_modular.pdf http://www.cs.man.ac.uk/~korovink/my_pub/inst_gen_modular.pd...
• pfdietz 7y ago
  Concolic testing https://en.wikipedia.org/wiki/Concolic_testing https://en.wikipedia.org/wiki/Concolic_testing Basically, the problem "find an input that causes the program to execute this sequence of statements". --- Identification of missing optimizations in the LLVM backend. https://github.com/google/souper https://github.com/google/souper
• BeniBoy 7y ago
  I found this blog post quite interesting[1]. The author is optimising rack positionning to minimise cabling. However, trying to use his method to optimise a linear typewriter[2] proved unsuccessful, as projected solving time was around 13 million years. [1]https://yurichev.com/blog/cabling_Z3/ https://yurichev.com/blog/cabling_Z3/ [2]https://www.benjaminpoilve.com/projects/typewriter-optimisation.html https://www.benjaminpoilve.com/projects/typewriter-optimisat...
  • zimpenfish 7y ago
    Yeah, I tried Z3 (and other things) for the typewriter (my write up is linked at the bottom of the original linear typewriter post) and got nothing useful out of it - even with extra constraints like "make sure E and T are close together". (But your 13M years is a lot quicker than my projected seven hundred ninety-eight trillion, seven hundred twenty billion, nine hundred fifty-two million, one hundred seventy-six thousand, seven hundred and forty-five years you'd need for an exhaustive search of the 26! possibilities.)
• oldgradstudent 7y ago
  Heavily used in hardware design and verification. Equivalence checking, logic synthesis and optimisation, formal verification, etc.
• rixed 7y ago
  In my current project, I started using a SMT solver to type a language I'm compiling (find out the "best" types for every expression). Then I also used it for storage ressource allocations (finding out which programs should store their output so that later retrieval is the cheapest), and then again to layout some graph on the GUI; and I have another similar use case already in mind. Of the many ways to solve a complex problems that we have on our tool box -- algorithms, neural networks, constraint solvers -- I would totally agree to say that solvers are underused. But when you get used to them it's not hard to find use cases.
• munificent 7y ago
  If you use a programming language with a package manager like npm, PIP, CPAN, Pub, Cargo, Bundler, etc. then every time you ask it to figure out what versions of your dependencies to use, you are effectively running a SAT solver. In particular, pub — the package manager for Dart — explicitly uses the CDCL process described in the article: https://medium.com/@nex3/pubgrub-2fb6470504f https://medium.com/@nex3/pubgrub-2fb6470504f
  • tcard 7y ago
    A notable exception being Go modules, which do Minimal Version Selection [1], a much simpler approach. [1] https://research.swtch.com/vgo-mvs https://research.swtch.com/vgo-mvs
• Veedrac 7y ago
  If you're willing to overlook that Z3 is a more general SMT solver, it's a useful tool for one-off problems where raw brute-force is inefficient. I used this to proof-of-concept an attack on Seahash[1]; this was the first time I'd ever used an SMT solver, but it was really very straightforward. [1] https://gitlab.redox-os.org/redox-os/tfs/issues/5#note_9768 https://gitlab.redox-os.org/redox-os/tfs/issues/5#note_9768
• jfries 7y ago
  I have used them to prove equivalence between pseudo code and optimized production code. Several rounding-related tricks and a too large search space made it very difficult to prove with traditional testing.
• c22 7y ago
  I used a SAT solver awhile ago to build a program that scheduled retail employees based on preferences set by both the employer and the employees.
• moonlet 7y ago
  Via routing, pin placement, optimizing logic, and probably a couple other hardware problems that are also nondeterministic and not coming to mind right now.
• sweeneyrod 7y ago
  Pedantry: you can reduce TSP to SAT just because it's in NP. It's the opposite reduction (from SAT to TSP) that you can do because TSP is NP-complete.
• pdobsan 7y ago
  SAT, its extensions and SMT solvers are heavily used in bioinformatics. For example in genetics and for protein folding problems.
• aseipp 7y ago
  An easy case that I've used multiple times is equivalence checking. In other words: phrase a problem like "are these two programs equal" as "Is there any input X that can satisfy the following: F(X) != G(X)". If you can compute F and G as boolean functions, a SAT solver can often quickly and easily give you an answer. If the solver says this equation is unsatisfiable (UNSAT), then they're equal. Otherwise, it will give you a counterexample: an input X where F(X) isn't the same as G(X). Three examples I've done this for, myself. - Hardware circuits: is a hand-optimized combinational function (optimized with hand-written karnaugh maps, or whatever) equivalent to a high level specification? You could for example use this to write N versions of an instruction decoder, a reference spec and versions specialized to different hardware devices, and check them all together. - Packet processing: are two different firewall/packet filters equivalent? In other words, is there any packet P for which two filters F(P) and G(P) have different results? This might be useful for example as a cloud user to ensure certain assumptions can't be violated (locking out necessary ports, etc) - Cryptographic code: is this piece of C code equivalent to a high level specification? Is it still the same if I optimize it? This is possible by bounding the input of the code and then extracting models from them. You can do this in practice for pretty interesting functions. For example, I showed a reference spec of ChaCha20's RFC was equivalent to some C code I wrote, up-to some bounded stream length. (Unfortunately when SIMD is involved it's trickier to pull this off but that's mostly a technical limitation more than a theoretical one.) There is a variant of the third approach I've also seen used: an easy way of attacking weak RNGs! For example, the ancient JellyBean version of Android had a weak RNG at one point that allowed Bitcoin wallets to be stolen by cracking the keys. Effectively, this PRNG was seeded with a 64-bit state. But 64-bits isn't that much: two different seeds may possibly collide and give the same resulting random value. So here's how you phrase the problem: instead of equality, you're basically trying to prove the PRNG is non-injective. If R(n) is a function that takes a seed state 'n' and produces a pseudo-random number, then translate R to boolean expression, and ask this question: forall x y, iff x != y, R(x) == R(y). Are there any two values `x` and `y` that are not equal, but do result in the same resulting RNG values? If this equation is satisfiable, then your RNG is weak. In practice, a SAT solver can prove this is the case for the JellyBean RNG in less than 0.1 seconds. And you can also do it the other way, prove injectivity: forall x y, x == y || R(x) != R(y). You prove that for all x,y either x and y are equal, and if they're not, they will never result in the same output. This can also be proved in less than a fraction of a second. [1] SAT solvers and SMT solvers are useful for a wide variety of practical applications, but they are not magic. You just need a bit of familiarity with them, and you'll probably find a lot of problems can be phrased that way! The secret, of course, is actually learning how to phrase problems in a manner that a SAT solver can actually work with. That's an entirely different problem. [1] You actually want to prove something slightly different: forall x y, not(x == y || R(x) != R(y)). You want to find two inputs that result in "unsatisfiable" in this case. Negating the result gets you that: if any two x/y are not the same, but R(x) == R(y), then the overall result is 'true', which is a satisfiable case with a counter example.
• jlebar 7y ago
  A practical example is the Alive theorem prover, which found many bugs in LLVM's instcombine pass (i.e. peephole optimizations) and which we now use to prove the correctness of new transformations. https://rise4fun.com/Alive https://rise4fun.com/Alive https://blog.regehr.org/archives/1170 https://blog.regehr.org/archives/1170
• mazesc 7y ago
  I'm a co-author of a paper where we use program synthesis to optimize big-data (i.e., slow-running) SQL queries. The synthesis engine we use encodes its search problems into SAT. https://www.microsoft.com/en-us/research/wp-content/uploads/2017/11/sosp17-final219.pdf https://www.microsoft.com/en-us/research/wp-content/uploads/...
  • vsrinivasan 7y ago
    Hello, i am CS undergrad.i wish to learn about program synthesis. while researching online for courses available. i came across the one offered at univ of washington and a few more, they do not have video lectures.if possible, please provide pointers on the right place to start.
    • mazesc 7y ago
      Hi,this blog post is a good starting point: https://alexpolozov.com/blog/program-synthesis-2018/ https://alexpolozov.com/blog/program-synthesis-2018/ Among other documents, it links to this extensive survey: https://www.microsoft.com/en-us/research/wp-content/uploads/2017/10/program_synthesis_now.pdf https://www.microsoft.com/en-us/research/wp-content/uploads/... All the best!
• Galanwe 7y ago
  > What would be a concrete problem you could solve with SAT solvers, besides the obvious "satisfy this boolean expression" (which doesn't exactly come up every day)? Say, you want to implement a package manager, with dependencies.
• ychen306 7y ago
  Program verification. E.g. when you want to prove that certain condition/path (e.g. asserts) is unreachable.
• dustfinger 7y ago
  Air Traffic Reschedualing [1]. The algorithm is using hard constraints rather than soley relying on machine learning. I believe that the paper is essentially describing a SAT solver strategy that is used by a machine learning algorithm. The agorithm should also great for employee reschedualing, or any kind of reschedualing where you want to find the nearest solution anytime the last known solution is invalidated by a state change. [1] https://www.researchgate.net/publication/259823636_Addressing_Hard_Constraints_in_the_Air_Traffic_Problem_through_Partitioning_and_Difference_Rewards https://www.researchgate.net/publication/259823636_Addressin...
• spsx 7y ago
  I think reducing the TSP to a SAT problem is not a very efficient approach. MIP solvers have become extremely sofisticated (and implement many of the techniques of SAT and much more) and offer a much more powerful modeling paradigm. it's hard to imagine a SAT solver outperforming them on such problems.