Difference between revisions of "Publications/metin.18.tacas"
From LRDE
(3 intermediate revisions by the same user not shown) | |||
Line 5: | Line 5: | ||
| title = CDCLSym: Introducing Effective Symmetry Breaking in SAT Solving |
| title = CDCLSym: Introducing Effective Symmetry Breaking in SAT Solving |
||
| booktitle = Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'18) |
| booktitle = Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'18) |
||
− | | pages = |
+ | | pages = 99 to 114 |
| publisher = Springer |
| publisher = Springer |
||
| series = Lecture Notes in Computer Science |
| series = Lecture Notes in Computer Science |
||
− | | volume = |
+ | | volume = 10805 |
| address = Thessaloniki, Greece |
| address = Thessaloniki, Greece |
||
| abstract = 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 avoids the main problem of the current static approaches: the prohibitive cost of the preprocessing phase. 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. |
| abstract = 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 avoids the main problem of the current static approaches: the prohibitive cost of the preprocessing phase. 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. |
||
+ | | lrdepaper = http://www.lrde.epita.fr/dload/papers/metin.18.tacas.pdf |
||
| lrdenewsdate = 2018-01-05 |
| lrdenewsdate = 2018-01-05 |
||
| lrdeprojects = Spot |
| lrdeprojects = Spot |
||
| type = inproceedings |
| type = inproceedings |
||
| id = metin.18.tacas |
| id = metin.18.tacas |
||
+ | | identifier = doi:10.1007/978-3-319-89960-2_6 |
||
| bibtex = |
| bibtex = |
||
@InProceedings<nowiki>{</nowiki> metin.18.tacas, |
@InProceedings<nowiki>{</nowiki> metin.18.tacas, |
||
author = <nowiki>{</nowiki>Hakan Metin and Souheib Baarir and Maximilien Colange and |
author = <nowiki>{</nowiki>Hakan Metin and Souheib Baarir and Maximilien Colange and |
||
Fabrice Kordon<nowiki>}</nowiki>, |
Fabrice Kordon<nowiki>}</nowiki>, |
||
− | title = <nowiki>{</nowiki>CDCLSym: Introducing Effective Symmetry Breaking in |
+ | title = <nowiki>{</nowiki><nowiki>{</nowiki>CDCLSym<nowiki>}</nowiki>: Introducing Effective Symmetry Breaking in |
− | Solving<nowiki>}</nowiki>, |
+ | <nowiki>{</nowiki>SAT<nowiki>}</nowiki> Solving<nowiki>}</nowiki>, |
booktitle = <nowiki>{</nowiki>Proceedings of the 24th International Conference on Tools |
booktitle = <nowiki>{</nowiki>Proceedings of the 24th International Conference on Tools |
||
and Algorithms for the Construction and Analysis of Systems |
and Algorithms for the Construction and Analysis of Systems |
||
Line 26: | Line 28: | ||
year = 2018, |
year = 2018, |
||
month = apr, |
month = apr, |
||
− | pages = <nowiki>{</nowiki> |
+ | pages = <nowiki>{</nowiki>99--114<nowiki>}</nowiki>, |
publisher = <nowiki>{</nowiki>Springer<nowiki>}</nowiki>, |
publisher = <nowiki>{</nowiki>Springer<nowiki>}</nowiki>, |
||
series = <nowiki>{</nowiki>Lecture Notes in Computer Science<nowiki>}</nowiki>, |
series = <nowiki>{</nowiki>Lecture Notes in Computer Science<nowiki>}</nowiki>, |
||
− | volume = <nowiki>{</nowiki> |
+ | volume = <nowiki>{</nowiki>10805<nowiki>}</nowiki>, |
address = <nowiki>{</nowiki>Thessaloniki, Greece<nowiki>}</nowiki>, |
address = <nowiki>{</nowiki>Thessaloniki, Greece<nowiki>}</nowiki>, |
||
abstract = <nowiki>{</nowiki>SAT solvers are now widely used to solve a large variety |
abstract = <nowiki>{</nowiki>SAT solvers are now widely used to solve a large variety |
||
Line 46: | Line 48: | ||
experiments on the benchmarks of last six SAT competitions |
experiments on the benchmarks of last six SAT competitions |
||
show that our approach is competitive with the best |
show that our approach is competitive with the best |
||
− | state-of-the-art static symmetry breaking solutions.<nowiki>}</nowiki> |
+ | state-of-the-art static symmetry breaking solutions.<nowiki>}</nowiki>, |
+ | doi = <nowiki>{</nowiki>10.1007/978-3-319-89960-2_6<nowiki>}</nowiki> |
||
<nowiki>}</nowiki> |
<nowiki>}</nowiki> |
||
Latest revision as of 19:07, 7 April 2023
- Authors
- Hakan Metin, Souheib Baarir, Maximilien Colange, Fabrice Kordon
- Where
- Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'18)
- Place
- Thessaloniki, Greece
- Type
- inproceedings
- Publisher
- Springer
- Projects
- Spot
- Date
- 2018-01-05
Abstract
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 avoids the main problem of the current static approaches: the prohibitive cost of the preprocessing phase. 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.
Documents
Bibtex (lrde.bib)
@InProceedings{ metin.18.tacas, author = {Hakan Metin and Souheib Baarir and Maximilien Colange and Fabrice Kordon}, title = {{CDCLSym}: Introducing Effective Symmetry Breaking in {SAT} Solving}, booktitle = {Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'18)}, year = 2018, month = apr, pages = {99--114}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {10805}, address = {Thessaloniki, Greece}, abstract = {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 avoids the main problem of the current static approaches: the prohibitive cost of the preprocessing phase. 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.}, doi = {10.1007/978-3-319-89960-2_6} }