sCOP: a SAT-based CP System

Overview of sCOP

  • sCOP is a Sat-based COnstraint Programming system written in Scala 2.12.
  • It works as follows:
    1. encode a XCSP3 file into a DIMACS CNF file.
    2. launch a SAT solver to solve the encoded CNF file.
    3. the output of the SAT solver is decoded to the solution of the XCSP3 instance.

Reference

Download

Components of sCOP

Requirements for sCOP

  • Java 8
  • (Note) Scala 2.12 is not necessary since scop.jar is a fat jar containing scala standard libraries.

Notations in the following

DIR It stands for the directory where you place scop-for-xcsp18
TMPDIR It is the directory where the solver is allowed to
  create temporary files
BENCHNAME It stands for the name of the instance file (with its extension)
NBCORE It stands for the number of processing units allocated to the solver

How to install

  • We need to compile 2 SAT solvers respectively for sequential solving and parallel solving.

(Sequential CSP) MapleCOMSPS

cd DIR/MapleCOMSPS
export MROOT=`pwd`
cd simp
make clean
make r

(Parallel CSP) glucose-syrup

cd DIR/syrup
make clean
make

lzma (os command)

  • we assume an os command ’lzma’ is available for decomposing *.xml.lzma instances.
  • If there is not ’lzma’ then simply give *.xml to scop.

How to run

  • (NOTE) we here assume 11GB/22GB can be allocated to JVM. This is XCSP18 competition setting but larger heap size is better in principal.
  • assume that the following command is executed in the ’scop-for-xcsp18’ directory.
  • (Sequential CSP) with -both option

    DIR/scop.sh 11g DIR/scop.jar -both DIR/MapleCOMSPS/simp/minisat_release default TMPDIR BENCHNAME
    
  • (Sequential CSP) with -order option

    DIR/scop.sh 11g DIR/scop.jar -order DIR/MapleCOMSPS/simp/minisat_release default TMPDIR BENCHNAME
    
  • (Parallel CSP) with -both option

    DIR/scop.sh 22g DIR/scop.jar -both DIR/syrup/bin/glucose-syrup -model:-nthreads=NBCORE:-maxmemory=20000 TMPDIR BENCHNAME
    
  • (Parallel CSP) with -order option

    DIR/scop.sh 22g DIR/scop.jar -order DIR/syrup/bin/glucose-syrup -model:-nthreads=NBCORE:-maxmemory=20000 TMPDIR BENCHNAME
    

Example (please refer http://xcsp.org/series for example XCSP3 instances)

  • (NOTE) we here assume 11GB/24GB can be allocated to JVM. This is XCSP18 competition setting but if possible larger size is preferred.
  • assume that the following command is executed in the ’scop-for-xcsp18’ directory.
./scop.sh 16g scop.jar -both MapleCOMSPS/simp/minisat_release default /tmp examples/AllInterval-007.xml

License

Contact

Links for Related Tool

Scarab a very light weight SAT-based CP System
Diet-Sugar A SAT-based CSP Solver Equipped with Hybrid Encoding integrating Order and Log Encodings
Sat4j SAT solver in Java, which Scarab adopts!
Sugar SAT-based CSP Solver using order encoding.
Copris Copris is a constraint programming DSL embedded in Scala.
  It is also developed by our team!
NACRE NACRE (Nogood And Clause Reasoning Engine) is a constraint solver written in C++.
Numberjack Constraint Programming System in Python
scalasmt SMT in Scala using Z3
OscaR OR in Scala
JaCoP Constraint programming in Java and Scala
Choco Constraint programming in Java
JSR 331 Java Specification Requests: Constraint Programming API
BEE a compiler which enables to encode finite domain constraint problems to CNF.
meSAT Multiple Encodings of CSP to SAT

Author: Takehide Soh

Created: 2018-10-15 月 17:15

Validate