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.
