34 citations · 124 across the 13 of their papers we have counts for
16 papers
Search-Space Pruning with Int-Splits for Faster QBF Solving
Maximilian Heisinger, Irfansha Shaik, Martina Seidl +1
In many QBF encodings, sequences of Boolean variables stand for binary representations of integer variables. Examples are state labels in bounded model checking or actions in plann…
New ways to multiply 3 x 3-matrices
Marijn J. H. Heule, Manuel Kauers, Martina Seidl
It is known since the 1970s that no more than 23 multiplications are required for computing the product of two 3 x 3-matrices. It is not known whether this can also be done with fe…
Local Search for Fast Matrix Multiplication
Marijn J. H. Heule, Manuel Kauers, Martina Seidl
Laderman discovered a scheme for computing the product of two 3x3 matrices using only 23 multiplications in 1976. Since then, some more such schemes were proposed, but it remains o…
On the maximal minimal cube lengths in distinct DNF tautologies
Manuel Kauers, Martina Seidl, Doron Zeilberger
Inspired by a recent article by Anthony Zaleski and Doron Zeilberger, we investigate the question of determining the largest k for which there exists boolean formulas in disjunctiv…
Expansion-Based QBF Solving Without Recursion
Roderick Bloem, Nicolas Braud-Santoni, Vedad Hadzic +3
In recent years, expansion-based techniques have been shown to be very powerful in theory and practice for solving quantified Boolean formulas (QBF), the extension of propositional…
Short Proofs for Some Symmetric Quantified Boolean Formulas
Manuel Kauers, Martina Seidl
We exploit symmetries to give short proofs for two prominent formula families of QBF proof complexity. On the one hand, we employ symmetry breakers. On the other hand, we enrich th…