  Under the auspices of the Computational Complexity Foundation (CCF)     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