TY - GEN
T1 - XOR Local Searchfor Boolean Brent Equations
AU - Nawrocki, Wojciech
AU - Liu, Zhenjun
AU - Fröhlich, Andreas
AU - Heule, Marijn
AU - Biere, Armin
PY - 2021/7
Y1 - 2021/7
N2 - 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.
AB - 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.
M3 - Conference proceedings
VL - volume 12831
T3 - Lecture Notes in Computer Science (LNCS)
SP - 417
EP - 435
BT - Proc. 24rd Intl. Conf. on Theory and Applications of Satisfiability Testing
PB - Springer
ER -