Abstract
Boolean functional synthesis concerns synthesizing Skolem functions for existentially quantified variables in a 2QBF specification. The problem has interesting applications even when the 2QBF specification is "unrealizable" in the classical sense. Over the last decade, significant progress has been made in solving this problem for large and difficult benchmarks. A useful paradigm that has emerged from this work is one of guess-check-repair of Skolem functions. In this talk, we look deeper into some effective techniques for "guessing" candidate Skolem functions, and for counterexample-guided repair of such functions, as implemented in two state-of-the-art tools, viz. BFSS and Manthan.