VCSP project discussion

Stream: general

[Martin Dvořák]

As @Shreyas Srinivas in
https://leanprover.zulipchat.com/#narrow/stream/113486-announce/topic/VCSP.20release
suggested, I am opening a thread for a discussion about my VCSP project beyond the PRs that are already discussed in respective threads.

[Shreyas Srinivas]

Is integer programming on the cards?

[Martin Dvořák]

You can get integer programming as a special case of
https://github.com/madvorak/vcsp/blob/b29ed7d0a7c0cc2ef6bdb814acc26af533b7f1a6/VCSP/LinearProgramming.lean#L33
but there is currently no theory about integer programming and no algorithms to solve them. I will highly appreciate any such contribution whether it is into Mathlib or into my project!

[Martin Dvořák]

Actually, you can also model integer programming as a special case of docs#ValuedCSP where D = Int and C = ENat and the template is infinite.