The limits of tractability in resolution-based propositional proof systems

Article

Dantchev, S. and Martin, B. 2011. The limits of tractability in resolution-based propositional proof systems. Annals of Pure and Applied Logic. 163 (6), pp. 656-668. https://doi.org/10.1016/j.apal.2011.11.001
TypeArticle
TitleThe limits of tractability in resolution-based propositional proof systems
AuthorsDantchev, S. and Martin, B.
Abstract

We study classes of propositional contradictions based on the Least Number Principle (LNP) in the refutation system of Resolution and its generalisations with bounded conjunction, Res(k).

Keywordspropositional proof complexity; resolution with bounded conjunction; lower bounds
Research GroupFoundations of Computing group
PublisherElsevier
JournalAnnals of Pure and Applied Logic
ISSN0168-0072
Publication dates
Online03 Dec 2011
Publication process dates
Deposited20 Dec 2012
Output statusPublished
Additional information

Computability in Europe 2010

Digital Object Identifier (DOI)https://doi.org/10.1016/j.apal.2011.11.001
LanguageEnglish
Permalink -

https://repository.mdx.ac.uk/item/83wz0

Log in to edit
  • 121
    total views
  • 0
    total downloads
  • 1
    views this month
  • 0
    downloads this month

Export as

Related outputs

The packing chromatic number of the infinite square lattice is between 13 and 15
Martin, B., Raimondi, F., Chen, T. and Martin, J. 2017. The packing chromatic number of the infinite square lattice is between 13 and 15. Discrete Applied Mathematics. 225, pp. 136-142. https://doi.org/10.1016/j.dam.2017.03.013
Constraint satisfaction problems for reducts of homogeneous graphs
Bodirsky, M., Martin, B., Pinsker, M. and Pongrácz, A. 2016. Constraint satisfaction problems for reducts of homogeneous graphs. 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Rome, Italy 12 - 15 Jul 2016 Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH. pp. 119:1-119:14 https://doi.org/10.4230/LIPIcs.ICALP.2016.119
Distance constraint satisfaction problems
Bodirskya, M., Dalmau, V., Martin, B., Mottet, A. and Pinsker, M. 2016. Distance constraint satisfaction problems. Information and Computation. 247, pp. 87-105. https://doi.org/10.1016/j.ic.2015.11.010
From complexity to algebra and back: digraph classes, collapsibility and the PGP
Carvalho, C., Madelaine, F. and Martin, B. 2015. From complexity to algebra and back: digraph classes, collapsibility and the PGP. 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). Kyoto, Japan 06 - 10 Jul 2015 Institute of Electrical and Electronics Engineers (IEEE). pp. 462-474
Constraint satisfaction with counting quantifiers 2
Martin, B. and Stacho, J. 2014. Constraint satisfaction with counting quantifiers 2. 9th International Computer Science Symposium in Russia, CSR 2014. Moscow, Russia 07 - 11 Jun 2014 Springer. pp. 259-272
QCSP on semicomplete digraphs
Dapić, P., Marković, P. and Martin, B. 2014. QCSP on semicomplete digraphs. 41st International Colloquium on Automata, Languages and Programming, ICALP 2014. Copenhagen, Denmark 08 - 11 Jul 2014 Springer. pp. 847-858
Constraint satisfaction problems over the integers with successor
Bodirsky, M., Martin, B. and Mottet, A. 2015. Constraint satisfaction problems over the integers with successor. 42nd ICALP 2015. Kyoto, Japan 06 - 10 Jul 2015 Heidelberg, Germany Springer Berlin. Heidelberg. pp. 256-267 https://doi.org/10.1007/978-3-662-47672-7_21
Hierarchies in fragments of monadic strict NP
Martin, B. and Madelaine, F. 2007. Hierarchies in fragments of monadic strict NP. in: Cooper, B., Löwe, B. and Sorbi, A. (ed.) Computation and logic in the real world: Third Conference on Computability in Europe, CiE 2007, Siena, Italy, June 18-23, 2007, Proceedings Springer Berlin. Heidelberg.
The lattice structure of sets of surjective hyper-operations
Martin, B. 2010. The lattice structure of sets of surjective hyper-operations. The 16th International Conference on Principles and Practice of Constraint Programming (CP 2010). St Andrews, Scotland 06 - 10 Sep 2010 Springer Verlag. https://doi.org/10.1007/978-3-642-15396-9_31
Distance constraint satisfaction problems
Bodirsky, M., Dalmau, V., Martin, B. and Pinsker, M. 2010. Distance constraint satisfaction problems. 35th International Symposium on Mathematical Foundations of Computer Science (MFCS 2010). Brno, Czech Republic 23 - 27 Aug 2010 Springer. pp. 162-173 https://doi.org/10.1007/978-3-642-15155-2_16
The complexity of positive first-order logic without equality II: the four-element case
Martin, B. and Martin, J. 2010. The complexity of positive first-order logic without equality II: the four-element case. 24th International Workshop (CSL 2010), 19th Annual Conference of the EACSL. Brno, Czech Republic 23 - 27 Aug 2010 Springer. pp. 426-438 https://doi.org/10.1007/978-3-642-15205-4_33
The limits of tractability in resolution-based propositional proof systems
Dantchev, S. and Martin, B. 2010. The limits of tractability in resolution-based propositional proof systems. 6th International Conference on Computability in Europe: Programs, Proofs, Processes (CIE 2010). Portugal 30 Jun - 04 Jul 2010
A tetrachotomy for positive first-order logic without equality
Madelaine, F. and Martin, B. 2011. A tetrachotomy for positive first-order logic without equality. 26th Annual IEEE Symposium on Logic in Computer Science (LICS 2011). Ontario, Canada 21 - 24 Jun 2011 IEEE. pp. 311-320 https://doi.org/10.1109/LICS.2011.27
QCSP on partially reflexive forests
Martin, B. 2011. QCSP on partially reflexive forests. The 17th International Conference on Principles and Practice of Constraint Programming (CP 2011). Perugia, Italy 12 - 16 Sep 2011 Springer. pp. 546-560 https://doi.org/10.1007/978-3-642-23786-7_42
The computational complexity of disconnected cut and 2K2-partition
Martin, B. and Paulusma, D. 2011. The computational complexity of disconnected cut and 2K2-partition. The 17th International Conference on Principles and Practice of Constraint Programming (CP 2011). Perugia, Italy 12 - 16 Sep 2011 Springer. pp. 561-575 https://doi.org/10.1007/978-3-642-23786-7_43
Quantified constraints and containment problems
Chen, H., Madelaine, F. and Martin, B. 2008. Quantified constraints and containment problems. 23rd Annual IEEE Symposium on Logic in Computer Science (LICS 2008). Pittsburgh, PA, USA 24 - 27 Jun 2008 IEEE. pp. 317-328 https://doi.org/10.1109/LICS.2008.15
First-order model checking problems parameterized by the model
Martin, B. 2008. First-order model checking problems parameterized by the model. The 4th Conference on Computability in Europe: Logic and Theory of Algorithms (CiE 2008). University of Athens, Greece 15 - 20 Jun 2008 Springer. pp. 417-427 https://doi.org/10.1007/978-3-540-69407-6_45
Rank complexity gap for Lovász-Schrijver and Sherali-Adams proof systems
Dantchev, S. and Martin, B. 2013. Rank complexity gap for Lovász-Schrijver and Sherali-Adams proof systems. Computational Complexity. 22 (1), pp. 191-213. https://doi.org/10.1007/s00037-012-0049-1
Constraint satisfaction with counting quantifiers
Madelaine, F., Martin, B. and Stacho, J. 2012. Constraint satisfaction with counting quantifiers. The 7th International Computer Science Symposium (CSR 2012). Nizhny Novgorod, Russia 03 - 07 Jul 2012 Springer. pp. 253-265 https://doi.org/10.1007/978-3-642-30642-6_24
Finding vertex-surjective graph homomorphisms
Golovach, P., Lidický, B., Martin, B. and Paulusma, D. 2012. Finding vertex-surjective graph homomorphisms. 7th International Computer Science Symposium (CSR 2012). Nizhny Novgorod, Russia 03 - 07 Jul 2012 Springer. pp. 160-171 https://doi.org/10.1007/978-3-642-30642-6_16
Low-level dichotomy for quantified constraint satisfaction problems
Martin, B. 2011. Low-level dichotomy for quantified constraint satisfaction problems. Information Processing Letters. 111 (20), pp. 999-1003. https://doi.org/10.1016/j.ipl.2011.07.010
Cutting planes and the parameter cutwidth
Dantchev, S. and Martin, B. 2011. Cutting planes and the parameter cutwidth. Theory of Computing Systems. 51 (1), pp. 50-64. https://doi.org/10.1007/s00224-011-9373-0
The complexity of surjective homomorphism problems - a survey
Bodirsky, M., Kara, J. and Martin, B. 2012. The complexity of surjective homomorphism problems - a survey. Discrete Applied Mathematics. 160 (12), pp. 1680-1690.
The complexity of positive first-order logic without equality
Madelaine, F. and Martin, B. 2012. The complexity of positive first-order logic without equality. ACM Transactions on Computational Logic. 13 (1), pp. 1-17. https://doi.org/10.1145/2071368.2071373
Parameterized proof complexity
Dantchev, S., Martin, B. and Szeider, S. 2011. Parameterized proof complexity. Computational Complexity. 20 (1), pp. 51-85. https://doi.org/10.1007/s00037-010-0001-1
On the scope of the universal-algebraic approach to constraint satisfaction
Bodirsky, M., Hils, M. and Martin, B. 2010. On the scope of the universal-algebraic approach to constraint satisfaction. 25th Annual IEEE Symposium on Logic in Computer Science (LICS). Edinburgh, United Kingdom 11 - 14 Jul 2010 IEEE. pp. 90-99 https://doi.org/10.1109/LICS.2010.13
Tight rank lower bounds for the Sherali–Adams proof system
Dantchev, S., Martin, B. and Rhodes, M. 2009. Tight rank lower bounds for the Sherali–Adams proof system. Theoretical Computer Science. 410 (21-23), pp. 2054-2063. https://doi.org/10.1016/j.tcs.2009.01.002