[2E4-OS-13c] AIと制約プログラミング(3/3)

[2E4-OS-13c-02] A fast unit propagation algorithm for compressed SAT instances

〇Yuma Hayase¹, Hidetomo Nabeshima¹, Xiao-Nan Lu¹ (1. Univarsity of Yamanashi)

Keywords:SAT solver, SAT-based Constraint Solver, SAT instances, compressed SAT instances

In this work, we propose a fast unit propagation algorithm for solving compressed SAT instances without decompression.Translating a constraint satisfaction problem (CSP) to a propositional satisfiability testing (SAT) is one of promising approaches for solving CSPs. We focus on the order encoding, which is a representative encoding translats CSP to SAT and widely used in many CSP solvers. SAT instances mechanically generated by such a encoding are very structured and can be highly compressed based on an approach similar to run-length encoding. We propose a fast unit propagation algorithm which can handle compressed clauses directly and show that it achieves the improvement both time and space complexity for solving large-scale SAT instances. The experimental results show that our solver can reduce both solving time and memory usage.