BIRS Workshop Lecture Videos

Banff International Research Station Logo

BIRS Workshop Lecture Videos

Hard Satisfiable Formulas for Splittings by Linear Combinations Knop, Alexander


Itsykson and Sokolov in 2014 introduced the class of DPLL(xor) algorithms that solve Boolean satisfiability problem using the splitting by linear combinations of variables modulo 2. This class extends the class of DPLL algorithms that split by variables. DPLL(xor) algorithms solve in polynomial time systems of linear equations modulo 2 that are hard for DPLL, PPSZ and CDCL algorithms. Itsykson and Sokolov have proved first exponential lower bounds for DPLL(xor) algorithms on unsatisfiable formulas. In the talk, we discuss several subclasses of DPLL(xor) algorithms and explain lower bounds for one of them.

Item Media

Item Citations and Data


Attribution-NonCommercial-NoDerivatives 4.0 International