ANNOUNCE: gini

847 views
Skip to first unread message

Scott Cotton

unread,
Jul 23, 2016, 5:33:31 PM7/23/16
to golang-nuts
I'm happy to announce the first public beta release of mini, available at 
github.

Gini is a SAT solver with some related tools built for solving the canonical NP-complete SAT problem.  SAT solvers have many applications in formal verification and discrete optimisation,
often acting as an indispensable component in these domains.

Gini is written in 100% pure go and thus far, our core CDCL solver either outperforms or is competitive with analogs in C/C++ like picosat and minisat.  Additionally, internal measures of raw speed such as mega-props/second  are good and independent of variations arising from  heuristics.

By bringing a high quality SAT solver to go, we hope to enable competitive innovations in the go community which tackle combinatorial explosion symbolically.

Gini is in first beta public release, following the recent SAT competition.  To maintain performance in the long term, we plan to have gini compete in sat races and sat competitions annually. To this end, we are happy to collaborate with gophers, the curious, raw speed junkies, algorithm officianados, and logicians alike.  

Cheers,


--
Scott Cotton
President, IRI France SAS


James Pirruccello

unread,
Jul 23, 2016, 7:15:01 PM7/23/16
to golang-nuts
This seems incredibly useful. I wonder if you'd consider creating an example project as a demonstration, showing what import path we should be using and very basic operation -- I think it would help get interested people onboard quickly. Thanks for considering!

- James

Markus Zimmermann

unread,
Jul 24, 2016, 6:55:39 AM7/24/16
to golang-nuts
I also would like to see some examples. Also, please make the whole project go-getable.

Looking forward to see where this project is going, exciting! Can you link to the papers where you demonstrate that you outperform picosat and minisat?

Scott Cotton

unread,
Jul 24, 2016, 6:50:37 PM7/24/16
to golang-nuts
Thanks James.

For library usage, there are examples in the _test files, which will have to do for the moment.  The gini command 
takes dimacs cnf and icnf inputs.  see satcompetition.org for details.

As for import path, we have chosen to use simply

import "gini"
or sub packages like "gini/ax"

This is unfortunately incompatible with go get'ing remote repositories, but on the other hand the source directories and import statements don't need to name a website, which we feel is cumbersome.  We may set up a website for gini, and make it go gettable at that time, but it is not top priority at the moment.

Nonetheless, you can clone with git and install/test/etc using go install.  If you'd like to discuss that further, feel free to file an issue.

Best

Scott

Scott Cotton

unread,
Jul 24, 2016, 6:50:37 PM7/24/16
to golang-nuts
There is a tool for solver benchmarking provided in the package.

As I see you're from JKU linz, home of picosat, Here's a comparison of core cdcl gini with core cdcl picosat on 50 randomly selected problems from the 2011 sat competition, with a timeout of 1 minute per problem,  benchmark suite constructed, run, and summarised by the above mentioned tool (I hope monospaced fonts 
show up ok in this forum...)

Suite sc11-r50

-----------------------------------------------------------------------------------------------------------

| Run                  | solved   | sat      | unsat     | unknown |  time      | utime      | stime      |

-----------------------------------------------------------------------------------------------------------

| g768l                | 29       | 15       | 14        | 21      |  1410.94s  | 1387.34s   | 0.00   s   |

-----------------------------------------------------------------------------------------------------------

| ps                   | 28       | 14       | 14        | 22      |  1567.51s  | 1555.18s   | 0.00   s   |

-----------------------------------------------------------------------------------------------------------

../suites/sc11-r50: ps v g768l

                                                                            ★ / 

                                                                            ★   

                                                                          /     

                                                                        /       

                                                                      /         

                                                                    /           

                                                                  /             

                                                                /               

                                                              /                 

                                                            /                   

                                                          /                     

                                                        /                       

                                                      /                         

                                                    /                           

                                                  /                             

                                                /                               

                                              /                                 

                                            /                                   

                                          /                                     

                                        /                                       

                                      /                                         

                                    /                                           

                                  /                                             

                                /                                               

                              /                                                 

                            /                                                   

                          / ☆                       ☆                           

                        /                                                       

                      /                                                         

                    /                                                           

                  /             ☆                                               

                /                                                               

              /     ☆                                                       ☆   

            /                             ☆       ☆                             

          /             ☆                                                       

  ★     /                                                                       

      /                                                                         

★   ☆       ☆                                                                   

★ / ☆             ☆                                                             

★                                                                               

                                        

--------------------------------------------------------------------------------

★ - ps wins

☆ - g768l wins



This is SAT, it is a hard and heuristic problem.  Your results may vary, and certainly there exists problems where other solvers are better (this is true for every solver).

We are in the process of drafting/submitting some papers related to gini.

Enjoy,
Scott

Justin Israel

unread,
Jul 28, 2016, 6:18:14 PM7/28/16
to golang-nuts
Neat. I had been using pigosat for a project. It vendors the picosat C dependency right in. 
Cool to see a pure Go solution.

Justin

Scott Cotton

unread,
Jul 29, 2016, 10:22:51 AM7/29/16
to golang-nuts
Thanks.

Out of curiosity, are you using sat solvers in visual effects pipelines?

Scott

Justin Israel

unread,
Jul 29, 2016, 6:01:44 PM7/29/16
to Scott Cotton, golang-nuts


On Sat, 30 Jul 2016, 2:22 AM Scott Cotton <w...@iri-labs.com> wrote:
Thanks.

Out of curiosity, are you using sat solvers in visual effects pipelines?

I was using it for a new version of the package dependency resolver component  of our environment management system. 
I was able to model the entire "repository"  of software package descriptions and their dependencies. Then add the specific package selections for an environment as constraints and resolve that back into the full list of needed packages. 
The useful bit in pigosat is that I can have it generate the cause of the failure to solve and convert that back into human readable reporting. 

--
You received this message because you are subscribed to the Google Groups "golang-nuts" group.
To unsubscribe from this group and stop receiving emails from it, send an email to golang-nuts...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Justin Israel

unread,
Jul 29, 2016, 6:06:53 PM7/29/16
to Scott Cotton, golang-nuts


On Sat, 30 Jul 2016, 10:01 AM Justin Israel <justin...@gmail.com> wrote:


On Sat, 30 Jul 2016, 2:22 AM Scott Cotton <w...@iri-labs.com> wrote:
Thanks.

Out of curiosity, are you using sat solvers in visual effects pipelines?

I was using it for a new version of the package dependency resolver component  of our environment management system. 
I was able to model the entire "repository"  of software package descriptions and their dependencies. Then add the specific package selections for an environment as constraints and resolve that back into the full list of needed packages. 
The useful bit in pigosat is that I can have it generate the cause of the failure to solve and convert that back into human readable reporting. 

I've actually got these extra wrapped api called in my own fork because the original author didnt yet merge them


The trace is awesome for explaining to a user why the solve failed. 

Scott Cotton

unread,
Jul 30, 2016, 9:46:31 PM7/30/16
to golang-nuts


Neat,  maybe a bit like sat4j does in eclipse dependency management?

For generating the cause of a failure, do you mean "failed assumptions" in picosat speak or 
unsat core or some other feature (proofs, etc)?

Scott

2016-07-30 0:01 GMT+02:00 Justin Israel <justin...@gmail.com>:


On Sat, 30 Jul 2016, 2:22 AM Scott Cotton <w...@iri-labs.com> wrote:
Thanks.

Out of curiosity, are you using sat solvers in visual effects pipelines?

I was using it for a new version of the package dependency resolver component  of our environment management system. 
I was able to model the entire "repository"  of software package descriptions and their dependencies. Then add the specific package selections for an environment as constraints and resolve that back into the full list of needed packages. 
The useful bit in pigosat is that I can have it generate the cause of the failure to solve and convert that back into human readable reporting. 


Scott

Justin Israel

unread,
Jul 31, 2016, 1:20:29 AM7/31/16
to Scott Cotton, golang-nuts


On Sun, 31 Jul 2016, 1:46 PM Scott Cotton <w...@iri-labs.com> wrote:
Neat,  maybe a bit like sat4j does in eclipse dependency management?

Probably similar I am sure. For standard distro package management systems I think they have to be concerned with the idea of installing new or upgrading existing or removing unneeded.
Since ours is just an environment management system, we have a slightly less complicated goal. We just need to find the total working resolve of the package set so that we can build a shell environment from the combination


For generating the cause of a failure, do you mean "failed assumptions" in picosat speak or 
unsat core or some other feature (proofs, etc)?

I would have to look at it again, but I think it was the dimac proof that you get from a failed solve when picosat is compiled with trace support (which it is in the pigosat bindings) . It's the actual progression of clauses and assumptions that lead to a fail.

Markus Zimmermann

unread,
Aug 6, 2016, 2:50:38 AM8/6/16
to golang-nuts
Nice. I put your solver on my benchmarking list for our use-cases. I hope I get to that in the following months. I am exceptionally excited to see a pure Go SAT solver :-) Are you trying to get in the next SAT competition?

I created an issue in the tracker about resolving the go-getable issue. It is really easy to solve. Also, I noticed that you are not following some conventions, so my recommendation would be to automatically integrate gofmt (for safety), govet, golint, goerrcheck and others using a CI like TravisCI (it is free for open source projects). Automatically testing and linting has its perks. You could use https://github.com/alecthomas/gometalinter or have a look at one of my projects on how to integrate them plus TravisCI.

Scott Cotton

unread,
Aug 11, 2016, 11:52:39 AM8/11/16
to golang-nuts
Hi Markus,

Apologies for the delay, been a busy week.

Yes we are planning to enter the coming SAT competitions, and we are seeking help/resources from interested parties.  Would be great to have a bona-fide team.  There are a number of categories of submissions to the SAT competitions, and I think Gini is in a good place to serve as a foundation for upcoming competitions.

What use-cases are referring to?

Re: go-gettable, there is an issue with the project for discussing that in more detail.  The problem is not so much technical as it is ready-ness to define a canonical URL or to re-organize the project without a dedicated "src" directory.

Travis-CI looks nice.  Provided it works with our directory layout without jumping through too many hoops, I think we'll set that up soon.  Thanks for the 
pointers.

Scott 
Reply all
Reply to author
Forward
0 new messages