DOI

We study the resolution complexity of Tseitin formulas over arbitrary rings in terms of combinatorial properties of graphs. We give some evidence that an expansion of a graph is a good characterization of the resolution complexity of Tseitin formulas. We extend the method of Ben-Sasson and Wigderson of proving lower bounds for the size of resolution proofs to constraint satisfaction problems under an arbitrary finite alphabet. For Tseitin formulas under the alphabet of cardinality d we provide a lower bound d e(G)-k for tree-like resolution complexity that is stronger than the one that can be obtained by the Ben-Sasson and Wigderson method. Here k is an upper bound on the degree of the graph and e(G) is the graph expansion that is equal to the minimal cut such that none of its parts is more than twice bigger than the other. We give a formal argument why a large graph expansion is necessary for lower bounds. Let G = âŒ

Язык оригиналаанглийский
Название основной публикацииComputer Science - Theory and Applications - 8th International Computer Science Symposium in Russia, CSR 2013
Страницы162-173
Число страниц12
DOI
СостояниеОпубликовано - 29 ноя 2013
Событие8th International Computer Science Symposium in Russia, CSR 2013 - Ekaterinburg, Российская Федерация
Продолжительность: 25 июн 201329 июн 2013

Серия публикаций

НазваниеLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Том7913 LNCS
ISSN (печатное издание)0302-9743
ISSN (электронное издание)1611-3349

конференция

конференция8th International Computer Science Symposium in Russia, CSR 2013
Страна/TерриторияРоссийская Федерация
ГородEkaterinburg
Период25/06/1329/06/13

    Предметные области Scopus

  • Теоретические компьютерные науки
  • Компьютерные науки (все)

ID: 49786016