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. On Monday, July 25, 2016 at 12:50:37 AM UTC+2, Scott Cotton wrote: > > 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 > > Le dimanche 24 juillet 2016 12:55:39 UTC+2, Markus Zimmermann a écrit : >> >> 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? >> >> On Saturday, July 23, 2016 at 11:33:31 PM UTC+2, Scott Cotton wrote: >>> >>> I'm happy to announce the first public beta release of mini, available >>> at >>> github <http://github.com/IRIFrance/gini>. >>> >>> 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 >>> http://www.iri-labs.com >>> >>> >>> -- 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+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
