Inverse Intersections for Boolean Satisfiability Problems
Paul W. Homer
TL;DR
This paper introduces a matrix-based method for solving SAT problems by computing inverse intersections, providing a complete set of solutions with a novel algorithm.
Contribution
It presents a new matrix representation for SAT problems and an algorithm using clause inverses to efficiently find satisfying assignments.
Findings
Matrix representation captures all solutions
Inverse-based algorithm finds solutions efficiently
Solution set size is exponential in matrix dimensions
Abstract
Boolean Satisfiability (SAT) problems are expressed as mathematical formulas. This paper presents a matrix representation for these SAT problems. It shows how to use this matrix representation to get the full set of valid satisfying variable assignments. It proves that this is the set of answers for the given problem and is exponential in size relative to the matrix. It presents a simple algorithm that utilizes the inverse of each clause to find an intersection for the matrix. This gives a satisfying variable assignment.
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
TopicsFormal Methods in Verification · Advanced Algebra and Logic · Machine Learning and Algorithms