claimroutine

Branching rule with disjoint children

Claim·§A.1 The branching rule·inside lemSparsification into bounded-occurrence k-CNF leaves

Statement (paper)

Let

H

be a nonempty proper subset of a width-

c

clause satisfying , let

H\cup P_1,\ldots,H\cup P_z

be all width-

c

clauses of

F

containing

H

, let

G

be the other clauses, and put

j=c-|H|

. Then each

P_a

has width

j

and

z\ge\theta_j

, and the satisfying assignments of the children

F_A=G\wedge H

and

F_B=G\wedge\bigwedge_{a=1}^zP_a\wedge\bigwedge_{\ell\in H}\{\neg\ell\}

are disjoint, since

F_A

requires some literal of

H

to be true whereas

F_B

requires every literal of

H

to be false.

In plain English

For a nonempty proper subset

H

of a width-

c

clause that meets the violation condition, with

H\cup P_1,\ldots,H\cup P_z

the width-

c

clauses of

F

containing

H

and

j=c-|H|

, each

P_a

has width

j

and

z\ge\theta_j

. The two children

F_A=G\wedge H

and

F_B=G\wedge\bigwedge_a P_a\wedge\bigwedge_{\ell\in H}\neg\ell

have disjoint sets of satisfying assignments.

Why it's here

This claim sets up the sparsification branching step: the width and count facts say the rewritten clauses stay within the

k

-CNF format and that the clause family around

H

is large enough. Disjointness comes from

F_A

forcing some literal of

H

true while

F_B

forces all of them false, which is what lets the lemma's tree keep leaves from sharing satisfying assignments, so the input count is the sum of the leaf counts.

Classified routine:

This is the branching step of the Impagliazzo–Paturi–Zane sparsification lemma (2001), here in the disjoint-children variant used by Calabro–Impagliazzo–Paturi. The width/count facts and the disjointness follow directly from the definitions.

Uses

Nothing else in the paper

Used by

Nothing in the paper

Sources

PaperOpen

Section: §A.1 The branching rule
Page: —
Label: —
Line: main_full_version.tex:3657

Leannot aligned

Phase 2 aligns this node to a Lean declaration.