§ DRUP

• Slides Merijn Heule: Proof Systems and Proof Complexity
• Clause $C$ is implied by $\Gamma$ via UP (unit propagation) iff unit propagation can prove UNSAT for $\Gamma \land \not C$.
• That is, $\Gamma \implies C$ is a tautology, which is to say, $\lnot \Gamma \lor C$ is a tautology, or that $\lnot (\lnot \Gamma \lor C)$ is UNSAT, or that $\Gamma \land \not C$ is UNSAT.

§ Beyond Inference

• Allow equisatisfiability, not just implication! (Can reqd equisatisfiability as WLOG).
• For example, the "pure literal rule", which allows one to infer a clause [l] if l only occurs positively in all clauses!
• Such inferences are captured by a proof system, extended resolution (Tseitin 1966):

• This adds the definition x := AND(A, B).
• It can be seen to do this by converting the fomula x <-> AND(A, B) into CNF.
• Backward direction AND(A, B) -> x is !(A && B) || x which is !A || !B || x.
• Forward direction: x -> AND(A, B) whose contrapositive is !(A &&B) -> !x, which is !(!(A && B)) || !x, which is (A && B) || !x, which is (A || !x) && (B || !x)
• First interference-based proof system (WTH is interference?)
• No known lower bounds on proof length, so crazy strong proof system.

§ Interference Based Proof Systems

• The Potential of Interference-Based Proof Systems

Interferences differ from classical inferences, which do not affect the models of a set of formulas, because they only allow the derivation of formulas (conclusions) that are implied by the original formulas (premises). Moreover, while inferences reason about the presence of formulas (the premises), interferences can be seen as reasoning about their absence.

§ Blocked Clause Rule

• Suppose we have a CNF formula $F$ ( $F$ is a set of clauses).
• We want to add a clause $C \lor l$.
• To preserve satisfiability, it must be that if we assign $l = T$, then all clauses in $F$ that are of the form $D \lor \lnot l$ are satisfiabile.
• We can encode this by saying that $C \lor D$ is a tautology, because either $C$ is true, in which case we assign $l = F$, or $D$ is true, in which case we assign $l = T$.
• Interestingly, see that $C \lor D$ is a resolvent at $l$ of $C \lor l$ with $D \lnot \lnot l$.
• Extending Resolution with this rule gives expoentially smaller proofs.

§ Autarkies

• An autarky is a society that is economically independent.
• A partial assignment $A$ is an autarky iff every assignment touched by $A$ is satisfied by $A$.
• I guess the idea is that the literals in the autarky $A$ are independent, since they make sure that any "territory" they are a part of is completely solved by them!

§ An example: pure literals

• Think of the case of a assignment $A[l] = T$ that occurs in a formula $\Gamma$ only positively.
• For any clause $C \in \Gamma$ such that $l \in C$, we have that $C[A] = T$, since $l$ only occurs positively.
• Thus, computing $\Gamma[A]$ will make all clauses that contain $l$ "vanish". It's as if we didn't have $l$ at all.
• See that this is equisatisfiable with the original formala.
• If $\Gamma$ has a satisfying assignment $A'$, then since $l$ only occurs positively, we can tweak and see that $A'[l := T]$ also makes $\Gamma$ SAT. But this means that we have a satisfying assignment $A'$ for $\Gamma[l := T]$ as well!
• On the other hand, suppose $\Gamma[l := T]$ is UNSAT. Then we wish to show that $\Gamma$ is UNSAT.
• For contradiction, suppose that $\Gamma$ has a sastisfying assignment $C$ (for contradiction). Once again, we can tweak the assignment such that we get $C[l := T]$, which will continue to be a satisfying assignment for $\Gamma$.
• Hm, this is not a super clean proof.
• The key idea is that we "eliminate" all clauses where $l := T$, so we do not get "half assigned" clauses we we delete $l$ by setting $l = F$.

§ To think

• How do show this by editing a resolution proof for $\Gamma$ into a resolution proof for $\Gamma[l := T]$?
• I guess what we can do is to consider the sub-resolution graph once $l$ has been eliminated? Needs some thought.

§ Extending the proof to any autarky

• The key property we need is that upon using an autarky assignment, all clauses that contain any literals from the assignment disappear, so we get a purified problem without any mention of these literals.

§ Conditional Autarky

• An assigment $A \equiv A_{con} \sqcup A_{aut}$ is a conditional autarky for $\Gamma$ if $A_{aut}$ is an autarky for $\Gamma[A_{con}]$.
• This says that once we substitute $A_{con}$, we get an autarky $A_{aut}$.
• We claim that $\Gamma$ and $\Gamma \land (A_{con} \implies A_{aut})$ are equisatisfiable, if $A$ is a conditional autarky.
• Clearly, if $\Gamma \land (A_{con} \implies A_{aut})$ is SAT, then $\Gamma$ is SAT.
• On the other side, suppose $\Gamma$ is satisfiable for assignment $B$. Two cases:
• (a) if $A_{con}[B] = F$, then we are done, since the implication is true.
• (b) if $A_{con}[B] = T$, then we need to show that $A_{aut}$ is SAT. But this means that we can replace $\Gamma$ with $\Gamma[A_{con}]$, for which by the previous autarky argument, we can safely change the model $B$ to $B'$ to make $A_{aut}$ SAT, and this will extend to a model of $\Gamma$ (unsure).