Skip to content

Commit

Permalink
Update README.md
Browse files Browse the repository at this point in the history
  • Loading branch information
madvorak authored May 30, 2024
1 parent a968968 commit 55b83d7
Showing 1 changed file with 9 additions and 9 deletions.
18 changes: 9 additions & 9 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down

0 comments on commit 55b83d7

Please sign in to comment.