Proving unsatisfiability with hitting formulas
From MaRDI portal
Cites work
- scientific article; zbMATH DE number 1256733 (Why is no real title available?)
- scientific article; zbMATH DE number 1059248 (Why is no real title available?)
- scientific article; zbMATH DE number 1114015 (Why is no real title available?)
- scientific article; zbMATH DE number 3325539 (Why is no real title available?)
- scientific article; zbMATH DE number 2243370 (Why is no real title available?)
- A Computing Procedure for Quantification Theory
- A combinatorial characterization of resolution width
- A lower bound for polynomial calculus with extension rule
- A machine program for theorem-proving
- Algebraic proof systems over formulas.
- Automata, Languages and Programming
- Automating tree-like resolution in time \(n^{o(\log n)}\) is \textsf{ETH}-hard
- CNF-Satisfiability Test by Counting and Polynomial Average Time
- Circuit complexity, proof complexity, and polynomial identity testing. The ideal proof system
- Communication Complexity
- Constraint satisfaction problems in clausal form. II: Minimal unsatisfiability and conflict structure
- Dag-like communication and its applications
- Deterministic polynomial identity testing in non-commutative models
- Discretely ordered modules as a first-order extension of the cutting planes proof system
- Hard examples for resolution
- Homogenization and the polynomial calculus
- How limited interaction hinders real communication (and what it means for proof and circuit complexity)
- Irreducible subcube partitions
- Learning decision trees from random examples
- Lower Bounds on Hilbert's Nullstellensatz and Propositional Proofs
- Lower bounds for unambiguous automata via communication complexity
- Monotone circuit lower bounds from resolution
- Near optimal seperation of tree-like and general resolution
- Nearly optimal separations between communication (or query) complexity and partitions
- Notes on resolution over linear equations
- On Davis-Putnam reductions for minimally unsatisfiable clause-sets
- On the complexity of cutting-plane proofs
- On the power of clause-learning SAT solvers as resolution engines
- On the virtue of succinct proofs
- Proof complexity of natural formulas via communication arguments
- Proofs as Games
- Query-to-communication lifting for BPP
- Resolution over linear equations and multilinear proofs
- Resolution over linear equations modulo two
- Semialgebraic Proofs and Efficient Algorithm Design
- Separations in proof complexity and TFNP
- Separations in query complexity using cheat sheets
- Size-space tradeoffs for resolution
- Some subsystems of constant-depth Frege with parity
- Space Complexity in Propositional Calculus
- The intractability of resolution
- The power of negative reasoning
- The relative efficiency of propositional proof systems
- Theory and Applications of Satisfiability Testing
This page was built for publication: Proving unsatisfiability with hitting formulas
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6906384)
