<!DOCTYPE article PUBLIC "-//NLM//DTD JATS (Z39.96) Journal Archiving and Interchange DTD v1.0 20120330//EN" "JATS-archivearticle1.dtd">
<article xmlns:xlink="http://www.w3.org/1999/xlink">
  <front>
    <journal-meta />
    <article-meta>
      <title-group>
        <article-title>Invited Talk: SAT Reasoning in CDCL(T) Solvers</article-title>
      </title-group>
      <contrib-group>
        <contrib contrib-type="author">
          <string-name>Katalin Fazekas</string-name>
          <email>k.katalin.fazekas@gmail.com</email>
          <xref ref-type="aff" rid="aff0">0</xref>
        </contrib>
        <contrib contrib-type="author">
          <string-name>Declaration on Generative AI</string-name>
        </contrib>
        <aff id="aff0">
          <label>0</label>
          <institution>TU Wien, Formal Methods in Systems Engineering, Institute of Logic and Computation</institution>
          ,
          <addr-line>Favoritenstraße 9-11/192-4, A-1040 Vienna</addr-line>
          ,
          <country country="AT">Austria</country>
        </aff>
      </contrib-group>
      <pub-date>
        <year>2023</year>
      </pub-date>
      <volume>271</volume>
      <abstract>
        <p>In our recent work we introduced an extension for the IPASIR interface of incremental SAT solvers. This extension, named IPASIR-UP, supports continuous interactions with the solver during SAT reasoning, allowing SMT solvers to seamlessly integrate any IPASIR-UP-compatible SAT solver as their core engine. While IPASIR-UP enables crucial interactions between SAT and theory solvers, the full potential of modern incremental SAT features, such as advanced inprocessing techniques, comprehensive proof production, and diverse search heuristics, remains largely untapped within this framework. In this talk, I presented the current landscape of embedding SAT solvers into SMT solvers via IPASIR-UP. I highlighted the currently supported features, discussed their limitations, and presented some open problems and challenges that need to be addressed in the future. This talk is based on joint work with Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, Mathias Fleury, Florian Pollitt, and Armin Biere [1, 2, 3, 4].</p>
      </abstract>
    </article-meta>
  </front>
  <body />
  <back>
    <ref-list />
  </back>
</article>