SAT 2004 START ConferenceManager    


Dealing with symmetries in Quantified Boolean Formulas

Gilles Audemard, Bertrand Mazure and Lakhdar Saïs

Presented at The Seventh International Conference on Theory and Applications of Satisfiability Testing (SAT 2004), Vancouver, BC, Canada, 10-13 May 2004


Abstract

Many reasoning task and combinatorial problems exhibit symmetries. Exploiting symmetries has been proved very important in reducing search efforts. This important task is widely investigated in constraint satisfaction problems and satisfiability of boolean formulas. In this paper, we show how symmetries can be naturally extended to Quantified Boolean Formulas (QBFs). A symmetries detection algorithm is given, extending the CNF approach proposed by Aloul and al. A new hybrid solver that handle QBFs formula and Symmetry Breaking predicates is then proposed. Experiments, conducted on instances from the last competition on QBFs, show that many of them contains symmetries. Breaking such symmetries lead to interesting improvements of QBFs solver on certain class of instances.


  
START Conference Manager (V2.47.2)
Maintainer: rrgerber@softconf.com