Loading...
Please wait, while we are loading the content...
Similar Documents
Resolution with Counting: Dag-Like Lower Bounds and Different Moduli
| Content Provider | arXiv |
|---|---|
| Author | Part, Fedor Tzameret, Iddo |
| Date of Submission | 2019-11-18 |
| Abstract | Resolution over linear equations is a natural extension of the popular resolution refutation system, augmented with the ability to carry out basic counting. Denoted Res(lin_R), this refutation system operates with disjunctions of linear equations with boolean variables over a ring R, to refute unsatisfiable sets of such disjunctions. Beginning in the work of [RT08], through the work of [IS14] which focused on tree-like lower bounds, this refutation system was shown to be fairly strong. Subsequent work (cf.[Kra17, IS14, KO18, GK18]) made it evident that establishing lower bounds against general Res(lin_R) refutations is a challenging and interesting task since the system captures a 'minimal' extension of resolution with counting gates for which no super-polynomial lower bounds are known to date. We provide the first super-polynomial size lower bounds on general (dag-like) resolution over linear equations refutations in the large characteristic regime. In particular we prove that the subset-sum principle 1+x1+...+2^n xn=0 requires refutations of exponential size over Q. Our proof technique is nontrivial and novel: roughly speaking, we show that under certain conditions every refutation of a subset-sum instance f=0 must pass through a fat clause containing an equation f=alpha for each alpha in the image of f under boolean assignments. We develop a somewhat different approach to prove exponential lower bounds against tree-like refutations of any subset-sum instance that depends on n variables, hence also separating tree-like from dag-like refutations over the rationals. (Abstract continued in the full paper.) |
| Related Links | https://arxiv.org/pdf/1806.09383.pdf |
| Page Count | 40 |
| arXiv | 1806.09383 |
| Language | English |
| Access Restriction | Open |
| Subject Keyword | Computer Science - Computational Complexity Computer Science - Data Structures and Algorithms Computer Science - Logic in Computer Science Nonnumerical Algorithms and Problems Mathematical Logic Deduction and Theorem Proving Computer Science First-order arithmetic and fragments Complexity classes (hierarchies, relations among complexity classes, etc.) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) Complexity of proofs |
| Content Type | Text |
| Resource Type | Article |
| Subject | Computer Science |
