Share Your Experience: Take the 2024 Developer Survey

# Questions tagged [resolution]

The tag has no usage guidance.

24 questions
Filter by
Sorted by
Tagged with
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}$: ...
• 21.7k
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 ...
• 133
1 vote
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 ...
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)$. ...
• 988
1 vote
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$-...
1 vote
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 ...
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 ...
• 316
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?
• 316
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 ...
• 187
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 ...
• 316
1 vote
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 ...
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 ...
• 4,630
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 ...
• 253
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 ...
• 111
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 ...
• 1,072
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 ...
• 181
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 ...
• 147
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 ...
• 31
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 ...
• 11k
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 ...
• 916
1 vote
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 ...
• 604
1 vote
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$ ...
• 1,117
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. ...
• 1,117