2019-04-09 23:42:14 (GMT)
About the choice of OCaml, I just wrote an experimental port of minisat in OCaml, trying to get as close as possible: minisat-ml :)
2019-04-10 0:7:50 (GMT)
So if you wanted to implement Zipperposition from scratch, would you use Rust instead of OCaml?
2019-04-10 0:37:21 (GMT)
I honestly don't know, rust is not as easy-going as OCaml. It'd definitely not be C or C++ though :)
2019-04-10 5:13:59 (GMT)
to elaborate on that: I think it'd be hard to achieve the same level of malleability and ease of modification with something that's not OCaml or Haskell. Rust would be a good candidate for a more performance-oriented prover, though.
2019-04-10 15:23:42 (GMT)
What features of OCaml do you think make it easier to modify the code? I saw that Rust also has pattern matching for example.
2019-04-10 15:23:53 (GMT)
(I've never used Rust by the way...)
2019-04-10 15:28:24 (GMT)
I grew to quite like OCaml while working on Zip, but do you think there are ways to write OCaml in a bit more efficient manner or do you think it is necessarily going to be slower (e.g. changing lists/sequences for arrays, design patterns such as Same execption etc.)?
2019-04-10 16:36:32 (GMT)
That's a good question. I started working on Zipperposition in 2012, when ocamlopt was not as optimizing and I was more keen on functional programming. These days, with projects like msat (and tools that use it, such as smbc or even Zipperposition), I'm programming in a way that is closer to imperative style, and using flambda and similar optimization tools.
Anyway, my point is: I think Zipperposition could be significantly faster both by algorithmic improvements, and engineering improvements (also, heuristics, but I leave that to y'all).
- algorithmic: I think there's some redundant work that is done in some parts (clauses simplified multiple times, for example). Also some term indices are not great (eg the feature vector index).
- engineering:
* term indices could use mutation (with, say, inline records for tree nodes)
* more generally, profiling (using perf+flamegraph as mentioned in the minisat-ml report) to find and improve hotspots.
2019-04-10 16:41:0 (GMT)
What features of OCaml do you think make it easier to modify the code?
compared to rust, OCaml has a GC, which means you don't have to care about allocations nor about aliasing at all. Many things are just immutable values, including expressions, etc. Things like Ctx or Env or even the terms can be shared easily; closures come naturally; and functors allow abstraction in a way that is hard to do in rust.
Of course rust allows for higher performance (and parallelism) but it's a lot more effort to use, I think. I tried a bit to write similar things and even hashconsing is super subtle to do properly (aliasing everywhere). If we wanted to compete with E or Vampire directly, rust would probably be the best choice, but OCaml is still much more concise and flexible imho :)
2019-04-10 16:53:20 (GMT)
@Petar Vukmirovic also, sequence/Iter should be well optimized by the compiler, I don't think this part is costly at all (and it allows computations of unifiers, etc. to be lazy which can only help).
2019-04-11 6:16:53 (GMT)
Was there any reason to not use the OCaml option -unsafe? Or did you use unsafe_get everywhere?
(I am trying to compile the minisat-ml...)
2019-04-11 6:25:28 (GMT)
(I did not have dune installed leading to the following error message: "From the command line:
Error: Alias "all" is empty.
It is not defined in . or any of its descendants.
make: *** [build] Error 1"
)
2019-04-11 7:25:51 (GMT)
I am not a specialist of Minisat 2.2, but in the litredundant function, I think you are missing Minisat's seen_failed (your seen = true corresponds to seen_removable). At least, later Minisat version have it (https://github.com/msoos/minisat/blob/master/minisat/core/Solver.cc#L388).
2019-04-11 7:32:51 (GMT)
The idea of seen_failed is to remember when a literal is not redundant, because redundant/not redundant does not change during the minimisation with a literal. Adding the flag does not change the behaviour. It only makes the minimisation more efficient.
2019-04-11 8:55:44 (GMT)
You use 63-bit integers, thus sparing one bit for each integer! Awesome ^^
(Sorry for the silly joke. The typo is in the "Memory layout" paragraph of your technical report. I have done too much proof-reading and reviews these last few weeks so I think I turned into a typo-detector...).
2019-04-11 9:0:31 (GMT)
@Sophie not a typo. The one bit is used for the garbage collection (or I did not understand the sentence)
2019-04-11 10:9:2 (GMT)
I talked to @Sophie offline and she was confused by the sentences "since all data in OCaml is stored as 64-bit words on x86_64" and "32-bit integers are replaced by 63-bit integers (on x86_64)"
2019-04-11 11:38:4 (GMT)
I run minisat-ml with the default options on a larger set of instances (3313 preprocessed problems from the SAT comp 2009 to 2017), with 30min timeout and 10GB RAM on the MPI cluster. For comparison:
| solver | solved | average time (s) |
|---|---|---|
| Microsat | 1018 | 310 |
| minisat-ml | 1133 | 348 |
| MiniSAT | 1388 | 326 |
| Glucose | 1703 | 320 |
2019-04-11 11:43:27 (GMT)
@Simon Cruanes Impressive results
2019-04-12 7:7:1 (GMT)
(I did not have dune installed leading to the following error message: "From the command line:
Error: Alias "all" is empty.
It is not defined in . or any of its descendants.
make: *** [build] Error 1"
)
might be an old version of dune that you use ("old" being relative).
2019-04-12 7:10:10 (GMT)
Indeed not a typo, but I understand how it can be confusing that a 63-bits integer is stored in a 64-bits word.
2019-04-12 7:13:20 (GMT)
@Simon Cruanes @Mathias Fleury Thanks for the clarification! :)
2019-04-12 7:21:51 (GMT)
@Mathias Fleury thanks a lot for the results. It's indeed not too bad. Is microsat the solver extracted from your Isabelle developments?
Related to the minimization: my own version of minisat 2.2.0 (as downloaded from minisat.se) doesn't have the seen_failed at all. It would be an improvement, I suppose, but the solver is still faithful to minisat.
2019-04-12 9:3:42 (GMT)
Mathias Fleury thanks a lot for the results. It's indeed not too bad. Is microsat the solver extracted from your Isabelle developments?
sadly not. It is the SAT solver from Marijn Heule (https://github.com/marijnheule/microsat). My solver is far from that.
2019-04-12 9:8:58 (GMT)
Oh neat!! Thanks :)
2019-04-12 9:12:28 (GMT)
Related to the minimization: my own version of minisat 2.2.0 (as downloaded from minisat.se) doesn't have the
seen_failedat all. It would be an improvement, I suppose, but the solver is still faithful to minisat.
Damn, The story of minisat is too complicated. I always thought that https://github.com/niklasso/minisat/ is the latest version, but apparently, it is not.
2019-04-12 9:13:5 (GMT)
I specifically picked 2.2.0, I think, don't worry :)
2019-04-12 9:13:31 (GMT)
Your solver extracts to SML? or C? I forgot
2019-04-12 9:14:44 (GMT)
SML.
2019-04-12 9:16:22 (GMT)
Extraction to LLVM is on my TODO list. Peter Lammich has developed a tool to do so and the generated code is more efficient (at least on his tests).
2019-04-12 13:26:40 (GMT)
That'd be interesting, if you can get closer to microsat. Anyway, thanks for the benchmarks again! :)
2019-04-12 13:31:49 (GMT)
Can I report your results in the tech report? Crediting you, of course?
2019-04-12 16:1:29 (GMT)
sure. I can also give you the raw results if you want to print cactus plots.
2019-04-12 16:6:27 (GMT)
I'd like that, especially if it's csv files :)
2019-04-16 22:11:41 (GMT)
2019-04-16 22:12:59 (GMT)
I'm super impressed that almost all the solvers, including isasat, beat zchaff (!!)
2019-04-17 6:20:59 (GMT)
Damn that was the wrong version of CaDiCaL
2019-04-17 6:29:38 (GMT)
(that was the version without DB reduction; I'll send you the corrected version later)
2019-04-17 14:39:57 (GMT)
Ah yeah, DB reduction can make a huge difference. It certainly did for msat.
2019-04-18 21:11:43 (GMT)
You should say what is the hardware of the MPI cluster