Proc. 24rd Intl. Conf. on Theory and Applications of Satisfiability Testing
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.