[2N5-OS-17b] OS-17 (2)

[2N5-OS-17b-01] SAT solving algorithm for compressed large-scaled instances

〇Yuma HAYASE¹, Hidetomo NABESHIMA¹ (1. University of Yamanashi)

Keywords:SAT solver, SAT based CSP solver, SAT instances, Compression of SAT instances

Translating a constraint satisfaction problem (CSP) to a propositional satisfiability testing (SAT) is one of promising approaches for solving CSP. In fact, SAT based CSP solvers have won the XCSP2018 and 2019 competitions. SAT instances generated from CSPs sometimes consist of a huge number of clauses and such instances are difficult to solve due to the shortage of memory, and even if memory is sufficient, it takes a long time to process a huge number of clauses. On the other hand, SAT instances mechanically generated by SAT based CSP solvers are very structured. In this work, we propose two techniques: (1) a compression technique of a SAT instance to variants of run-length encoding and (2) direct processing techniques the compressed clauses without decompression. The experimental results show that our proposed techniques can solve large-scaled SAT instances more than a normal solver.