<?xml version="1.0" encoding="UTF-8"?>
<OAI-PMH xmlns="http://www.openarchives.org/OAI/2.0/" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:schemaLocation="http://www.openarchives.org/OAI/2.0/ http://www.openarchives.org/OAI/2.0/OAI-PMH.xsd">
  <responseDate>2026-07-23T21:02:47Z</responseDate>
  <request identifier="19640" metadataPrefix="oai_dc" verb="GetRecord">https://drops.dagstuhl.de/oai</request>
  <GetRecord>
    <record>
      <header>
        <identifier>oai:drops-oai.dagstuhl.de:19640</identifier>
        <datestamp>2026-04-20T13:10:11Z</datestamp>
        <setSpec>ddc:004</setSpec>
        <setSpec>open_access</setSpec>
      </header>
      <metadata>
        <oai_dc:dc xmlns:oai_dc="http://www.openarchives.org/OAI/2.0/oai_dc/" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:schemaLocation="http://www.openarchives.org/OAI/2.0/oai_dc/ http://www.openarchives.org/OAI/2.0/oai_dc.xsd">
          <dc:title>SAT Encodings and Beyond (Dagstuhl Seminar 23261)</dc:title>
          <dc:creator>Heule, Marijn J. H.</dc:creator>
          <dc:creator>Lynce, Inês</dc:creator>
          <dc:creator>Szeider, Stefan</dc:creator>
          <dc:creator>Schidler, Andre</dc:creator>
          <dc:subject>constraint propagation</dc:subject>
          <dc:subject>lower and upper bounds</dc:subject>
          <dc:subject>problem formulation</dc:subject>
          <dc:subject>propositional satisfiability</dc:subject>
          <dc:subject>symmetry breaking</dc:subject>
          <dc:description>This report documents the program and the outcomes of Dagstuhl Seminar 23261 "SAT Encodings and Beyond." The seminar facilitated an intense examination and discussion of current results and challenges related to encodings for SAT and related solving paradigms. The seminar featured presentations and group work that provided theoretical, practical, and industrial viewpoints. The goal was to foster more profound insights and advancements in encoding techniques, which are pivotal in enhancing solvers' efficiency.</dc:description>
          <dc:publisher>Schloss Dagstuhl – Leibniz-Zentrum für Informatik</dc:publisher>
          <dc:contributor>Marijn J. H. Heule and Inês Lynce and Stefan Szeider and Andre Schidler</dc:contributor>
          <dc:date>2024</dc:date>
          <dc:relation>Is Part Of Dagstuhl Reports, Volume 13, Issue 6 (2024)</dc:relation>
          <dc:type>Article</dc:type>
          <dc:type>Text</dc:type>
          <dc:type>doc-type:ResearchArticle</dc:type>
          <dc:type>publishedVersion</dc:type>
          <dc:format>application/pdf</dc:format>
          <dc:identifier>doi:10.4230/DagRep.13.6.106</dc:identifier>
          <dc:identifier>urn:nbn:de:0030-drops-196409</dc:identifier>
          <dc:identifier>https://drops.dagstuhl.de/entities/document/10.4230/DagRep.13.6.106</dc:identifier>
          <dc:language>eng</dc:language>
          <dc:rights>https://creativecommons.org/licenses/by/4.0/legalcode</dc:rights>
        </oai_dc:dc>
      </metadata>
    </record>
  </GetRecord>
</OAI-PMH>
