@COMMENT This file was generated by bib2html.pl <https://sourceforge.net/projects/bib2html/> version 0.94
@COMMENT written by Patrick Riley <http://sourceforge.net/users/patstg/>
@COMMENT This file came from Kuldeep S. Meel's publication pages at
@COMMENT http://www.comp.nus.edu.sg/~meel/publications/
@inproceedings{JM26,
  title={
    The Limitations and Power of NP-Oracle Based Functional Synthesis Techniques
  },
  author={Juba, Brendan and Meel, Kuldeep S.},
  booktitle=AAAI,
  pages={14261--14268},
  year={2026},
  bib2html_rescat={Synthesis},
  bib2html_pubtype={Refereed Conference},
  bib2html_dl_pdf={https://doi.org/10.1609/aaai.v40i17.38440},
  abstract={
    Given a Boolean relational specification between inputs and outputs, the
    problem of functional synthesis is to construct a function that maps each
    assignment of the input to an assignment of the output such that each tuple
    of input and output assignments meets the specification. The past decade has
    witnessed significant improvement in the scalability of functional synthesis
    tools, allowing them to handle problems with tens of thousands of variables.
    A common ingredient in these approaches is their reliance on SAT solvers,
    thereby exploiting the breakthrough advances in SAT solving over the past
    three decades. While the recent techniques have been shown to perform well
    in practice, there is little theoretical understanding of the limitations
    and power of these approaches. The primary contribution of this work is to
    initiate a systematic theoretical investigation into the power of functional
    synthesis approaches that rely on NP oracles. We first show that even when
    small Skolem functions exist, naive bit-by-bit learning approaches fail due
    to the relational nature of specifications. We establish fundamental
    limitations of interpolation-based approaches proving that even when small
    Skolem functions exist, resolution-based interpolation must produce
    exponential-size circuits. We prove that access to an NP oracle is
    inherently necessary for efficient synthesis. Our main technical result
    shows that it is possible to use NP oracles to synthesize small Skolem
    functions in time polynomial in the size of the specification and the size
    of the smallest sufficient set of witnesses, establishing positive results
    for a broad class of relational specifications.
  },
}