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 Le samedi 6 août 2016 08:50:38 UTC+2, Markus Zimmermann a écrit : > > 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.
