#flags #algebra #graph #combinatorics

flag-algebra

Razborov的旗帜代数实现

16个不稳定版本 (3个破坏性更新)

0.4.0 2024年6月24日
0.3.0 2024年2月5日
0.2.1 2023年6月27日
0.1.12 2021年4月25日
0.1.3 2019年1月24日

#64数学

Download history 135/week @ 2024-06-21 9/week @ 2024-06-28

864 每月下载次数

GPL-3.0 许可证

230KB
6K SLoC

flag-algebra

旗帜代数的泛型实现。

旗帜代数是一种用于产生组合数学中某些不等式的计算机辅助证明的框架,依赖于半定规划。

示例

// Proving that in any graph, at least 1/4 of the triples
// are triangles or independent sets.
use flag_algebra::*;
use flag_algebra::flags::Graph;

// Work on the graphs of size 3.
let basis = Basis::new(3);

// Define useful flags.
let k3 = flag(&Graph::new(3, &[(0, 1), (1, 2), (2, 0)])); // Triangle
let e3 = flag(&Graph::new(3, &[])); // Independent set of size 3

// Definition of the optimization problem.
let pb = Problem::<i64, _> {
    // Constraints
   ineqs: vec![total_sum_is_one(basis), flags_are_nonnegative(basis)],
    // Use all relevant Cauchy-Schwarz inequalities.
    cs: basis.all_cs(),
    // Minimize density of triangle plus density of independent of size 3.
    obj: k3 + e3,
};

// Write the correspondind SDP program in "goodman.sdpa".
// This program can then be solved by CSDP. The answer would be 0.25.
pb.write_sdpa("goodman").unwrap();

功能

此库目前可以执行以下操作。

  • 从头生成旗帜列表。
  • 生成旗帜代数算子和将它们存储在文件中。
  • 在旗帜代数中进行计算(乘法,去标签)并添加用户定义的向量。
  • 定义、操作或放大旗帜不等式(例如通过将不等式乘以所有旗帜)。
  • 以.spda格式编写问题或直接运行CSDP求解器。
  • 自动消除不必要的约束(以原始方式)。
  • 它是泛型的:定义新的特定类/子类旗帜归结为实现Rust Trait。
  • 以(希望)可读的格式输出旗帜、问题或证书作为HTML页面(假设其大小合理)。

支持的旗帜

此库是泛型的。要使用一种组合对象(例如图)作为旗帜,只需为相应的Rust数据类型实现Flag trait即可。

目前,Flag已针对GraphsOriented graphsDirected graphsedge-colored graphs(具有一些固定的颜色数)实现。

除了直接为您的类型实现[Flag],还有两种机制帮助根据现有的旗帜类定义旗帜类。

  • 用于定义顶点着色标记的Colored结构。如果N是一个整数标识符,则Colored<F, N>是类型为F的标记的类型,其中顶点进一步用N种不同的颜色着色。当F实现时,Colored<F, N>会自动实现Flag
  • 为已定义类的子集的类[SubClass]结构和[SubFlag]。这在例如在不考虑其他图的情况下计算无三角形的图标记代数时很有用。有关更多详细信息,请参阅[SubFlag]的文档页面。

表达标记代数中的元素

参见[Type]、[Basis]和[QFlag]。

Type<F:Flag>结构识别标记代数中的“类型”σ(即完全标记的标记)由一个对象表示。结构Basis<F:Flag>对应于一个(n, σ)对,并识别大小为n的σ标记集合。结构QFlag

许可:GPL-3.0

依赖项

~74MB
~1M SLoC