CosySEL: Improving SAT Solving Using Local Symmetries
Many satisfiability problems exhibit symmetry properties. Thus, the development of symmetry exploitation techniques seems a natural way to try to improve the efficiency of solvers by preventing them from exploring isomorphic parts of the search space. These techniques can be classified into two categories: dynamic and static symmetry breaking. Static approaches have often appeared to be more effective than dynamic ones. But although these approaches can be considered as complementary, very few works have tried to combine them. In this paper, we present a new tool, CosySEL, that implements a composition of the static Effective Symmetry Breaking Predicates (ESBP) technique with the dynamic Symmetric Explanation Learning (SEL). ESBP exploits symmetries to prune the search tree and SEL uses symmetries to speed up the tree traversal. These two accelerations are complementary and their combination was made possible by the introduction of local symmetries. We conduct our experiments on instances issued from the last ten SAT competitions and the results show that our tool outperforms the existing tools on highly symmetrical problems.
Mon 16 JanDisplayed time zone: Eastern Time (US & Canada) change
16:00 - 18:00 | |||
16:00 30mTalk | Solving Constrained Horn Clauses over Algebraic Data Types VMCAI Lucas Zavalia Florida State University Tallahassee, Lidiia Chernigovskaia , Grigory Fedyukovich Florida State University | ||
16:30 30mTalk | Satisfiability Modulo Custom Theories in Z3 (Tool Paper) VMCAI | ||
17:00 30mTalk | CosySEL: Improving SAT Solving Using Local Symmetries VMCAI |