Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > KEYWORD > RESOLUTION OVER LINEAR EQUATIONS:
Reports tagged with Resolution over linear equations:
TR17-117 | 20th July 2017
Dmitry Itsykson, Alexander Knop

Hard satisfiable formulas for splittings by linear combinations

Itsykson and Sokolov in 2014 introduced the class of DPLL($\oplus$) 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($\oplus$) algorithms solve in polynomial time systems of linear equations modulo two ... more >>>


TR18-117 | 23rd June 2018
Fedor Part, Iddo Tzameret

Resolution with Counting: Lower Bounds over Different Moduli

Revisions: 1

Resolution over linear equations (introduced in [RT08]) emerged recently as an important object of study. This refutation system, denoted Res(lin$_R$), operates with disjunction of linear equations over a ring $R$. On the one hand, the system captures a natural ``minimal'' extension of resolution in which efficient counting can be achieved; ... more >>>


TR20-034 | 12th March 2020
Erfan Khaniki

On Proof complexity of Resolution over Polynomial Calculus

Revisions: 1

The refutation system ${Res}_R({PC}_d)$ is a natural extension of resolution refutation system such that it operates with disjunctions of degree $d$ polynomials over ring $R$ with boolean variables. For $d=1$, this system is called ${Res}_R({lin})$. Based on properties of $R$, ${Res}_R({lin})$ systems can be too strong to prove lower ... more >>>




ISSN 1433-8092 | Imprint