[1E2-OS-3a] AI における離散構造処理と制約充足(1)

[1E2-OS-3a-03] A SAT-based CSP Solver sCOP and its Results on 2018 XCSP3 Competition

〇Takehide Soh¹, Daniel Le Berre^3,4, Mutsunori Banbara², Naoyuki Tamura¹ (1. Kobe University, 2. Nagoya University, 3. CRIL-CNRS, UMR 8188, 4. Université d'Artois)

Keywords:SAT, CSP, SAT Solver, CSP Solver

Constraint Satisfaction Problem (CSP) is the combinatorial problem of
finding a variable assignment which satisfies all given constraints
over finite domains. CSP has a wide range of applications in the
research domains of Artificial Intelligence and Operations
Research. XCSP3 is one of the major constraint languages that can
describe CSPs. More than 23,000 instances over 105 series are
available in the XCSP3 database. In 2018, the international XCSP3
competition was held and 18 solvers participated.

This paper describes the under development CSP solver sCOP and its
results on the 2018 XCSP3 competition. sCOP is a SAT-based solver
which encodes CSPs into SAT problems and finds a solution using SAT
solvers. Currently, sCOP equips the order and log encodings, and uses
off-the-shelves backend SAT solvers. We registered sCOP to two
competition tracks CSP-Standard-Sequential and CSP-Standard-Parallel
of the 2018 XCSP3 competition and won both tracks.