Hi, Gini was benchmarked on a reasonably sized set of randomly selected sat competition problems against minisat and picosat. It did very well, before there was even gophersat. SAT competition problems are much harder than many application use case problems because they are of interest as a challenge to solver developers.
Gophersat, last I checked said it was much slower than standard C sat solvers such as these. Gini outperformed picosat and minisat (by minisat, I mean the core cdcl solver, not with preprocessing, which is not a cop-out because pre-processing has it's own problems for applications). Also, Gini still has the issue of array bounds checking. When I bench mark it, there is a package which I compile with bounds checking off, and it makes quite a significant difference on some problems. So it seems to me, from the points above, that gophersat will probably be better, is questionable. My take is this: anybody using SAT in an actual application needs to benchmark for that application. It might well even be that any difference between solvers is simply irrelevant performance-wise. Don't take my word for it, or gophersat's authors word for it. Bench mark. You can use the tool "bench" with gini to easily do this for cnf at least for any solver. (Also, Gini now supports cardinality constraints. It uses a simple mechanism which is known to be effective for a wide number of use cases and has absolutely no overhead w.r.t. solving problems without cardinality constraints. Handling cardinality constraints is also difficult to predict; I recommend ignoring all expert opinions about who is better and simply benchmark). Scott On Friday, 22 December 2017 02:25:53 UTC+1, Fabien wrote: > > Short answer : according to the few tests I ran, they are pretty close. > You can use any of them, or, even better, both of them. > > Long answer : > > I have only compared them on about a dozen industrial problems, so take it > with a grain of salt, but it's hard to name a winner. Gini is usually a > little faster, but when it is slower, it is way slower than Gophersat. Gini > is very good (sometimes even better than state-of-the-art C++ solvers, like > glucose) on some very easy problems (those that can be solved in about 10 > to 50 ms), probably because it has a very good parser and low warmup costs. > But it is not as good on harder problems, and it can only deal with pure > SAT, CNF problems (and they can be exponentially bigger than their > pseudo-boolean counterparts). > > So, if you must solve hundreds of easy problems in a second, and if your > problem is described as a CNF and you have no control over that, picking > gini might be a good choice. If your problem is a little harder, or if you > have the possibility to describe it as a pseudo-boolean problem, gophersat > will probably be better. > > Since they are not efficient on the same kinds of problems, using both of > them concurrently might be interesting, too. Making them solve the same > problem and stop them when an answer was found. > > When solving pure CNF problems, the current version of gophersat suffers > from the fact that it can natively deal with cardinality constraints and > pseudo-boolean constraints: binary clauses take a lot of space in memory, > and a lot of time is spent in the solver figuring out whether we are > dealing with a clause or a more complex constraint. In the next future, we > will probably include the ability to compile an optimized version of the > solver for pure sat problems via build tags. Having generics in the > language would solve that issue too ;) > > Le jeudi 21 décembre 2017 16:44:24 UTC+1, Damian Gryski a écrit : >> >> How does it compare to https://github.com/IRIFrance/gini ? > > -- 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.
