Presentation information

Organized Session

Organized Session » OS-17

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

Wed. Jun 10, 2020 3:50 PM - 5:30 PM Room N (jsai2020online-14)

宋 剛秀(神戸大学)、沖本 天太(神戸大学)

3:50 PM - 4:10 PM

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

〇Yuma HAYASE1, Hidetomo NABESHIMA1 (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.

Authentication for paper PDF access

A password is required to view paper PDFs. If you are a registered participant, please log on the site from Participant Log In.
You could view the PDF with entering the PDF viewing password bellow.