Name
Abstract | ||
|---|---|---|
We consider an extension of the resolution proof system that operates with disjunctions of linear equalities over F2; we denote this system by Res(⊕). It is well known that tree-like resolution is equivalent in behavior to DPLL algorithms for the Boolean satisfiability problem. Every DPLL algorithm splits the input problem into two by assigning two possible values to a variable; then it simplifies the two resulting formulas and makes two recursive calls. Tree-like Res(⊕)-proofs correspond to an extension of the DPLL paradigm, in which we can split by an arbitrary linear combination of variables modulo two. These algorithms quickly solve formulas that explicitly encode linear systems modulo two which were used for proving exponential lower bounds for conventional DPLL algorithms. |
Year | DOI | Venue |
|---|---|---|
2020 | 10.1016/j.apal.2019.102722 | Annals of Pure and Applied Logic |
Keywords | Field | DocType |
03F20,03F03,03D15,68Q17 | Integer,Linear equation,Linear combination,Discrete mathematics,Combinatorics,Exponential function,Linear system,Modulo,Boolean satisfiability problem,Binary entropy function,Mathematics | Journal |
Volume | Issue | ISSN |
171 | 1 | 0168-0072 |
Citations | PageRank | References |
0 | 0.34 | 0 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Dmitry Itsykson | 1 | 33 | 10.09 |
| Dmitry Sokolov | 2 | 12 | 4.76 |