Towards a more efficient approach to NEXP-complete problems

2^nd November 2023, 11:00
Tony Tan

Abstract

Many NEXP-complete problems have algorithms that are elegant in theory, but not so practical. For example, the satisfiability of two-variable fragment of first-order logic is a well known NEXP-complete problem. However, for more than 2 decades the only known algorithm works as follows: On input formula F, guess an exponential size model and verify that it satisfies F.

Obviously, there is a lot of room for improvement.

I will describe this talk into two parts: In the first part I will briefly describe some of the recent work on two-variable logic. In the second part I will discuss Dependency Quantified Boolean Formula (DQBF) and its strong correlation with SAT which makes it an ideal candidate as the problem in the class NEXP, just like SAT is the problem in the class NP.