3 ms·
I think the statistical methods would be better compared to a sat solver like Z3. Prolog gives you more flexibility, but it isn't going to be able to use the ad
by slaymaker1907 6y ago
I think the statistical methods would be better compared to a sat solver like Z3. Prolog gives you more flexibility, but it isn't going to be able to use the advanced search techniques that Z3 can take advantage of. Optimizers like Optaplanner are in sort of the same family as Z3, but they often trade being better at optimization for the ability to quickly find solutions, particularly if the number of solutions is small.
- ge0ffrey 6y agoIn my experience, seeing OptaPlanner pitted against the other best-of-the-best enterpise-grade solvers, OptaPlanner wins when scaling out - very clearly. Not when scaling down. This is the nature of the Local Search algorithms. The bigger the search space, the more we like it.
- rurban 6y agoMany prologs or derivates (like datalog or picat) use efficient sat solvers internally for quite some time already.