Ashera: Neural Optimization Modulo Theories

Overview:

Ashera is a state-of-the-art Optimization Modulo Theory (OMT) solver, which explicitly targets a rising class of optimization problems such as multi-agent traveling salesman (mTSP) and multi-resource DAG scheduling. We excel at disjunctive problems which lead to well studied failure modes for ILP solvers exploiting both Logical Neighborhood Search and Neural Diving. 

Logical Neighborhood Search decouples combinatorial search with convex optimization. For any feasible solution, Ashera performs convex optimization within the connected region inclusive of that feasible solution, while combinatorial search is relied upon to search for improved feasilble solutions in disjoint regions. 

Neural Diving introduced by Nair et. al trains a neural partial assignment generator which can be used to quickly explore a diverse set of plausible solutions. We observe that deployed instances of OMT problems are solved periodically. Thus, we adopt a similar notion in Ashera for generating plausible partial assignments from similar instances of the same OMT problem. 

Scheduling Example

Figure 1: Example of OMT in Periodic Scheduling 

Active Research Directions: 

In the example of task scheduling, GPUs and CPUs can be permuted and task with identical requirements can be permuted, leading to optimization challenges.  Using the Ashera framework, we are actively developing a principled approach to automate symmetry breaking. This requires both innovative approaches for detecting and learning symmetries as well as creative system design to incorporate and expoit the discovered symmetries. 

We are always actively looking for collaborators and interested users. Please direct any inquires to Justin Wong (wong.justin@berkeley.edu).

Contributors: 

Justin Wong (wong.justin@berkeley.edu)

Pei-Wei Chen (pwchen@berkeley.edu)

Tianjun Zhang (tianjunz@berkeley.edu)

Joseph E. Gonzalez (jegonzal@berkeley.edu)

Yuandong Tian (yuandong@fb.com)

Sanjit A. Seshia (sseshia@berkeley.edu)