Skip to content

madvorak/vcsp

Repository files navigation

General-Valued Constraint Satisfaction Problems

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).

Results (please see the definitions in ValuedCSP.lean first)

Mathlib contributions that stem from this project

Pull requests (these PRs are compatible with each other)

Proposals for Linear Programming (these PRs are incompatible with each other)