Reducing SAT to Max2XOR
Carlos Ans\'otegui, Jordi Levy
TL;DR
This paper introduces a method to translate SAT problems into Max2XOR constraints and proposes new resolution rules for solving Max2XOR, enhancing reasoning techniques for parity constraints.
Contribution
It presents a novel gadget for converting SAT clauses into Max2XOR constraints and introduces new resolution rules for Max2XOR problems.
Findings
Effective translation of SAT to Max2XOR constraints
New resolution rules improve Max2XOR problem-solving
Potential for more efficient reasoning with XOR constraints
Abstract
Representing some problems with XOR clauses (parity constraints) can allow to apply more efficient reasoning techniques. In this paper, we present a gadget for translating SAT clauses into Max2XOR constraints, i.e., XOR clauses of at most 2 variables equal to zero or to one. Additionally, we present new resolution rules for the Max2XOR problem which asks for which is the maximum number of constraints that can be satisfied from a set of 2XOR equations.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsConstraint Satisfaction and Optimization · Formal Methods in Verification · Logic, Reasoning, and Knowledge