Name
Abstract | ||
|---|---|---|
Combining clausal and XOR reasoning has been studied for almost two decades, in particular in the context of CDCL and look-ahead, but not in classical local search. To stimulate research in this direction, we propose to standardize a hybrid format, called XNF, which allows both clauses and XORs. We implemented a tool to extract XOR constraints from a CNF, simplify them, and produce an XNF formula. The usefulness of XNF formulas is demonstrated by focusing on the impact of combined clausal and XOR reasoning on local search. Native support for XOR facilitates satisfying any falsified long XOR using a single flip, similarly to satisfying a falsified clause. When combined with XOR-based heuristics, local search performance is significantly improved on matrix multiplication challenges which are hard for CDCL. |
Year | DOI | Venue |
|---|---|---|
2021 | 10.1007/978-3-030-80223-3_29 | THEORY AND APPLICATIONS OF SATISFIABILITY TESTING, SAT 2021 |
DocType | Volume | ISSN |
Conference | 12831 | 0302-9743 |
Citations | PageRank | References |
0 | 0.34 | 0 |
Authors | ||
5 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Wojciech Nawrocki | 1 | 0 | 0.34 |
| Zhenjun Liu | 2 | 0 | 0.34 |
| Andreas Fröhlich | 3 | 61 | 5.39 |
| Marijn J. H. Heule | 4 | 3 | 1.39 |
| Armin Biere | 5 | 4106 | 245.11 |