2:20 PM - 2:40 PM
[1E2-OS-3a-03] A SAT-based CSP Solver sCOP and its Results on 2018 XCSP3 Competition
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.
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.