Questions tagged [resolution]
The resolution tag has no usage guidance.
18
questions
4
votes
1
answer
84
views
Methods for Determining the minimal Width of Resolution Refutations for CNF Formulas
Recall that the width of a resolution refutation $R$ of a CNF formula $F$ is the maximal number of literals in any clause occurring in $R$. I am intersting in finding the minimal width of some certain ...
- 315
7
votes
1
answer
402
views
What kind of resolution is CDCL corresponding to?
For an unsatisfiable CNF instance, CDCL will return a resolution refutation.
My question : what kind of resolution does it return? tree-like, regular or general?
- 315
3
votes
0
answers
60
views
How does extended resolution p-simulate extended Frege?
I found a slide stating that "extended resolution and extended Frege p-simulate each other", without providing a proof. It's obvious that extended Frege p-simulates extended resolution, but ...
- 145
0
votes
0
answers
97
views
When the tree-like resolution size is the same with general(regular) resolution size？
Background:
For an unsatisfiable SAT formulas, the length of a resolution refutaion means the number of clauses in it.
It's well known that there exist exponential separation between tree-like and ...
- 315
1
vote
0
answers
251
views
Is there a standard definition of resolution for arbitrary clauses?
Knuth defines in [1] a resolution operator for arbitrary clauses which sets $C = C' \diamond C'' = (C' \lor C'')$ when there is no literal $x$ such that $x \in C'$ and $\neg x \in C''$. I skimmed over ...
user30584
4
votes
1
answer
162
views
Eliminating tautological axioms in tree-like $k$-DNF resolution
The propositional proof system $k$-DNF-resolution, a.k.a. $Res(k)$, is a generalization of propositional resolution, where the lines in a proof are $k$-DNF formulas, i.e., disjunctions of $k$-terms of ...
- 4,631
6
votes
1
answer
114
views
Axioms of Minimum Size Resolution Refutations
Let $\phi$ be an unsatisfiable CNF formula and let $\Pi$ be a resolution refutation of $\phi$ of minimum size. Let $\psi$ be the subformula of $\phi$ containing the clauses that actually appear as ...
- 243
11
votes
1
answer
255
views
Direct Proof that the Pigeonhole Principle is Hard for Regular Resolution
It is well known that the pigeonhole principle $PHP_n^{n+1}$ is hard for general resolution. The original proof due to Haken is elegant. One first defines a complexity measure for derived clauses, in ...
- 111
6
votes
1
answer
222
views
Resolution vs Nondeterministic Search Problems
It is well known that each resolution refutation $\Pi$ for an unsatisfiable CNF formula $F = C_1\wedge C_2 \wedge ... \wedge C_m$ over variables $X$ can be translated in polynomial time (in the size ...
- 1,062
4
votes
1
answer
236
views
resolution based theorem prover for temporal logic
I am looking at implementing a a resolution-based theorem prover for propositional linear temporal logic (PLTL) (as opposed to a model checker). The ones out there (by Fisher et. al. and others) are ...
- 181
5
votes
1
answer
248
views
Mechanization of Mathematics
Its been a while since I took my theory course, but I recall that Hilberts Decision problem was shown to be false.
By the completeness theorem of first-order logic, a statement is universally valid ...
- 87
3
votes
0
answers
72
views
Substitution in Resolution Proofs
Let $F = C_1 \wedge C_2\; \wedge ... \wedge\; C_m$ be a unsatisfiable $k$-CNF on variables $x_1,...,x_n$, where $k$ is constant.
Let $x_j\rightarrow x_j^1\wedge x_j^2$ be a substitution that replaces ...
- 31
-4
votes
1
answer
565
views
"tree-like" vs "DAG-like" resolution
hi all there seems to be a deep/not-much-explored phenomenon in the way that SAT resolution proofs can define a tree and/or a DAG & its relationship to lower bounds/circuit complexity. could there ...
- 11k
2
votes
0
answers
194
views
Most general form of SAT which is in P
2-SAT is in P.
Additionally, a (CNF) SAT-problem is trivially poly-time solvable if no two expressions can be resolved (via Robinson resolution, ie for every pair of disjunctive clauses, they either ...
- 916
1
vote
1
answer
331
views
What is resolution ((in FOL))? [closed]
I'm searching for an authoritative definition of resolution (logic resolution).
Preferably on a reference freely available on the Internet (so I can read it right now).
If this is too broad then ...
- 604
1
vote
1
answer
127
views
Implied Clause and Resolvent
(I posted this question on MathSE first, no answer, that is the reason why I come here.)
Let $F$ be a 3-CNF formula on $n$ variables. A clause $c$ is implied by the formula if $F$ and $F \wedge c$ ...
- 1,109
4
votes
1
answer
356
views
About Closure under Resolution
The question looks very simple, that is why I posted it first on MathSE, unsuccesfully - no answer for 12 days. I tried to find a short and elegant answer to the question, but I haven't succeed yet. ...
- 1,109
17
votes
2
answers
4k
views
Is propositional resolution a complete proof system?
This question is about propositional logic and all occurrences of "resolution" should be read as "propositional resolution".
This question is something extremely basic but it has been bothering me ...
- 12.6k