Gophersat: A SAT solver written in Go | Hacker News Reader

Gophersat: A SAT solver written in Go

github.com

133 pointssacado236 comments

Tests might be a good place for early pull requests since they hardlink a specific /Users/ path:

https://github.com/crillab/gophersat/blob/7f9dbd11144643b0ee...

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.

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

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

[1]: https://github.com/Masterminds/glide/tree/gps-integration

[2]: https://github.com/golang/dep

Is it common for companies to ban LGPL?

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.

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.

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.

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/)

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).

It would be nice to have some usage hints.

Here is the generated godoc: https://godoc.org/github.com/crillab/gophersat/solver

'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.

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:

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 :

    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.

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)?

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.

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 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

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

No, polynomial time. For reference, see these Wikipedia pages:

https://en.wikipedia.org/wiki/Polynomial-time_reduction

https://en.wikipedia.org/wiki/Karp%27s_21_NP-complete_proble...

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.

Now it's a race to claim the obvious name...

ETA: too late. https://github.com/mndrix/golog

Golorp is still available.

Next step - SMT solver.

Or next step, answer-set solver.

constraint solver, pseudo boolean solver

Pseudo-boolean is on the todo-list. Constraints too, but they will happen later.

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

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

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

I’m about to make you feel old — the high score for the sat hasn’t been 1600 for 12 years.

He's not that old! CollegeBoard changed it last year so that 1600 is the maximum again.

And now I'm old :(!

I was thinking "separating axis theorem" and was really confused as to where the rest of the physics engine was.

It might be able to do that if it can handle a problem with enough variables.!

I think you just need A, B, C, and D, right? hint: the answer is C.

Reply on news.ycombinator.com