GaussianAnalysisRocq library documentation
Main resultsGlossary
On this page
GaussianApplicationsapplicationsRandomSATReplacement

Random k-SAT: forced variables and the replacement of a shorter clause

GaussianApplications.RandomSAT.Replacementapplications/RandomSAT/Replacement.v408 lines21 lemmas and theorems, 5 definitionssource
Imports 4 library modules and 8 external

External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.reals.reals, mathcomp.algebra.arithmetic_tactic, mathcomp.algebra.ring_tactic, mathcomp.algebra.field_tactic

Imported by 2

Part of target T7 of phase 12 (see Model.v). A Rocq formalization of the credited argument of the subsection 'Killing a solution set with one clause' and of the lemma 'Replacing a (k-1)-clause' of 'A limiting satisfiability threshold for every fixed clause size' (family 235 of the OpenAI math collection, revision 1581d4cbd, source/sections/forcing.tex), following the Lean development of the collection (lean/OAI/Probability/RandomSAT):

Lean: forcedVariables (Clauses.lean, line 162)

Lean: card_killingClauses (Clauses.lean, line 216)

Lean: killFraction (Replacement.lean, line 18)

Lean: killFraction_le_pow (Replacement.lean, line 56)

Lean: replacement_numeric (Replacement.lean, line 228)

Lean: shorter_clause_replacement (Replacement.lean, line 324)

S is a set of assignments on n variables.

  • forced S is the set of the variables on which all the elements of S agree, and is empty when S is empty, as b(H) = 0 for an unsatisfiable H in the manuscript; frozen S s0 is the set of the variables on which they all agree with s0 (forced_frozen).
  • A clause empties a nonempty S exactly when its variables are forced and its signs oppose the forced values (kills_frozen, frozen_kills), so these clauses correspond to the sets of k forced variables (card_kills). With kfrac b v r = 'C(b, r) / ('C(v, r) 2^r), the killing probability of a nonempty S is kfrac #|forced S| n k (killE_forced): the q_r(H) = (b)_r / (2^r (v)_r) of the manuscript.
  • Bounds on kfrac: kfrac b v r <= (b / (2 v))^r for b, r <= v and v > 0 (kfrac_le_pow), the recursion in r (kfrac_succ) and its lower bound (kfrac_succ_lower), and kfrac b v r <= 1 / (v + 1) when b <= r and 1 <= r < v, for few forced variables (kfrac_small).
  • kill_replacement, the lemma 'Replacing a (k-1)-clause': for 1 <= r < v, a > 0 with 1 / (v + 1) <= a^-r and g >= 2 (r + 1) a, the probability that a block of g independent clauses of size r + 1 empties S is at least kill r S - a^-r. The manuscript takes r = k - 1, v = n - 1, a = n^(1/k) and g = ceil(2 k n^(1/k)); the lemma assumes only the inequalities that these choices satisfy.

Main results

ResultsStatement
killE_forcedkill_replacement
For a nonempty set S of assignments on n variables with b forced variables (on which all its elements agree), the probability that a uniform clause of size k empties S is 'C(b, k) / ('C(n, k) 2^k). For 1 <= r < v, a > 0 with 1 / (v + 1) <= a^-r and an integer g >= 2 (r + 1) a, a block of g independent uniform clauses of size r + 1 empties a set S of assignments on v variables with probability at least kill r S - a^-r, for every S.

Declarations26 exported

lemma, theoremdefinitioninstancelocal
sectionkilling_clauses
Variable n : nat.
Local Notation asg := {ffun 'I_n -> bool}.
definition support source, line 60
Type
forall [n k : nat], clause n k -> {set 'I_n}
Definition
Definition support k (c : clause n k) : {set 'I_n} := [set i | val c i != None].
Used by 3 declarations in 2 files
lemma card_support_clause source, line 62 
forall [n k : nat] (c : clause n k), #|support c| = k
Statement as written in the source
Lemma card_support_clause k (c : clause n k) : #|support c| = k.
Used by 2 declarations in 2 files
definition frozen source, line 66
Type
forall [n : nat], {set {ffun 'I_n -> bool}} -> {ffun 'I_n -> bool} -> {set 'I_n}
Definition
Definition frozen (S : {set asg}) (s0 : asg) : {set 'I_n} :=
  [set i | [forall s in S, s i == s0 i]].

The variables on which all the assignments of S agree with s0.

Used by 3 declarations in 1 file
definition forced source, line 71
Type
forall [n : nat], {set {ffun 'I_n -> bool}} -> {set 'I_n}
Definition
Definition forced (S : {set asg}) : {set 'I_n} :=
  [set i | (S != set0) && [exists b, [forall s in S, s i == b]]].

The variables forced by S: those on which all its elements agree, when S is not empty.

Used by 12 declarations in 3 files
lemma forced_frozen source, line 74 
forall [n : nat] [S : {set {ffun 'I_n -> bool}}] [s0 : {ffun 'I_n -> bool}],
s0 \in S -> forced S = frozen S s0
Statement as written in the source
Lemma forced_frozen (S : {set asg}) (s0 : asg) :
  s0 \in S -> forced S = frozen S s0.
Used by 1 declaration in 1 file
lemma forced0 source, line 84 
forall n : nat, forced set0 = set0
Statement as written in the source
Lemma forced0 : forced set0 = set0.
Used by 1 declaration in 1 file
lemma kills_frozen source, line 89 
forall [n k : nat] [S : {set {ffun 'I_n -> bool}}] [s0 : {ffun 'I_n -> bool}]
  [c : clause n k],
s0 \in S ->
add_clause S c = set0 ->
forall [i : 'I_n],
\val c i != None -> i \in frozen S s0 /\ \val c i = Some (~~ s0 i)

A clause kills S when no element of S satisfies it: then each of its variables is frozen in S with the sign opposite to the frozen value.

Statement as written in the source
Lemma kills_frozen k (S : {set asg}) (s0 : asg) (c : clause n k) : s0 \in S ->
  add_clause S c = set0 ->
  forall i, val c i != None -> (i \in frozen S s0) /\ val c i = Some (~~ s0 i).
Used by 1 declaration in 1 file
lemma frozen_kills source, line 103 
forall [n k : nat] [S : {set {ffun 'I_n -> bool}}] [s0 : {ffun 'I_n -> bool}]
  [c : clause n k],
s0 \in S ->
(forall i : 'I_n,
 \val c i != None -> i \in frozen S s0 /\ \val c i = Some (~~ s0 i)) ->
add_clause S c = set0
Statement as written in the source
Lemma frozen_kills k (S : {set asg}) (s0 : asg) (c : clause n k) : s0 \in S ->
  (forall i, val c i != None ->
    (i \in frozen S s0) /\ val c i = Some (~~ s0 i)) ->
  add_clause S c = set0.
Used by 1 declaration in 1 file
definition opp_ffun source, line 116
Type
forall [n : nat], {ffun 'I_n -> bool} -> {set 'I_n} -> {ffun 'I_n -> option bool}
Definition
Definition opp_ffun (s0 : asg) (A : {set 'I_n}) : {ffun 'I_n -> option bool} :=
  [ffun i => if i \in A then Some (~~ s0 i) else None].

The opposing clause on a set A of k variables.

Used by 1 declaration in 1 file
lemma proper_opp source, line 119 
forall [n k : nat] (s0 : {ffun 'I_n -> bool}) [A : {set 'I_n}],
#|A| = k -> proper_clause k (opp_ffun s0 A)
Statement as written in the source
Lemma proper_opp k s0 (A : {set 'I_n}) :
  #|A| = k -> proper_clause k (opp_ffun s0 A).
Used by 1 declaration in 1 file
lemma card_kills source, line 128 
forall [n : nat] (k : nat) [S : {set {ffun 'I_n -> bool}}],
S != set0 -> #|[set c | add_clause S c == set0]| = 'C(#|forced S|, k)

The killing clauses of a nonempty S correspond to the sets of k forced variables.

Statement as written in the source
Lemma card_kills k (S : {set asg}) : S != set0 ->
  #|[set c : clause n k | add_clause S c == set0]| = 'C(#|forced S|, k).
Used by 1 declaration in 1 file
definition kfrac source, line 159
Type
forall {R : realType}, nat -> nat -> nat -> R
Definition
Definition kfrac {R : realType} (b v r : nat) : R :=
  'C(b, r)%:R / ('C(v, r)%:R * 2 ^+ r).

The fraction of the clauses of size r on v variables whose variables all lie in a given set of b variables, with prescribed signs.

Used by 9 declarations in 1 file
lemma killE_forced main result source, line 163 
forall (R : realType) [n : nat] (k : nat) [S : {set {ffun 'I_n -> bool}}],
S != set0 -> kill k S = kfrac #|forced S| n k

The probability that a uniform k-clause kills a nonempty S.

Main result, as the README states it

For a nonempty set S of assignments on n variables with b forced variables (on which all its elements agree), the probability that a uniform clause of size k empties S is 'C(b, k) / ('C(n, k) 2^k). For 1 <= r < v, a > 0 with 1 / (v + 1) <= a^-r and an integer g >= 2 (r + 1) a, a block of g independent uniform clauses of size r + 1 empties a set S of assignments on v variables with probability at least kill r S - a^-r, for every S.

Statement as written in the source
Lemma killE_forced (R : realType) n k (S : {set {ffun 'I_n -> bool}}) :
  S != set0 -> kill (R := R) k S = kfrac #|forced S| n k.
Used by 2 declarations in 2 files
sectionkfrac
Context {R : realType}.
Local Notation kfrac := (@kfrac R).
lemma kfrac_ge0 source, line 179 
forall {R : realType} (b v r : nat), 0 <= kfrac b v r
Statement as written in the source
Lemma kfrac_ge0 b v r : 0 <= kfrac b v r.
Used by 4 declarations in 2 files
lemma kfrac0 source, line 182 
forall {R : realType} (b v : nat), kfrac b v 0 = 1
Statement as written in the source
Lemma kfrac0 b v : kfrac b v 0 = 1.
Used by 1 declaration in 1 file
lemma kfrac_succ source, line 185 
forall {R : realType} (b : nat) [v r : nat],
(r < v)%N -> kfrac b v r.+1 = kfrac b v r * (b - r)%:R / (2 * (v - r)%:R)
Statement as written in the source
Lemma kfrac_succ b v r : (r < v)%N ->
  kfrac b v r.+1 = kfrac b v r * (b - r)%:R / (2 * (v - r)%:R).
Used by 2 declarations in 1 file
lemma ratio_le source, line 201 
forall {R : realType} [b v r : nat],
(b <= v)%N -> (r <= b)%N -> (r < v)%N -> ((b - r)%:R / (v - r)%:R : R) <= (b%:R / v%:R : R)
Statement as written in the source
Lemma ratio_le b v r : (b <= v)%N -> (r <= b)%N -> (r < v)%N ->
  (b - r)%:R / (v - r)%:R <= b%:R / v%:R :> R.
Used by 1 declaration in 1 file
lemma kfrac_le_pow source, line 213 
forall {R : realType} [b v r : nat],
(b <= v)%N -> (r <= v)%N -> (0 < v)%N -> kfrac b v r <= (b%:R / (2 * v%:R)) ^+ r
Statement as written in the source
Lemma kfrac_le_pow b v r : (b <= v)%N -> (r <= v)%N -> (0 < v)%N ->
  kfrac b v r <= (b%:R / (2 * v%:R)) ^+ r.
Used by 3 declarations in 2 files
lemma kfrac_le_half_pow source, line 228 
forall {R : realType} [b v r : nat],
(b <= v)%N -> (r <= v)%N -> (0 < v)%N -> kfrac b v r <= 2^-1 ^+ r
Statement as written in the source
Lemma kfrac_le_half_pow b v r : (b <= v)%N -> (r <= v)%N -> (0 < v)%N ->
  kfrac b v r <= 2^-1 ^+ r.
Used by 1 declaration in 1 file
lemma bin_ge_internal source, line 241 
forall [v r : nat], (0 < r)%N -> (r < v)%N -> (v <= 'C(v, r))%N
Statement as written in the source
Lemma bin_ge_internal v r : (1 <= r)%N -> (r < v)%N -> (v <= 'C(v, r))%N.
Used by 1 declaration in 1 file
lemma kfrac_small source, line 250 
forall {R : realType} [b v r : nat],
(0 < r)%N -> (r < v)%N -> (b <= r)%N -> kfrac b v r <= v.+1%:R^-1
Statement as written in the source
Lemma kfrac_small b v r : (1 <= r)%N -> (r < v)%N -> (b <= r)%N ->
  kfrac b v r <= (v.+1%:R)^-1.
Used by 1 declaration in 1 file
lemma kfrac_succ_lower source, line 272 
forall {R : realType} [b v r : nat],
(r < b)%N -> (r < v)%N -> kfrac b v r * (b%:R / (2 * v%:R)) / r.+1%:R <= kfrac b v r.+1
Statement as written in the source
Lemma kfrac_succ_lower b v r : (r.+1 <= b)%N -> (r < v)%N ->
  kfrac b v r * (b%:R / (2 * v%:R)) / r.+1%:R <= kfrac b v r.+1.
Used by 1 declaration in 1 file
lemma power_survival_bound source, line 295 
forall {R : realType} [q : R] (g : nat),
0 <= q -> q <= 1 -> (1 - q) ^+ g * (1 + g%:R * q) <= 1
Statement as written in the source
Lemma power_survival_bound (q : R) g : 0 <= q -> q <= 1 ->
  (1 - q) ^+ g * (1 + g%:R * q) <= 1.
Used by 1 declaration in 1 file
lemma block_ge_of_double source, line 307 
forall {R : realType} [x q : R] [g : nat],
0 <= x -> 2 * x <= 1 -> 0 <= q -> q <= 1 -> 2 * x <= g%:R * q -> x <= 1 - (1 - q) ^+ g
Statement as written in the source
Lemma block_ge_of_double (x q : R) g : 0 <= x -> 2 * x <= 1 -> 0 <= q ->
  q <= 1 -> 2 * x <= g%:R * q -> x <= 1 - (1 - q) ^+ g.
Used by 1 declaration in 1 file
lemma replacement_numeric source, line 324 
forall {R : realType} [b v r g : nat] [a : R],
(0 < r)%N ->
(r < v)%N ->
(b <= v)%N ->
0 < a ->
v.+1%:R^-1 <= a^-1 ^+ r ->
2 * r.+1%:R * a <= g%:R -> kfrac b v r - a^-1 ^+ r <= 1 - (1 - kfrac b v r.+1) ^+ g
Statement as written in the source
Lemma replacement_numeric b v r g (a : R) : (1 <= r)%N -> (r < v)%N ->
  (b <= v)%N -> 0 < a -> (v.+1%:R)^-1 <= a^-1 ^+ r -> 2 * r.+1%:R * a <= g%:R ->
  kfrac b v r - a^-1 ^+ r <= 1 - (1 - kfrac b v r.+1) ^+ g.
Used by 1 declaration in 1 file
lemma kill_replacement main result source, line 389 
forall [R : realType] [v r g : nat] [a : R] (S0 : {set {ffun 'I_v -> bool}}),
(0 < r)%N ->
(r < v)%N ->
0 < a ->
v.+1%:R^-1 <= a^-1 ^+ r ->
2 * r.+1%:R * a <= g%:R -> kill r S0 - a^-1 ^+ r <= 1 - survival r.+1 g S0

Replacing a shorter clause by a block of g clauses: the probability that the block kills S is at least the probability that one clause of size r kills it, minus a^-r.

Main result

Stated in the README together with killE_forced.

Statement as written in the source
Lemma kill_replacement (R : realType) v r g (a : R)
    (S : {set {ffun 'I_v -> bool}}) :
  (1 <= r)%N -> (r < v)%N -> 0 < a -> (v.+1%:R)^-1 <= a^-1 ^+ r ->
  2 * r.+1%:R * a <= g%:R ->
  kill r S - a^-1 ^+ r <= 1 - survival r.+1 g S.
Used by 1 declaration in 1 file
Generated from commit 9046883 (tag phase12) of the ellipsoid fitting repository. Signatures are printed by Rocq 9.1.1; links in the source statements come from the compiled .glob files. The source links open the files on GitHub at this commit, in the now-public repository.