Oops. Thanks. Those tests are outdated, we ran our own tests and benchmarks outside `go test`'s facilities, for practical reasons. This will be corrected very soon.
You're right, doc is very lacking for now. As Gys assumed correctly, when you work in the SAT solving field, using gophersat is very straightforward, but for a more wider audience, it is really lacking. A complete documentation and a tutorial about SAT for end users is a priority in the short term, but in a nutshell:
1. You have a problem that can be represented as a propositional formula (i.e boolean values). For instance : you have three employees, and you must have at least one employee working at any moment, and a given employee cannot work both in the morning and in the afternoon. Oh, and employees a and c don't work very well when they are together. You can represent it this way :
- e1-m means employee 1 works in the morning, e2-m employee 2 etc.
- e1-a means employee 1 works in the afternoon, etc.
- all those constraints (called "clauses") must be checked :
- e1-m or e2-m or e3-m (at least one employee in the morning)
- e1-a or e2-a or e3-a (at least one in the afternoon)
- not(e1-m) or not(e1-a) (e1 cannot work both in the morning and in the afternoon)
- not(e2-m) or not(e2-a)
- not(e3-m) or not(e3-a)
- not(e1-m) or not(e3-m) (e1 and e3 can't both work in the morning)
- not(e1-a) or not(e3-a)
So:
- you have a set of clauses, and all clauses must be true,
- each clause is a set of literals, and at least one of these literals must be true.
2. In the DIMACS file format, you associate each variable with an integer value (so, e1-m is 1, e2-m is 2, e3-m 3, e1-a 4, e2-a 5, e3-a 6). A negative value indicates the variable is expected to be false (so, -1 means "not(e1-m)").
Then, each line represents a clause and ends with a 0 (for historical reasons). The above problem would be:
Meaning "there is at least one way to solve your problem, for instance both 2 and 4 are true, everything else is false". So, e2 works in the morning, e1 in the afternoon, and e3 stays at home.
We will add, very soon, a facility function, to let the user submit this problem not only in a text format, but by providing a list of list of integers. Next step is providing user-friendly, higher-level input formats. Because, yes, providing DIMACS files for a given problem can be tricky and/or boring.
Do you have (or can you point me to) a good collection of these DIMACS files? That is, a good collection of representative SAT problems (and hopefully some pathological cases)?
Pathological cases aren't amazingly interesting for sat solvers. Everybody uses more or less the same base algorithm (DPLL) and its easy to exploit its search strategy to create exponential runtimes. All sat solvers explode for pathological cases but they still have practical use, so people care about real world inputs much more than ones designed to blow up your implementation.
You have a lot of huge, real-wold (industrial) examples on the website of the SAT 2017 competition. Be careful, however, these files are really huge (zip files in Gbytes) and the CNF files come "as is", i.e with no explanation about the underlying problem: https://baldur.iti.kit.edu/sat-competition-2017/benchmarks/
Classical one-player puzzles can be represented easily, and I'll include a tutorial and generators for those in the short run: sudoku and 8 queens, for instance. There's an article explaining how to represent the sudoku problem here : http://sat.inesc.pt/~ines/publications/aimath06.pdf (section 3).
As for pathological problems: the usual testcase for SAT solvers are random problems. They can be generated easily (I'll probably include a generator for them in the repository). You choose a number of variables , n (around n=300 things start to get interesting) and randomly generate n x 4.2 clauses (this is a sweet spot: less clauses and the problem tends to be easily solved, more clauses and it becomes easy to prove it cannot be solved). Those clauses must contain 3 literals, chosen randomly. Those problems are very hard to solve, even with a relatively small number of variables and clauses. But they are not that interesting in practice, because real-world problems are very different, they more structured and easier to solve.
There's also gps[0], which has been what the community has been working to integrate with dependency management tools since 2016[1] and is what's currently used in dep[2]. I'm not sure how generically applicable it is, though.
I think it's even more common with companies using Go, because the output is often statically linked which changes the distribution requirements. The main difference between GPL and LGPL is that the the latter allows proprietary or non-free software to be linked without creating a derivative work.
> The main difference between GPL and LGPL is that the the latter allows proprietary or non-free software to be linked without creating a derivative work.
That's not strictly correct. LGPL has the requirement that it must be possible to replace the components that are under LGPL. So you could statically link them as long as you provide separate .o files. Of course that's a bit harder with Go.
But the concept of derivative work comes from copyright law, your choice of license doesn't affect whether something is a derived work or not. All that changes is the set of restrictions.
At least at the major companies I have worked at (n=3), GPL is to be avoided, if at all possible. LGPL, to a lesser extent. The general impression I received was that it was cancerous.
You might also like to take a look at my boolean AST solver utility... I know nothing about SAT solving so it's probably rather naïve, but it was useful for me and takes AST as the input... So rather easier to use in some circumstances: github.com/dave/brenda
A very pragmatic one: Eclipse includes a SAT solver to manage package dependencies (eg: can package X be installed in version 1.0 and coexist with package Y with version <= 2.3)
SAT is also used for bounded model checking, ie checking whether a given system (hardware or software) is guaranteed to never be in an invalid state. You can have a look at MIT's alloy project (http://alloy.mit.edu/alloy/)
SAT is sometimes used in cryptography, to try to solve cryptographic problems.
SAT solvers are very efficient nowadays, so it often makes sense to translate an NP-complete problem into SAT. This is not always the case, though (some problems would require to generate a huge number of clauses, making the use of a SAT solver impractical).
36 comments
[ 9.2 ms ] story [ 79.1 ms ] threadhttps://github.com/crillab/gophersat/blob/7f9dbd11144643b0ee...
Next step: Reason about first-order and higher-order logic. For example, with a Prolog engine written in Go.
ETA: too late. https://github.com/mndrix/golog
Here is the generated godoc: https://godoc.org/github.com/crillab/gophersat/solver
I assume more details about the inner workings requires a lot of documentation that can also be found elsewhere.
1. You have a problem that can be represented as a propositional formula (i.e boolean values). For instance : you have three employees, and you must have at least one employee working at any moment, and a given employee cannot work both in the morning and in the afternoon. Oh, and employees a and c don't work very well when they are together. You can represent it this way :
So:- you have a set of clauses, and all clauses must be true,
- each clause is a set of literals, and at least one of these literals must be true.
2. In the DIMACS file format, you associate each variable with an integer value (so, e1-m is 1, e2-m is 2, e3-m 3, e1-a 4, e2-a 5, e3-a 6). A negative value indicates the variable is expected to be false (so, -1 means "not(e1-m)").
Then, each line represents a clause and ends with a 0 (for historical reasons). The above problem would be:
The file starts with a prolog, which is `p cnf nb-vars nb-clauses`, so the whole file is And, when given that input, gophersat answers : Meaning "there is at least one way to solve your problem, for instance both 2 and 4 are true, everything else is false". So, e2 works in the morning, e1 in the afternoon, and e3 stays at home.We will add, very soon, a facility function, to let the user submit this problem not only in a text format, but by providing a list of list of integers. Next step is providing user-friendly, higher-level input formats. Because, yes, providing DIMACS files for a given problem can be tricky and/or boring.
Classical one-player puzzles can be represented easily, and I'll include a tutorial and generators for those in the short run: sudoku and 8 queens, for instance. There's an article explaining how to represent the sudoku problem here : http://sat.inesc.pt/~ines/publications/aimath06.pdf (section 3).
As for pathological problems: the usual testcase for SAT solvers are random problems. They can be generated easily (I'll probably include a generator for them in the repository). You choose a number of variables , n (around n=300 things start to get interesting) and randomly generate n x 4.2 clauses (this is a sweet spot: less clauses and the problem tends to be easily solved, more clauses and it becomes easy to prove it cannot be solved). Those clauses must contain 3 literals, chosen randomly. Those problems are very hard to solve, even with a relatively small number of variables and clauses. But they are not that interesting in practice, because real-world problems are very different, they more structured and easier to solve.
[0]: https://github.com/sdboyer/gps
[1]: https://github.com/Masterminds/glide/tree/gps-integration
[2]: https://github.com/golang/dep
That's not strictly correct. LGPL has the requirement that it must be possible to replace the components that are under LGPL. So you could statically link them as long as you provide separate .o files. Of course that's a bit harder with Go.
But the concept of derivative work comes from copyright law, your choice of license doesn't affect whether something is a derived work or not. All that changes is the set of restrictions.
https://en.wikipedia.org/wiki/Polynomial-time_reduction
https://en.wikipedia.org/wiki/Karp%27s_21_NP-complete_proble...
What are the significant applications (industrial, military, or scientific) of SAT solvers?
They're not just a theoretical curiosity are they?
The wikipedia entry describes a number of algorithms, but is silent about their use (or lack thereof) in the world.
A very pragmatic one: Eclipse includes a SAT solver to manage package dependencies (eg: can package X be installed in version 1.0 and coexist with package Y with version <= 2.3)
SAT is also used for bounded model checking, ie checking whether a given system (hardware or software) is guaranteed to never be in an invalid state. You can have a look at MIT's alloy project (http://alloy.mit.edu/alloy/)
SAT is sometimes used in cryptography, to try to solve cryptographic problems.
SAT solvers are very efficient nowadays, so it often makes sense to translate an NP-complete problem into SAT. This is not always the case, though (some problems would require to generate a huge number of clauses, making the use of a SAT solver impractical).