Justin Wong and Pei-Wei Chen and Tianjun Zhang and Joseph Gonzalez and Yuandong Tian and Sanjit A. Seshia

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2023-103

May 11, 2023

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2023/EECS-2023-103.pdf

Applications of Satisfiability Modulo Theories (SMT) within design automation and software/hardware verification often require finding models whose quantitative cost objective is guaranteed to be optimal. As an example, in worst-case execution time analysis, it does not suffice to simply discover a feasible execution trace; we are instead interested in proving properties on the longest execution trace. Such problems can be formulated as Optimization Modulo Theory (OMT), and solving them is much more challenging than both SMT problems and unconstrained optimization. Current solutions struggle to scale to problems of large size, because they require experts to tune solvers and carefully craft problem encodings. This approach is not only problem-specific but also requires manual effort. Recent progress in neural techniques have been successfully applied to Mixed Integer Linear Programming (MILP) and certain instances of the Traveling Salesman Problem (TSP). We make the case for learning-based solvers in OMT and present Ashera, a neural-guided OMT solver. Ashera innovates on prior art by introducing Logical Neighborhood Search and neural-based warm starting. Additionally, we introduce new benchmarks for learning-based OMT techniques, targeted at real-world applications including scheduling and multi-agent TSP. Ashera exhibits as much as a 3x speedup and shows improved scaling compared to MILP approximation as used in industry and state-of-the-art OMT solvers.

---

BibTeX citation:

@techreport{Wong:EECS-2023-103,
    Author= {Wong, Justin and Chen, Pei-Wei and Zhang, Tianjun and Gonzalez, Joseph and Tian, Yuandong and Seshia, Sanjit A.},
    Title= {Ashera; Neural Guided Optimization Modulo Theory},
    Year= {2023},
    Month= {May},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2023/EECS-2023-103.html},
    Number= {UCB/EECS-2023-103},
    Abstract= {Applications of Satisfiability Modulo Theories (SMT) within design automation and software/hardware verification often require finding models whose quantitative cost objective is guaranteed to be optimal. As an example, in worst-case execution time analysis, it does not suffice to simply discover a feasible execution trace; we are instead interested in proving properties on the longest execution trace. Such problems can be formulated as Optimization Modulo Theory (OMT), and solving them is much more challenging than both SMT problems and unconstrained optimization. Current solutions struggle to scale to problems of large size, because they require experts to tune solvers and carefully craft problem encodings. This approach is not only problem-specific but also requires manual effort. Recent progress in neural techniques have been successfully applied to Mixed Integer Linear Programming (MILP) and certain instances of the Traveling Salesman Problem (TSP). We make the case for learning-based solvers in OMT and present Ashera, a neural-guided OMT solver. Ashera innovates on prior art by introducing Logical Neighborhood Search and neural-based warm starting.  Additionally, we introduce new benchmarks for learning-based OMT techniques, targeted at real-world applications including scheduling and multi-agent TSP. Ashera exhibits as much as a 3x speedup and shows improved scaling compared to MILP approximation as used in industry and state-of-the-art OMT solvers.},
}

EndNote citation:

%0 Report
%A Wong, Justin 
%A Chen, Pei-Wei 
%A Zhang, Tianjun 
%A Gonzalez, Joseph 
%A Tian, Yuandong 
%A Seshia, Sanjit A. 
%T Ashera; Neural Guided Optimization Modulo Theory
%I EECS Department, University of California, Berkeley
%D 2023
%8 May 11
%@ UCB/EECS-2023-103
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2023/EECS-2023-103.html
%F Wong:EECS-2023-103