Hakan Metin

Research

Publications: DBLP Google Scholar

• Composing Symmetry Propagation and Effective Symmetry Breaking for SAT Solving
  Hakan Metin, Souheib Baarir and Fabrice Kordon
  In 11th NFM 2019: Houston, TX, USA.
  [Abstract] [BibTeX]

  SAT solving is an active research area aiming at finding solutions to a large variety of problems. Propositional Satisfiability problems often exhibit symmetry properties, and exploiting them extends the class of problems that state-of-the-art solvers can handle. Two classes of approaches have been developed to take benefit of these symmetries: Static and Dynamic Symmetry Breaking based approaches. They bring benefits for complementary classes of problems. However, and to the best of our knowledge, no tentative has been made to combine them. In this paper, we study the theoretical and practical aspects of the composition of two of these approaches, namely Symmetry Propagation and Effective Symmetry Breaking. Extensive experiments conducted on symmetric problems extracted from the last seven editions of the SAT contest show the effectiveness of such a composition on many symmetrical problems.

                    @inproceedings{metin2019composing,
                      title={Composing Symmetry Propagation and Effective Symmetry Breaking for SAT Solving},
                      author={Metin, Hakan and Baarir, Souheib and Kordon, Fabrice},
                      booktitle={NASA Formal Methods Symposium},
                      pages={316--332},
                      year={2019},
                      organization={Springer}
                    }
  		

• CDCLSym: Introducing Effective Symmetry Breaking in SAT Solving
  Hakan Metin, Souheib Baarir, Maximilien Colange and Fabrice Kordon
  In 24th TACAS 2018: Thessaloniki, Greece (Part of ETAPS 2018).
  [Abstract] [BibTeX]

  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.

                    @inproceedings{metin2018cdclsym,
                      title={CDCLSym: Introducing effective symmetry breaking in SAT solving},
                      author={Metin, Hakan and Baarir, Souheib and Colange, Maximilien and Kordon, Fabrice},
                      booktitle={International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
                      pages={99--114},
                      year={2018},
                      organization={Springer}
                    }
  		

Teaching

• Introduction to Operating Systems (L2) from 2017 to 2018
• Eléments de programmation 2 (L1) in 2018