Skip to main content
Share Your Experience: Take the 2024 Developer Survey
24 votes
Accepted

Algebraic equivalent of SAT?

This is standard and widely used in computer science theory. There are many references that use boolean polynomials with False -> 0 and True -> 1, or in other words, a polynomial over GF(2) used ...
D.W.'s user avatar
  • 12.1k
15 votes
Accepted

Lower Bounds for Frege and Extended Frege

1, 2, 4) The best known lower bounds on extended Frege are the same as for Frege: linear number of lines, and quadratic size. This applies e.g. to the tautologies $\neg^{2n}\top$ (basically, any ...
Emil Jeřábek's user avatar
13 votes

Algebraic equivalent of SAT?

I think what you are asking about is also known as "polynomial calculus" in proof complexity and SAT solving. It was introduced in [1, 2] to investigate whether coNP can be separated from NP ...
Martin Berger's user avatar
8 votes

Do we currently know a polynomial-size Frege proof for Tseitin formulas?

Tseitin tautologies are unsatisfiable systems of linear equations over $\mathbb F_2$, and as such they can be refuted just by summing all the equations together (possibly after reconstructing the ...
Emil Jeřábek's user avatar
8 votes
Accepted

Do we currently know a polynomial-size Frege proof for Tseitin formulas?

Section 6 of the following paper has a sketch: Alasdair Urquhart. Hard examples for resolution. Journal of the ACM, 34(1):209–219, 1987. DOI: https://doi.org/10.1145/7531.8928
Emre Yolcu's user avatar
7 votes
Accepted

Document references describing weaknesses for cutting planes and algebraic proof system?

For each of these proof systems we know that there are some formulas where the shortest proof needs to have exponential length. Some of the earliest examples are an exponential lower bound for the ...
notautogenerated's user avatar
7 votes
Accepted

Resolution augmented with the rule of symmetry or the rule of extension

First, ER p-simulates SR: for example, ER is p-equivalent to the extended Frege proof system (EF) which is p-equivalent to the substitution Frege proof system (SF), and it is easy to see that SF p-...
Emil Jeřábek's user avatar
6 votes
Accepted

Is there any work relating type systems and Cook-Reckhow proof systems?

Cook-Reckhow propositional proof systems are nonunifrom. E.g. the computational complexity counterpart to the class of polynomial-size $\mathsf{Extended Frege}$ proofs is the nonuniform complexity ...
Kaveh's user avatar
  • 21.7k
6 votes
Accepted

Axioms of Minimum Size Resolution Refutations

With the caveat that I am posting this quickly in a sleep-deprived state, I think the answer is "no" to all three questions. Take the pigeonhole principle formulas PHP^m_n for m pigeons and n holes. ...
Jakob Nordstrom's user avatar
6 votes
Accepted

Can CDCL Algorithm Derived Conflict Clauses Always Be Obtained Through Resolution from an Unsatisfiable CNF Formula?

It is indeed and here is the reference for it if needed: Pipatsrisawat, K., & Darwiche, A. (2011). On the power of clause-learning SAT solvers as resolution engines. Artificial intelligence, 175(2)...
holf's user avatar
  • 2,174
5 votes

Can CDCL Algorithm Derived Conflict Clauses Always Be Obtained Through Resolution from an Unsatisfiable CNF Formula?

Yes, anything learned by conflict analysis in conflict-driven clause learning can be derived by resolution from the original formula. The technically slightly more precise claim is that any newly ...
Jakob Nordstrom's user avatar
5 votes
Accepted

Horn clause on cnf

Yes, any unsatisfiable Horn CNF has a tree-like resolution refutation with a linear number of clauses. Consider the standard poly-time Horn-SAT algorithm, which works as follows. First, set all ...
Emil Jeřábek's user avatar
4 votes
Accepted

A variation of propositional pigeonhole principle

Even the “further loosened” version has short Frege (in fact, $\mathrm{TC}^0$-Frege) refutations. Why is the principle unsatisfiable in the first place? Because if you map each pigeon to the hole with ...
Emil Jeřábek's user avatar
4 votes
Accepted

Is there a relation between the techniques used by Dan Willard, versus those of Brown and Palsberg, to exclude diagonalization?

I'll defer if someone more knowledgeable on the subject arrives, but I think the answer is that they are not the same. Willard's work is about building theories that avoid the typical formulation of ...
Dan Doel's user avatar
  • 1,021
3 votes

IPS upper bound for subset sum axiom

First, Kaveh is correct that the verification for IPS is randomized, so all it would show is $\mathsf{NP} \subseteq \mathsf{coAM}$ (not $\mathsf{NP} = \mathsf{coNP}$). However, this alone would still ...
Joshua Grochow's user avatar
3 votes

Construct proof systems for common algorithmic task, like equivalence of regular expressions

You have a non-deterministic algorithm deciding the problem. If you want to think of it as a proof system for $EQUIV$, then the proof of $(u,v) \in EQUIVE$ is just the string representing the ...
Kaveh's user avatar
  • 21.7k
3 votes
Accepted

Why isn't the proof obtained using Buss's proof of the derivational completeness of LK anchored?

The answer occurred to me right after I finished typing up the post. Rather than delete it, I figured I would post it anyway in case anyone else has the same question. Answer The mistake in the ...
Johnny's user avatar
  • 201
2 votes
Accepted

Power of non-implicationally-complete Frege systems and Boolean equational calculus

$\let\eq\leftrightarrow\def\ru{\mathrel/}\let\ET\bigwedge$Frege systems are required to be implicationally complete to make all such systems p-equivalent, yielding a robust definition of the Frege ...
Emil Jeřábek's user avatar
2 votes

Methods for Determining the minimal Width of Resolution Refutations for CNF Formulas

Partially answering question (2), the Prover-Delayer game of Atserias and Dalmau can be interpreted as a more general "dag-like query complexity" specialized to CNFs. See e.g. GGKS'18. And ...
notautogenerated's user avatar
2 votes
Accepted

In regards to the tautologies of a polynomially-bounded propositional proof system

Your question is like asking what is the class of formulas for the problem SAT? In the definition of SAT it is fixed to some fixed class, say those based on $\{\lnot, \land, \lor\}$ but it doesn't ...
Kaveh's user avatar
  • 21.7k
2 votes

IPS upper bound for subset sum axiom

I think what you are missing is probably the complexity of the proof verification algorithm for IPS. It is generally true that if we have a Cook-Reckhow proof system and have short proofs for a coNP-...
Kaveh's user avatar
  • 21.7k
2 votes

Construct proof systems for common algorithmic task, like equivalence of regular expressions

Kaveh's response exemplifies well the Cook-Reckhow notion of an abstract proof system. Nonetheless, for comparison, I point to a recent preprint of mine and Damien Pous: A cut-free cyclic proof ...
Anupam Das's user avatar
2 votes
Accepted

Proof of SPFA's worst-case complexity?

Here's the algorithm (from the wikipedia page) then a proof of the time bound: ...
Neal Young's user avatar
  • 10.8k
1 vote
Accepted

Is mathematical proof itself NP-hard?

Here is a link to some lecture notes that answer my question - http://www.cs.cornell.edu/~sabhar/publications/iaspcmi-proofcomplexity00.pdf Proof complexity is a vast field of mathematics.
Atsina's user avatar
  • 119
1 vote
Accepted

Eliminating tautological axioms in tree-like $k$-DNF resolution

Since I could not find a proof in the literature, I wrote a short note containing the proof.
Jan Johannsen's user avatar
1 vote

Resolution vs Nondeterministic Search Problems

If I understood correctly the question, the so-called Buss-Pudlak game provides a simple transformation from a proof system to such a decision tree (see Buss-Pudlak '94 http://math.cas.cz/%7Epudlak/...
Iddo Tzameret's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible