This is a playground for experiments preceding our contribution to the Lean 4 version of Mathlib.
Permalink to the definition of VCSP in Mathlib
Our long-term goal is to formalize the dichotomy for fixed-template finite-valued constraint satisfaction problems [Thapper, Živný, Kolmogorov] while exploring potential generalizations (infinite domains, partially ordered codomains, and more).
Main results (please see the definitions in ValuedCSP.lean first)
- If a VCSP template over LinearOrderedCancelAddCommMonoid can express MaxCut, it cannot have any commutative fractional polymorphism.
- Basic LP relaxation for VCSP over any OrderedRing of CharZero is valid.
- If a VCSP template over ℚ has symmetric fractional polymorphisms of all arities, then Basic LP relaxation is tight.
- David Bartl's version
- Our most general version
- Equality version
- Inequality version
- Special version for extended rationals
- Strong LP duality
- leanprover-community/mathlib4#7404
- leanprover-community/mathlib4#7893
- leanprover-community/mathlib4#7894
- leanprover-community/mathlib4#8707
- leanprover-community/mathlib4#9072
- leanprover-community/mathlib4#9307
- leanprover-community/mathlib4#9652
- leanprover-community/mathlib4#9838
- leanprover-community/mathlib4#10297
- leanprover-community/mathlib4#10379
- leanprover-community/mathlib4#11689
- leanprover-community/mathlib4#12806
- leanprover-community/mathlib4#12901
- leanprover-community/mathlib4#12903
- leanprover-community/mathlib4#12911
- leanprover-community/mathlib4#13167