From 55b83d7205dcae654fd309e002d88bdb56e51dbc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Dvo=C5=99=C3=A1k?= Date: Thu, 30 May 2024 17:31:14 +0200 Subject: [PATCH] Update README.md --- README.md | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/README.md b/README.md index d7143bc..2e6ad12 100644 --- a/README.md +++ b/README.md @@ -10,18 +10,18 @@ Our long-term goal is to formalize the dichotomy for fixed-template finite-value ### Main results (please see the definitions in [ValuedCSP.lean](https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Combinatorics/Optimization/ValuedCSP.lean) first) -* [If a VCSP template over LinearOrderedCancelAddCommMonoid can express MaxCut, it cannot have any commutative fractional polymorphism.](https://github.com/madvorak/vcsp/blob/83e34093cb667373feb3095a2681dcda0ddfff9e/VCSP/Hardness.lean#L70) -* [Basic LP relaxation for VCSP over any OrderedRing of CharZero is valid.](https://github.com/madvorak/vcsp/blob/83e34093cb667373feb3095a2681dcda0ddfff9e/VCSP/LinearRelaxation.lean#L268) -* [If a VCSP template over ℚ has symmetric fractional polymorphisms of all arities, then Basic LP relaxation is tight.](https://github.com/madvorak/vcsp/blob/83e34093cb667373feb3095a2681dcda0ddfff9e/VCSP/LinearRelaxationAndSFP.lean#L398) +* [If a VCSP template over LinearOrderedCancelAddCommMonoid can express MaxCut, it cannot have any commutative fractional polymorphism.](https://github.com/madvorak/vcsp/blob/a96896872daccd490913d37e159a093a6dde50cb/VCSP/Hardness.lean#L70) +* [Basic LP relaxation for VCSP over any OrderedRing of CharZero is valid.](https://github.com/madvorak/vcsp/blob/a96896872daccd490913d37e159a093a6dde50cb/VCSP/LinearRelaxation.lean#L268) +* [If a VCSP template over ℚ has symmetric fractional polymorphisms of all arities, then Basic LP relaxation is tight.](https://github.com/madvorak/vcsp/blob/a96896872daccd490913d37e159a093a6dde50cb/VCSP/LinearRelaxationAndSFP.lean#L398) ### Farkas-like theorems (can be use independently of the VCSP) -* [David Bartl's version](https://github.com/madvorak/vcsp/blob/83e34093cb667373feb3095a2681dcda0ddfff9e/VCSP/FarkasBartl.lean#L190) -* [The most general version](https://github.com/madvorak/vcsp/blob/83e34093cb667373feb3095a2681dcda0ddfff9e/VCSP/FarkasBartl.lean#L252) -* [Equality version](https://github.com/madvorak/vcsp/blob/83e34093cb667373feb3095a2681dcda0ddfff9e/VCSP/FarkasBasic.lean#L102) -* [Inequality version](https://github.com/madvorak/vcsp/blob/83e34093cb667373feb3095a2681dcda0ddfff9e/VCSP/FarkasBasic.lean#L107) -* [Special version for extended rationals](https://github.com/madvorak/vcsp/blob/83e34093cb667373feb3095a2681dcda0ddfff9e/VCSP/FarkasSpecial.lean#L282) -* [Strong LP duality](https://github.com/madvorak/vcsp/blob/83e34093cb667373feb3095a2681dcda0ddfff9e/VCSP/LinearProgramming.lean#L122) (only the most basic version) +* [David Bartl's version](https://github.com/madvorak/vcsp/blob/a96896872daccd490913d37e159a093a6dde50cb/VCSP/FarkasBartl.lean#L192) +* [The most general version](https://github.com/madvorak/vcsp/blob/a96896872daccd490913d37e159a093a6dde50cb/VCSP/FarkasBartl.lean#L252) +* [Equality version](https://github.com/madvorak/vcsp/blob/a96896872daccd490913d37e159a093a6dde50cb/VCSP/FarkasBasic.lean#L102) +* [Inequality version](https://github.com/madvorak/vcsp/blob/a96896872daccd490913d37e159a093a6dde50cb/VCSP/FarkasBasic.lean#L107) +* [Special version for extended rationals](https://github.com/madvorak/vcsp/blob/a96896872daccd490913d37e159a093a6dde50cb/VCSP/FarkasSpecial.lean#L282) +* [Strong LP duality](https://github.com/madvorak/vcsp/blob/a96896872daccd490913d37e159a093a6dde50cb/VCSP/LinearProgramming.lean#L122) (only the most basic version) ## Mathlib contributions that stem from this project