22
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 ...
- 11.7k
12
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 ...
- 11.4k
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 ...
- 16.9k
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
- 286
5
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)...
- 2,164
3
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 ...
- 16.9k
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 ...
- 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 ...
- 16.9k
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 ...
- 216
Only top scored, non community-wiki answers of a minimum length are eligible