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

Questions tagged [resolution]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
6 votes
0 answers
122 views

Proof complexity of Sudoku

Let $P$ be a $N$x$N$ Sudoku puzzle (assume $N=n^2$ for some $n\in \mathbb{N}$, e.g. standard $9$x$9$ puzzle is $n=3$). We can represent it in propositional logic as follows: Variables $p_{i,j,k}$: ...
Kaveh's user avatar
  • 21.7k
3 votes
1 answer
209 views

Horn clause on cnf

Recall that a CNF formula is Horn if each clause contains at most one positive literal. Is it possible any unsatisfiable Horn CNF formula has a polynomial-size treelike Resolution refutation? Is there ...
David's user avatar
  • 133
1 vote
0 answers
48 views

Short learned clauses for XSAT

Are there any studies about how effective a limited resolution pre-processor is for DPLL-CDCL type SAT solvers? By limited resolution pre-processor I mean a pre-processor that generates short (1,2, or ...
Russell Easterly's user avatar
4 votes
0 answers
57 views

Complexity of circuit evaluation in Resolution

Consider the standard evaluation function for CNF formulas $\mathsf{Eval}(\varphi,x)$ taking as input a CNF $\varphi$ and an assignment $x$ to the variables and outputting the value of $\varphi(x)$. ...
Noel Arteche's user avatar
1 vote
0 answers
42 views

Max number of m-clauses NOT subsumed by k-clauses

This question is releated to: Max number of k-clauses such that no two clauses can be resolved? and How often can a clause cause a conflict Assume there are $N$ variables and a maximum size set of $k$-...
Russell Easterly's user avatar
1 vote
1 answer
83 views

Max number of k-clauses such that no two clauses can be resolved?

Let $n$ be the number of variables and $k$ the size of the clauses. What is the maximum number of k-clauses such that no two clauses can be resolved to a smaller (less than $k$) clause. I will accept ...
Russell Easterly's user avatar
4 votes
1 answer
92 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 ...
Jxb's user avatar
  • 316
7 votes
1 answer
430 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?
Jxb's user avatar
  • 316
3 votes
0 answers
75 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 ...
Soha's user avatar
  • 187
0 votes
0 answers
123 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 ...
Jxb's user avatar
  • 316
1 vote
0 answers
254 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 ...
user avatar
4 votes
1 answer
168 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 ...
Jan Johannsen's user avatar
6 votes
1 answer
126 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 ...
Nathan's user avatar
  • 253
11 votes
1 answer
271 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 ...
corregular's user avatar
6 votes
1 answer
228 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 ...
verifying's user avatar
  • 1,072
4 votes
1 answer
240 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 ...
Motorhead's user avatar
  • 181
5 votes
1 answer
249 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 ...
abrahimladha's user avatar
3 votes
0 answers
73 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 ...
tori's user avatar
  • 31
-4 votes
1 answer
583 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 ...
vzn's user avatar
  • 11k
2 votes
0 answers
197 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 ...
dspyz's user avatar
  • 916
1 vote
1 answer
339 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 ...
Trylks's user avatar
  • 604
1 vote
1 answer
131 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$ ...
Xavier Labouze's user avatar
4 votes
1 answer
370 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. ...
Xavier Labouze's user avatar
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 ...
Vijay D's user avatar
  • 12.6k