7 ms·

Gophersat: A SAT solver written in Go

133 points by sacado2 9y ago

shamdasani 9y ago
I thought this would help me get a 1600 on my SAT :(
- PaulHoule 9y ago
  It might be able to do that if it can handle a problem with enough variables.!
  - pkaeding 9y ago
    I think you just need A, B, C, and D, right? hint: the answer is C.
- empath75 9y ago
  I’m about to make you feel old — the high score for the sat hasn’t been 1600 for 12 years.
  - brianyu8 9y ago
    He's not that old! CollegeBoard changed it last year so that 1600 is the maximum again.
    - FilterSweep 9y ago
      And now I'm old :(!
- eropple 9y ago
  I was thinking "separating axis theorem" and was really confused as to where the rest of the physics engine was.
xvilka 9y ago
Next step - SMT solver.
- dualogy 9y ago
  Or next step, answer-set solver.
  - rrobukef 9y ago
    constraint solver, pseudo boolean solver
    - sacado2 9y ago
      Pseudo-boolean is on the todo-list. Constraints too, but they will happen later.
carbocation 9y ago
Tests might be a good place for early pull requests since they hardlink a specific /Users/ path: https://github.com/crillab/gophersat/blob/7f9dbd11144643b0ee7881b6e55e851229057077/solver/solver_test.go#L31 https://github.com/crillab/gophersat/blob/7f9dbd11144643b0ee...
- sacado2 9y ago
  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.
zmonx 9y ago
Nice! SAT solvers reason about propositional logic, i.e., zeroth-order logic. Next step: Reason about first-order and higher-order logic. For example, with a Prolog engine written in Go.
- firethief 9y ago
  Now it's a race to claim the obvious name... ETA: too late. https://github.com/mndrix/golog https://github.com/mndrix/golog
  - monocasa 9y ago
    Golorp is still available.
baby 9y ago
It would be nice to have some usage hints. Here is the generated godoc: https://godoc.org/github.com/crillab/gophersat/solver https://godoc.org/github.com/crillab/gophersat/solver
- Gys 9y ago
  'Gophersat can be used as a standalone solver (reading DIMACS CNF files from a file or standard input) or as a library in any go program.' I assume more details about the inner workings requires a lot of documentation that can also be found elsewhere.
- sacado2 9y ago
  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: 1 2 3 0 4 5 6 0 -1 -4 0 -2 -5 0 -3 -6 0 -1 -3 0 -4 -6 0 The file starts with a prolog, which is `p cnf nb-vars nb-clauses`, so the whole file is p cnf 6 7 1 2 3 0 4 5 6 0 -1 -4 0 -2 -5 0 -3 -6 0 -1 -3 0 -4 -6 0 And, when given that input, gophersat answers : SATISFIABLE -1 2 -3 4 -5 -6 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.
ominous_prime 9y ago
Another Go SAT implementation (with an MIT license for those that can't use GPL): https://github.com/mitchellh/go-sat https://github.com/mitchellh/go-sat
- jzelinskie 9y ago
  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. [0]: https://github.com/sdboyer/gps https://github.com/sdboyer/gps [1]: https://github.com/Masterminds/glide/tree/gps-integration https://github.com/Masterminds/glide/tree/gps-integration [2]: https://github.com/golang/dep https://github.com/golang/dep
- acidtrucks 9y ago
  Is it common for companies to ban LGPL?
  - Newtopian 9y ago
    for many companies the fitness criterion is locked in proportionality to how much money it costs... for them LGPL is to be avoided at all costs.
  - ominous_prime 9y ago
    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.
    - cyphar 9y ago
      > 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.
kizer 9y ago
Is it usually linear to reduce other NP-complete problems to SAT?
- rw 9y ago
  No, polynomial time. For reference, see these Wikipedia pages: https://en.wikipedia.org/wiki/Polynomial-time_reduction https://en.wikipedia.org/wiki/Polynomial-time_reduction https://en.wikipedia.org/wiki/Karp%27s_21_NP-complete_problems https://en.wikipedia.org/wiki/Karp%27s_21_NP-complete_proble...
dbrophy 9y ago
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
bhoessen 9y ago
What about performances versus minisat/glucose/lingeling/... Do you plan to parallelize it? If so, using which technique
- sacado2 9y ago
  For the moment, it is in the sat4j ballpark. Parallelization will probably happen in the remote future.
mac01021 9y ago
Maybe someone here can satisfy my curiosity: 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.
- sacado2 9y ago
  Just a few examples. 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/ 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).

133 points by sacado2 9y ago

shamdasani 9y ago

I thought this would help me get a 1600 on my SAT :(

PaulHoule 9y ago
It might be able to do that if it can handle a problem with enough variables.!
- pkaeding 9y ago
  I think you just need A, B, C, and D, right? hint: the answer is C.
empath75 9y ago
I’m about to make you feel old — the high score for the sat hasn’t been 1600 for 12 years.
- brianyu8 9y ago
  He's not that old! CollegeBoard changed it last year so that 1600 is the maximum again.
  - FilterSweep 9y ago
    And now I'm old :(!
eropple 9y ago
I was thinking "separating axis theorem" and was really confused as to where the rest of the physics engine was.

xvilka 9y ago

Next step - SMT solver.

dualogy 9y ago
Or next step, answer-set solver.
- rrobukef 9y ago
  constraint solver, pseudo boolean solver
  - sacado2 9y ago
    Pseudo-boolean is on the todo-list. Constraints too, but they will happen later.

carbocation 9y ago

Tests might be a good place for early pull requests since they hardlink a specific /Users/ path: https://github.com/crillab/gophersat/blob/7f9dbd11144643b0ee7881b6e55e851229057077/solver/solver_test.go#L31 https://github.com/crillab/gophersat/blob/7f9dbd11144643b0ee...

sacado2 9y ago
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.

zmonx 9y ago

Nice! SAT solvers reason about propositional logic, i.e., zeroth-order logic. Next step: Reason about first-order and higher-order logic. For example, with a Prolog engine written in Go.

firethief 9y ago
Now it's a race to claim the obvious name... ETA: too late. https://github.com/mndrix/golog https://github.com/mndrix/golog
- monocasa 9y ago
  Golorp is still available.

baby 9y ago

It would be nice to have some usage hints. Here is the generated godoc: https://godoc.org/github.com/crillab/gophersat/solver https://godoc.org/github.com/crillab/gophersat/solver

Gys 9y ago
'Gophersat can be used as a standalone solver (reading DIMACS CNF files from a file or standard input) or as a library in any go program.' I assume more details about the inner workings requires a lot of documentation that can also be found elsewhere.
sacado2 9y ago
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: 1 2 3 0 4 5 6 0 -1 -4 0 -2 -5 0 -3 -6 0 -1 -3 0 -4 -6 0 The file starts with a prolog, which is `p cnf nb-vars nb-clauses`, so the whole file is p cnf 6 7 1 2 3 0 4 5 6 0 -1 -4 0 -2 -5 0 -3 -6 0 -1 -3 0 -4 -6 0 And, when given that input, gophersat answers : SATISFIABLE -1 2 -3 4 -5 -6 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.

ominous_prime 9y ago

Another Go SAT implementation (with an MIT license for those that can't use GPL): https://github.com/mitchellh/go-sat https://github.com/mitchellh/go-sat

jzelinskie 9y ago
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. [0]: https://github.com/sdboyer/gps https://github.com/sdboyer/gps [1]: https://github.com/Masterminds/glide/tree/gps-integration https://github.com/Masterminds/glide/tree/gps-integration [2]: https://github.com/golang/dep https://github.com/golang/dep
acidtrucks 9y ago
Is it common for companies to ban LGPL?
- Newtopian 9y ago
  for many companies the fitness criterion is locked in proportionality to how much money it costs... for them LGPL is to be avoided at all costs.
- ominous_prime 9y ago
  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.
  - cyphar 9y ago
    > 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.

kizer 9y ago

Is it usually linear to reduce other NP-complete problems to SAT?

rw 9y ago
No, polynomial time. For reference, see these Wikipedia pages: https://en.wikipedia.org/wiki/Polynomial-time_reduction https://en.wikipedia.org/wiki/Polynomial-time_reduction https://en.wikipedia.org/wiki/Karp%27s_21_NP-complete_problems https://en.wikipedia.org/wiki/Karp%27s_21_NP-complete_proble...

dbrophy 9y ago

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

bhoessen 9y ago

What about performances versus minisat/glucose/lingeling/... Do you plan to parallelize it? If so, using which technique

sacado2 9y ago
For the moment, it is in the sat4j ballpark. Parallelization will probably happen in the remote future.

mac01021 9y ago

Maybe someone here can satisfy my curiosity: 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.

sacado2 9y ago
Just a few examples. 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/ 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).