Unified Characterisations of Resolution Hardness Measures

No abstract is available for this paper.

• Publication year

  2014

• Venue

  International Conference on Theory and Applications of Satisfiability Testing

• Publication date

  2014-07-14

• Fields of study

  Mathematics, Computer Science

• Identifiers
  DOI 10.1007/978-3-319-09284-3_13
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Minimal Unsatisfiability and Autarkies

  2021cited by this paper
• SOFSEM 2014: Theory and Practice of Computer Science

  2014cited by this paper
• A Brief History of Strahler Numbers

  2014cited by this paper
• Generalizing determinization from automata to coalgebras

  2013cited by this paper
• Trading inference effort versus size in CNF Knowledge Compilation

  2013influential reference
• Some trade-off results for polynomial calculus: extended abstract

  2013cited by this paper
• On SAT Representations of XOR Constraints

  2013cited by this paper
• Pebble Games, Proof Complexity, and Time-Space Trade-offs

  2013cited by this paper
• Hardness measures and resolution lower bounds

  2013cited by this paper
• Complexity issues related to propagation completeness

  2013cited by this paper
• Just a Pebble Game

  2013cited by this paper
• Automated reasoning

  2013cited by this paper
• A characterization of tree-like Resolution size

  2013cited by this paper
• Generalising and Unifying SLUR and Unit-Refutation Completeness

  2013cited by this paper
• Improving Watermark Resistance against Removal Attacks Using Orthogonal Wavelet Adaptation

  2012cited by this paper
• Inprocessing Rules

  2012cited by this paper
• Generalising Unit-Refutation Completeness and SLUR via Nested Input Resolution

  2012influential reference
• On hierarchies over the SLUR class

  2012cited by this paper
• Time-space tradeoffs in resolution: superpolynomial lower bounds for superlinear space

  2012cited by this paper
• Relating Proof Complexity Measures and Practical Hardness of SAT

  2012cited by this paper
• Properties of SLUR Formulae

  2012cited by this paper
• Parameterized Complexity of DPLL Search Procedures

  2011cited by this paper
• The Depth of Resolution Proofs

  2011cited by this paper
• Constraint Satisfaction Problems in Clausal Form I: Autarkies and Deficiency

  2011cited by this paper
• Simulating Circuit-Level Simplifications on CNF

  2011cited by this paper
• On the Maximal Number of Cubic Runs in a String

  2010cited by this paper
• A Lower Bound for the Pigeonhole Principle in Tree-like Resolution by Asymmetric Prover-Delayer Games

  2010cited by this paper
• Electronic Colloquium on Computational Complexity, Report No. 125 (2010) Understanding Space in Proof Complexity: Separations and Trade-offs via Substitutions

  2010cited by this paper
• Lower bounds for bounded depth Frege proofs via Pudlák-Buss games

  2010cited by this paper
• Handbook of satisfiability

  2009cited by this paper
• Frontiers in Artificial Intelligence and Applications

  2009cited by this paper
• Measuring the Hardness of SAT Instances

  2008cited by this paper
• Short Proofs May Be Spacious: An Optimal Separation of Space and Length in Resolution

  2008cited by this paper
• Towards an optimal separation of space and length in resolution

  2008cited by this paper
• Interpolation Theorems, Lower Bounds for Proof Systems, and Independence Results for Bounded Arithmetic

  2007cited by this paper
• Exponential Lower Bounds for the Running Time of DPLL Algorithms on Satisfiable Formulas

  2004cited by this paper
• Space and Width in Propositional Resolution (Column: Computational Complexity)

  2004cited by this paper
• Upper and Lower Bounds on the Complexity of Generalised Resolution and Generalised Constraint Satisfaction Problems

  2004influential reference
• A sharp threshold in proof complexity yields lower bounds for satisfiability search

  2004cited by this paper
• A combinatorial characterization of resolution width

  2003cited by this paper
• Lower Bounds for Bounded-Depth Frege Proofs via Buss-Pudlack Games

  2003cited by this paper
• A combinatorial characterization of treelike resolution space

  2003cited by this paper
• Short proofs are narrow—resolution made simple

  2001influential reference
• Space complexity in propositional calculus

  2000influential reference
• A lower bound for DLL algorithms for k-SAT (preliminary version)

  2000cited by this paper
• Proofs as Games

  2000cited by this paper
• The Propositional Formula Checker HeerHugo

  2000cited by this paper
• An improved version of width restricted resolution

  2000cited by this paper
• New Methods for 3-SAT Decision and Worst-case Analysis

  1999cited by this paper
• On a Generalization of Extended Resolution

  1999cited by this paper
• Space Bounds for Resolution

  1999cited by this paper
• Lower Bounds for Space in Resolution

  1999cited by this paper
• Investigating a general hierarchy of polynomially decidable classes of CNF's based on short tree-like resolution proofs

  1999cited by this paper
• Propositional Logic: Deduction and Algorithms

  1999cited by this paper
• Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic

  1997cited by this paper
• On resolution with short clauses

  1996cited by this paper
• Using the Groebner basis algorithm to find proofs of unsatisfiability

  1996cited by this paper
• On Finding Solutions for Extended Horn Formulas

  1995cited by this paper
• Tractable Databases: How to Make Propositional Unit Resolution Complete Through Compilation

  1994cited by this paper
• Aussagenlogik - Deduktion und Algorithmen

  1994cited by this paper
• Computer Science Logic

  1993cited by this paper
• On generalized Horn formulas and k-resolution

  1993cited by this paper
• Trees Everywhere

  1990cited by this paper
• The Intractability of Resolution

  1985cited by this paper
• On the Complexity of Derivation in Propositional Calculus

  1983cited by this paper

• Space characterizations of complexity measures and size-space trade-offs in propositional proof systems

  2023cites this paper
• Analysis of Pure Literal Elimination Rule for Non-uniform Random (MAX) k-SAT Problem with an Arbitrary Degree Distribution

  2022cites this paper
• Frege Systems for Quantified Boolean Logic

  2020cites this paper
• Hardness Characterisations and Size-Width Lower Bounds for QBF Resolution

  2020cites this paper
• Phase Transition in Realistic Random SAT Models

  2019cites this paper
• Proof complexity

  2019influential citation
• Scale-Free Random SAT Instances

  2017cites this paper
• Structure features for SAT instances classification

  2017cites this paper
• Total Space in Resolution Is at Least Width Squared

  2016cites this paper
• Are Short Proofs Narrow? QBF Resolution Is Not So Simple

  2016cites this paper
• Lower Bounds: From Circuits to QBF Proof Systems

  2016cites this paper
• Feasible Interpolation for QBF Resolution Calculi

  2015cites this paper
• A Game Characterisation of Tree-like Q-resolution Size

  2015cites this paper
• Theoretical Foundations of Applied SAT Solving ( 14 w 5101 ) January 19-24 , 2014

  2015cites this paper
• A framework for good SAT translations, with applications to CNF representations of XOR constraints

  2014influential citation
• Total Space in Resolution

  2014cites this paper
• On SAT representations of XOR constraints (towards a theory of good SAT representations)

  2014cites this paper
• Towards a theory of good SAT representations

  2013influential citation
• Frege Systems for Quantified Boolean Logic

  year unknowncites this paper