<?xml version="1.0" encoding="utf-8"?>
<TEI xmlns="http://www.tei-c.org/ns/1.0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:hal="http://hal.archives-ouvertes.fr/" xmlns:gml="http://www.opengis.net/gml/3.3/" xmlns:gmlce="http://www.opengis.net/gml/3.3/ce" version="1.1" xsi:schemaLocation="http://www.tei-c.org/ns/1.0 http://api.archives-ouvertes.fr/documents/aofr-sword.xsd">
  <teiHeader>
    <fileDesc>
      <titleStmt>
        <title>HAL TEI export of hal-01766948</title>
      </titleStmt>
      <publicationStmt>
        <distributor>CCSD</distributor>
        <availability status="restricted">
          <licence target="https://creativecommons.org/publicdomain/zero/1.0/">CC0 1.0 - Universal</licence>
        </availability>
        <date when="2026-05-24T22:31:21+02:00"/>
      </publicationStmt>
      <sourceDesc>
        <p part="N">HAL API Platform</p>
      </sourceDesc>
    </fileDesc>
  </teiHeader>
  <text>
    <body>
      <listBibl>
        <biblFull>
          <titleStmt>
            <title xml:lang="en">CDCLSym: Introducing Effective Symmetry Breaking in SAT Solving</title>
            <author role="aut">
              <persName>
                <forename type="first">Hakan</forename>
                <surname>Metin</surname>
              </persName>
              <email type="md5">20810eb896f965d15f360d124dfa9e4c</email>
              <email type="domain">lip6.fr</email>
              <idno type="idhal" notation="numeric">1030869</idno>
              <idno type="halauthorid" notation="string">1351439-1030869</idno>
              <affiliation ref="#struct-541717"/>
            </author>
            <author role="aut">
              <persName>
                <forename type="first">Souheib</forename>
                <surname>Baarir</surname>
              </persName>
              <email type="md5">db8f12c6ee84295c784d957461c9fda6</email>
              <email type="domain">lip6.fr</email>
              <idno type="idhal" notation="numeric">961876</idno>
              <idno type="halauthorid" notation="string">686508-961876</idno>
              <idno type="ORCID">https://orcid.org/0000-0001-8140-0273</idno>
              <idno type="IDREF">https://www.idref.fr/147205336</idno>
              <idno type="VIAF">https://viaf.org/viaf/189805824</idno>
              <affiliation ref="#struct-541717"/>
            </author>
            <author role="aut">
              <persName>
                <forename type="first">Maximilien</forename>
                <surname>Colange</surname>
              </persName>
              <email type="md5">57e8d0800836297264e5dfc50dc93e24</email>
              <email type="domain">lip6.fr</email>
              <idno type="idhal" notation="numeric">971687</idno>
              <idno type="halauthorid" notation="string">956742-971687</idno>
              <affiliation ref="#struct-10947"/>
            </author>
            <author role="aut">
              <persName>
                <forename type="first">Fabrice</forename>
                <surname>Kordon</surname>
              </persName>
              <email type="md5">c31b42c685f457d01a9fb6a6d448fd9d</email>
              <email type="domain">lip6.fr</email>
              <idno type="idhal" notation="string">fabrice-kordon</idno>
              <idno type="idhal" notation="numeric">9774</idno>
              <idno type="halauthorid" notation="string">7750-9774</idno>
              <idno type="ORCID">https://orcid.org/0000-0002-5626-828X</idno>
              <idno type="IDREF">https://www.idref.fr/074605283</idno>
              <idno type="VIAF">https://viaf.org/viaf/55088809</idno>
              <affiliation ref="#struct-541717"/>
            </author>
            <editor role="depositor">
              <persName>
                <forename>Fabrice</forename>
                <surname>Kordon</surname>
              </persName>
              <email type="md5">c31b42c685f457d01a9fb6a6d448fd9d</email>
              <email type="domain">lip6.fr</email>
            </editor>
          </titleStmt>
          <editionStmt>
            <edition n="v1" type="current">
              <date type="whenSubmitted">2018-04-14 19:02:24</date>
              <date type="whenModified">2024-10-30 13:34:14</date>
              <date type="whenReleased">2018-04-23 11:32:02</date>
              <date type="whenProduced">2018-04-14</date>
              <date type="whenEndEmbargoed">2018-04-14</date>
              <ref type="file" target="https://hal.sorbonne-universite.fr/hal-01766948v1/document">
                <date notBefore="2018-04-14"/>
              </ref>
              <ref type="file" subtype="greenPublisher" n="1" target="https://hal.sorbonne-universite.fr/hal-01766948v1/file/10.1007-978-3-319-89960-2_6.pdf" id="file-1766948-1804308">
                <date notBefore="2018-04-14"/>
              </ref>
            </edition>
            <respStmt>
              <resp>contributor</resp>
              <name key="151582">
                <persName>
                  <forename>Fabrice</forename>
                  <surname>Kordon</surname>
                </persName>
                <email type="md5">c31b42c685f457d01a9fb6a6d448fd9d</email>
                <email type="domain">lip6.fr</email>
              </name>
            </respStmt>
          </editionStmt>
          <publicationStmt>
            <distributor>CCSD</distributor>
            <idno type="halId">hal-01766948</idno>
            <idno type="halUri">https://hal.sorbonne-universite.fr/hal-01766948</idno>
            <idno type="halBibtex">metin:hal-01766948</idno>
            <idno type="halRefHtml">&lt;i&gt;Tools and Algorithms for the Construction and Analysis of Systems -- TACAS&lt;/i&gt;, Apr 2018, Tessaloniki, Greece</idno>
            <idno type="halRef">Tools and Algorithms for the Construction and Analysis of Systems -- TACAS, Apr 2018, Tessaloniki, Greece</idno>
            <availability status="restricted">
              <licence target="https://about.hal.science/hal-authorisation-v1/">HAL Authorization<ref corresp="#file-1766948-1804308"/></licence>
            </availability>
          </publicationStmt>
          <seriesStmt>
            <idno type="stamp" n="CNRS">CNRS - Centre national de la recherche scientifique</idno>
            <idno type="stamp" n="LIP6" corresp="SORBONNE-UNIVERSITE">Laboratoire d'Informatique de Paris 6</idno>
            <idno type="stamp" n="SORBONNE-UNIVERSITE">Sorbonne Université</idno>
            <idno type="stamp" n="SORBONNE-UNIV" corresp="SORBONNE-UNIVERSITE">Sorbonne Université 01/01/2018</idno>
            <idno type="stamp" n="SU-SCIENCES" corresp="SORBONNE-UNIVERSITE">Faculté des Sciences de Sorbonne Université</idno>
            <idno type="stamp" n="TEST-HALCNRS">Collection test HAL CNRS</idno>
            <idno type="stamp" n="SU-TI">Sorbonne Université - Texte Intégral</idno>
            <idno type="stamp" n="ALLIANCE-SU"> Alliance Sorbonne Université</idno>
            <idno type="stamp" n="SUPRA_MATHS_INFO">Mathématiques + Informatique</idno>
          </seriesStmt>
          <notesStmt>
            <note type="audience" n="2">International</note>
            <note type="invited" n="0">No</note>
            <note type="popular" n="0">No</note>
            <note type="peer" n="1">Yes</note>
            <note type="proceedings" n="1">Yes</note>
          </notesStmt>
          <sourceDesc>
            <biblStruct>
              <analytic>
                <title xml:lang="en">CDCLSym: Introducing Effective Symmetry Breaking in SAT Solving</title>
                <author role="aut">
                  <persName>
                    <forename type="first">Hakan</forename>
                    <surname>Metin</surname>
                  </persName>
                  <email type="md5">20810eb896f965d15f360d124dfa9e4c</email>
                  <email type="domain">lip6.fr</email>
                  <idno type="idhal" notation="numeric">1030869</idno>
                  <idno type="halauthorid" notation="string">1351439-1030869</idno>
                  <affiliation ref="#struct-541717"/>
                </author>
                <author role="aut">
                  <persName>
                    <forename type="first">Souheib</forename>
                    <surname>Baarir</surname>
                  </persName>
                  <email type="md5">db8f12c6ee84295c784d957461c9fda6</email>
                  <email type="domain">lip6.fr</email>
                  <idno type="idhal" notation="numeric">961876</idno>
                  <idno type="halauthorid" notation="string">686508-961876</idno>
                  <idno type="ORCID">https://orcid.org/0000-0001-8140-0273</idno>
                  <idno type="IDREF">https://www.idref.fr/147205336</idno>
                  <idno type="VIAF">https://viaf.org/viaf/189805824</idno>
                  <affiliation ref="#struct-541717"/>
                </author>
                <author role="aut">
                  <persName>
                    <forename type="first">Maximilien</forename>
                    <surname>Colange</surname>
                  </persName>
                  <email type="md5">57e8d0800836297264e5dfc50dc93e24</email>
                  <email type="domain">lip6.fr</email>
                  <idno type="idhal" notation="numeric">971687</idno>
                  <idno type="halauthorid" notation="string">956742-971687</idno>
                  <affiliation ref="#struct-10947"/>
                </author>
                <author role="aut">
                  <persName>
                    <forename type="first">Fabrice</forename>
                    <surname>Kordon</surname>
                  </persName>
                  <email type="md5">c31b42c685f457d01a9fb6a6d448fd9d</email>
                  <email type="domain">lip6.fr</email>
                  <idno type="idhal" notation="string">fabrice-kordon</idno>
                  <idno type="idhal" notation="numeric">9774</idno>
                  <idno type="halauthorid" notation="string">7750-9774</idno>
                  <idno type="ORCID">https://orcid.org/0000-0002-5626-828X</idno>
                  <idno type="IDREF">https://www.idref.fr/074605283</idno>
                  <idno type="VIAF">https://viaf.org/viaf/55088809</idno>
                  <affiliation ref="#struct-541717"/>
                </author>
              </analytic>
              <monogr>
                <title level="m">Tools and Algorithms for the Construction and Analysis of Systems 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings,</title>
                <meeting>
                  <title>Tools and Algorithms for the Construction and Analysis of Systems -- TACAS</title>
                  <date type="start">2018-04-14</date>
                  <settlement>Tessaloniki</settlement>
                  <country key="GR">Greece</country>
                </meeting>
                <imprint/>
              </monogr>
            </biblStruct>
          </sourceDesc>
          <profileDesc>
            <langUsage>
              <language ident="en">English</language>
            </langUsage>
            <textClass>
              <classCode scheme="halDomain" n="info.info-se">Computer Science [cs]/Software Engineering [cs.SE]</classCode>
              <classCode scheme="halDomain" n="info.info-es">Computer Science [cs]/Embedded Systems</classCode>
              <classCode scheme="halDomain" n="info.info-fl">Computer Science [cs]/Formal Languages and Automata Theory [cs.FL]</classCode>
              <classCode scheme="halDomain" n="info.info-lo">Computer Science [cs]/Logic in Computer Science [cs.LO]</classCode>
              <classCode scheme="halTypology" n="COMM">Conference papers</classCode>
              <classCode scheme="halOldTypology" n="COMM">Conference papers</classCode>
              <classCode scheme="halTreeTypology" n="COMM">Conference papers</classCode>
            </textClass>
            <abstract xml:lang="en">
              <p>SAT solvers are now widely used to solve a large variety of problems, including formal verification of systems. SAT problems derived from such applications often exhibit symmetry properties that could be exploited to speed up their solving. Static symmetry breaking is so far the most popular approach to take advantage of symmetries. It relies on a symmetry preprocessor which augments the initial problem with constraints that force the solver to consider only a few configurations among the many symmetric ones. This paper presents a new way to handle symmetries, that avoid the main problem of the current static approaches: the prohibitive cost of the preprocessing phase. Our proposal has been implemented in MiniSym. Extensive experiments on the benchmarks of last six SAT competitions show that our approach is competitive with the best state-of-the-art static symmetry breaking solutions.</p>
            </abstract>
          </profileDesc>
        </biblFull>
      </listBibl>
    </body>
    <back>
      <listOrg type="structures">
        <org type="researchteam" xml:id="struct-541717" status="VALID">
          <orgName>Modélisation et Vérification</orgName>
          <orgName type="acronym">MoVe</orgName>
          <date type="start">2018-01-01</date>
          <desc>
            <address>
              <country key="FR"/>
            </address>
          </desc>
          <listRelation>
            <relation active="#struct-541703" type="direct"/>
            <relation active="#struct-413221" type="indirect"/>
            <relation name="UMR7606" active="#struct-441569" type="indirect"/>
          </listRelation>
        </org>
        <org type="laboratory" xml:id="struct-10947" status="OLD">
          <orgName>Laboratoire de Recherche et de Développement de l'EPITA</orgName>
          <orgName type="acronym">LRDE</orgName>
          <date type="end">2022-08-31</date>
          <desc>
            <address>
              <addrLine>LRDE, EPITA 14-16, rue Voltaire F-94276 Le Kremlin Bicêtre cedex France</addrLine>
              <country key="FR"/>
            </address>
            <ref type="url">http://www.lrde.epita.fr</ref>
          </desc>
          <listRelation>
            <relation active="#struct-305456" type="direct"/>
          </listRelation>
        </org>
        <org type="laboratory" xml:id="struct-541703" status="VALID">
          <idno type="IdRef">13558292X</idno>
          <idno type="RNSR">199712651U</idno>
          <idno type="ROR">https://ror.org/05krcen59</idno>
          <orgName>LIP6</orgName>
          <date type="start">2018-01-01</date>
          <desc>
            <address>
              <addrLine>4 Place JUSSIEU 75252 PARIS CEDEX 05</addrLine>
              <country key="FR"/>
            </address>
            <ref type="url">http://www.lip6.fr/</ref>
          </desc>
          <listRelation>
            <relation active="#struct-413221" type="direct"/>
            <relation name="UMR7606" active="#struct-441569" type="direct"/>
          </listRelation>
        </org>
        <org type="regroupinstitution" xml:id="struct-413221" status="VALID">
          <idno type="IdRef">221333754</idno>
          <idno type="ROR">https://ror.org/02en5vm52</idno>
          <orgName>Sorbonne Université</orgName>
          <orgName type="acronym">SU</orgName>
          <date type="start">2018-01-01</date>
          <desc>
            <address>
              <addrLine>21 rue de l’École de médecine - 75006 Paris</addrLine>
              <country key="FR"/>
            </address>
            <ref type="url">http://www.sorbonne-universite.fr/</ref>
          </desc>
        </org>
        <org type="regroupinstitution" xml:id="struct-441569" status="VALID">
          <idno type="IdRef">02636817X</idno>
          <idno type="ISNI">0000000122597504</idno>
          <idno type="ROR">https://ror.org/02feahw73</idno>
          <orgName>Centre National de la Recherche Scientifique</orgName>
          <orgName type="acronym">CNRS</orgName>
          <date type="start">1939-10-19</date>
          <desc>
            <address>
              <country key="FR"/>
            </address>
            <ref type="url">https://www.cnrs.fr/</ref>
          </desc>
        </org>
        <org type="institution" xml:id="struct-305456" status="VALID">
          <orgName>Ecole Pour l'Informatique et les Techniques Avancées</orgName>
          <orgName type="acronym">EPITA</orgName>
          <date type="start">2016-11-23</date>
          <desc>
            <address>
              <country key="FR"/>
            </address>
          </desc>
        </org>
      </listOrg>
    </back>
  </text>
</TEI>