Scalable SAT Solving in the Cloud (Mallob)

简介

• 并行赛道：1节点（64核+256GB）运行5000秒
• 云（分布式）赛道：100节点（16核+64G）运行1000秒，MPI通信

• HordeSat：2015年提出的分布式SAT求解框架（当时SAT竞赛还没有云赛道）
• Mallob：可扩展的、负载均衡的、去中心的、多任务的分布式SAT求解框架。

符号

环境：个节点，每个节点个计算单元，每个计算单元个核心（线程）

任务分配的单位：计算单元，，同样也是MPI通信的单元​

任务：共个任务，每个任务有对应的资源需求​，即计算单元个数

任务分配

当任务进入系统：

• 寻找一个空闲的计算单元​：稀疏正则图上的随机游走
  • 立方体：8节点的稀疏正则图
• 以为根构建任务树（完全二叉树），为任务实际占用的资源

根据SC的要求：一次只能运行一个任务，可以直接使用计算单元的物理地址构建任务树。

针对大规模任务出现内存恐慌(Memory Panic)：逐步减少每个计算单元中运行的顺序SAT示例个数，至少保证一个MPI负责一个。

子句通信

• 合并方法：2或3路归并
• 查重方法：可能存在两个不一样的子句，仅对二元子句做额外的重复判断

• 缓存空间限制：，其中是默认缓冲区大小，是合并数量，是超参数