Documentation

Complexitylib.Algebraic.LowerBound.Cutwidth.Aggregate.Geometry.Joint.Conjunction.Family

Joint weights for arbitrary signed conjunction families #

Consistent two-variable conjunctions use the graph certificate. Conjunctions on three or more variables have enough marginal bias to pay the same edge cost, and inconsistent conjunctions are constant. Their weights combine without an assumption that the actual messages are independent.

source
noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Joint.evalLiteralsFamilyWeightBound {V : Type u_1} {I : Type u_2} [Fintype V] [DecidableEq V] [Fintype I] [DecidableEq I] (L : I → Finset (V × Bool)) (two : ∀ (i : I), 2 ≤ (literalVars (L i)).card) :
Entropy.WeightBound (fun (x : V → Bool) (i : I) => evalLiterals (L i) x) (↑(Fintype.card I) * Entropy.Graph.edgeCost + ↑(Fintype.card V) * Entropy.Graph.vertexCost)

Any family of conjunctions on at least two distinct primary variables obeys the joint graph cost, including arbitrary repetitions and contradictory literals.

Equations
  • One or more equations did not get rendered due to their size.
Instances For