We found a match
Your institution may have access to this item. Find your institution then sign in to continue.
- Title
Fractional Encoding of At-Most-K Constraints on SAT.
- Authors
Yonekura, Miki; Nishimura, Shunji
- Abstract
The satisfiability problem (SAT) in propositional logic determines if there is an assignment of values that makes a given propositional formula true. Recently, fast SAT solvers have been developed, and SAT encoding research has gained attention. This enables various real-world problems to be transformed into SAT and solved, realizing a solution to the original problems. We propose a new encoding method, Fractional Encoding, which focuses on the At-Most-K constraints—a bottleneck of computational complexity—and reduces the scale of logical expressions by dividing target variables. Furthermore, we confirm that Fractional Encoding outperforms existing methods in terms of the number of generated clauses and required auxiliary variables. Hence, it enables the efficient solving of real-world problems like planning and hardware verification.
- Subjects
SATISFIABILITY (Computer science); INTEGRATED circuit verification; ENCODING; PROPOSITION (Logic); COMPUTATIONAL complexity; PROBLEM solving
- Publication
Electronics (2079-9292), 2023, Vol 12, Issue 15, p3211
- ISSN
2079-9292
- Publication type
Article
- DOI
10.3390/electronics12153211