4 citations · 7 across the 3 of their papers we have counts for
7 papers · 1 filter
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…
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…
Symmetries of Quantified Boolean Formulas
Manuel Kauers, Martina Seidl
While symmetries are well understood for Boolean formulas and successfully exploited in practical SAT solving, less is known about symmetries in quantified Boolean formulas (QBF).…
Blocked Clauses in First-Order Logic
Benjamin Kiesl, Martin Suda, Martina Seidl +2
Blocked clauses provide the basis for powerful reasoning techniques used in SAT, QBF, and DQBF solving. Their definition, which relies on a simple syntactic criterion, guarantees t…
Q-Resolution with Generalized Axioms
Florian Lonsing, Uwe Egly, Martina Seidl
Q-resolution is a proof system for quantified Boolean formulas (QBFs) in prenex conjunctive normal form (PCNF) which underlies search-based QBF solvers with clause and cube learnin…