Could a modification of <PERSON>'s proof system be used to solve 3-SAT in polynomial time?
A literal is a nonzero integer, and we define $\sim x = -x$.
A clause is a nonempty set of literals.
A CNF is a set of clauses.
A K-rule is a pair $(F,C)$ where $F$ is a CNF and $C$ is a clause.
A <PERSON>-style proof system (KPS) is a set of K-rules.
If $S$ is a KPS, then an $S$-proof of $C$ from $F$, or an $(S,F)$-proof of $C$, is a sequence $\langle C_1,..,C_n\rangle$ of clauses such that $C = C_n$ and for all $1\le i\le n$, either $C_i \in F$ or there is a K-rule $R = (G,A) \in S$ and a function $f : {x,\sim x : x \in B \in G \lor x \in A} \rightarrow \mathbb{Z}_{\ne 0}$ which respects negation such that letting $g(B) := {f(a) : a ∈ B}$, we have $C_i = g(A)$, and for all $B \in G$, there exists some $j < i$ with $C_j = g(B)$.
For fixed $S$, the language ${(F,C) : F \vdash_S C}$ is polynomial-time decidable:
read inputs F and C
if C ∈ F
return true
let D = {x1,~x1,..,xn,~xn} be the set of literals occuring in F or C, and their negations
Contin := true
while Contin
Contin ← false
for (G,A) in S
for h : {abs(x) : x ∈ B ∈ G ∨ x ∈ A} -> D # there are |D|^c such functions
f(x) := (x > 0 ? h(x) : -h(-x))
g(B) := {f(a) : a ∈ B}
for B in G
if g(B) ∉ G
continue in the for-loop where h is chosen
if g(A) ∉ F
push g(A) to F
Contin ← true
if C ∈ F
return true
else
return false
$S$ is sound if for all CNF's $F$ and clauses $C$, the existence of an $(S,F)$-proof of $C$ implies that $F \vDash C$.
$S$ is complete for a class $\Gamma$ of CNF's if for all $F \in \Gamma$ and $C$, if $F \vDash C$ then $C$ is $(S,F)$-provable.
No KPS is complete for full $SAT$, since any clause of the form ${-1,1,2,3,..,n}$ is tautological, but for any system $S$, $sup{|A| : (\emptyset,A) \in S}$ is only finite, making the clause $(S,\emptyset)$-unprovable for sufficiently large $n$.
${({{1},{-1}},{2})}$ is complete for $1$-$SAT$, and represents the rule $a,\sim a \vdash b$.
${(\emptyset,{1,-1}),({{1}},{1,2}),({{1,2},{-1,3}},{2,3})}$ is complete for $2$-$SAT$, and represents the system consisting of the rules (1) $\vdash a\lor\sim a$, (2) $a\lor a \vdash a\lor b$, and (3) $a\lor b, \sim a\lor c \vdash b\lor c$.
Question 1. Is it known that no sound KPS can be complete for $3$-$SAT$?
If such a KPS was found, it would imply $P=NP$ and the polynomial-boundedness of natural propositional proof systems. 330