Name
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 et al. A new hybrid solver that handle QBFs 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. |
Year | Venue | Keywords |
|---|---|---|
2004 | SAT | symmetry breaking,constraint satisfaction problem,satisfiability |
Field | DocType | Citations |
Maximum satisfiability problem,Discrete mathematics,Combinatorics,Computer science,Boolean satisfiability problem,Parity function,Constraint satisfaction problem,True quantified Boolean formula,Boolean expression,And-inverter graph,Two-element Boolean algebra | Conference | 4 |
PageRank | References | Authors |
0.44 | 8 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Gilles Audemard | 1 | 640 | 37.66 |
| Bertrand Mazure | 2 | 413 | 29.79 |
| Lakhdar Sais | 3 | 859 | 65.57 |