We're sorry but this page doesn't work properly without JavaScript enabled. Please enable it to continue.
Feedback

Hard Satisfiable Formulas for Splittings by Linear Combinations

Formal Metadata

Title
Hard Satisfiable Formulas for Splittings by Linear Combinations
Title of Series
Number of Parts
28
Author
Contributors
License
CC Attribution - NonCommercial - NoDerivatives 4.0 International:
You are free to use, copy, distribute and transmit the work or content in unchanged form for any legal and non-commercial purpose as long as the work is attributed to the author in the manner specified by the author or licensor.
Identifiers
Publisher
Release Date
Language

Content Metadata

Subject Area
Genre
Abstract
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.