Meeting 28.11.2016

Alex: Boolean equivalence handling (↔) was removed from Leo-III. Instead now the equivalences are translated to equalities. This makes implementing their handling much easier. Next he will work on clause selection and afterwards on including the relevance filter developed by Max.

Max: Has reworked mini-scoping and pre-processing in general. NNF calculation was completely removed. Now the CNF is calculated directly. This avoids many repeated iterations over the matrix. He plans now to extend the pre-processing with clever instantiation for ∀-quantified variables.

Hans-Jörg: Finished setting up the benchmarking suite, first weekly benchmarks were successful. 14h run time. Leo-III proved none of the 360 counter satisfiable problems. For the 743 problems of the last CASC the result distribution was the following:

• Unknown: 35
• ScriptTimeout: 48
• Timeout: 205
• Theorem: 112
• Error: 343 This result is not surprising, given that Leo-III is not yet supposed to be production ready.

On the pre-processing side of thing, he is currently working on integrating transitivity constraints into the SAT based unit clause search.