A Parameterized Approach to Equality Graph Saturation

PhD Qualifying Examination


Title: "A Parameterized Approach to Equality Graph Saturation"

by

Mr. Chun Kit LAM


Abstract:

Equality graphs (e-graphs) are used to compactly represent equivalence classes 
of terms in symbolic reasoning systems. Beyond their original roots in 
automated theorem proving, e-graphs have been used in a variety of 
applications. They have become particularly important as the key ingredient in 
the popular technique of equality saturation, which has notable applications in 
compiler optimization, program synthesis, program verification, and symbolic 
execution, among others. However, despite its crucial role in equality 
saturation, e-graph extraction has received relatively little attention in the 
literature, which we seek to start addressing.

In this survey, we will formally define the e-graph extraction problem, show 
that it is NP-hard and hard to approximate to a constant factor, and present a 
fixed-parameter tractable algorithm for finding the optimal extraction.


Date:                   Monday, 29 April 2024

Time:                   4:00pm - 6:00pm

Venue:                  Room 5501
                        Lifts 25/26

Committee Members:      Dr. Amir Goharshady (Supervisor)
                        Dr. Lionel Parreaux (Supervisor)
                        Dr. Jiasi Shen (Chairperson)
                        Prof. Siu-Wing Cheng