Wojciech Nawrocki, Zhenjun Liu, Andreas Fröhlich, Marijn Heule, Armin Biere,
"XOR Local Searchfor Boolean Brent Equations"
: Proc. 24rd Intl. Conf. on Theory and Applications of Satisfiability Testing, Serie Lecture Notes in Computer Science (LNCS), Vol. volume 12831, Springer, Seite(n) 417-435, 7-2021
Original Titel:
XOR Local Searchfor Boolean Brent Equations
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. 24rd Intl. Conf. on Theory and Applications of Satisfiability Testing
Original Kurzfassung:
Combining clausal and XOR reasoning has been studied foralmost two decades, in particular in the context of CDCL and look-ahead, but not in classical local search. To stimulate research in thisdirection, we propose to standardize a hybrid format, called XNF, whichallows both clauses and XORs. We implemented a tool to extract XORconstraints from a CNF, simplify them, and produce an XNF formula.The usefulness of XNF formulas is demonstrated by focusing on theimpact of combined clausal and XOR reasoning on local search. Nativesupport for XOR facilitates satisfying any falsified long XOR using asingle flip, similarly to satisfying a falsified clause. When combined withXOR-based heuristics, local search performance is significantly improvedon matrix multiplication challenges which are hard for CDCL.
Forschungs-