Skip to content

Fun-sCOP

  • Joint work by Takehide Soh, Daniel Le Berre, Mutsunori Banbara, and Naoyuki Tamura.
  • Fun-sCOP won several prises in recent XCSP3 competitions.
    • 2023 Main CSP🥈
    • 2022 Main CSP🥈
    • 2019 Main CSP🥈
    • 2018 Main CSP🥇 Parallel CSP🥇

Overview

  • Fun-sCOP is a Sat-based COnstraint Programming system written in Scala 2.12.
  • Fun-sCOP aims to be a re-implementation of Sugar (Tamura et al.) written in Java. Many things are imported from Sugar (software design, normalization, and encoding). Currently, main differences are as follows:
    • XCSP3 instances is accepted as input in Fun-sCOP.
    • Hybrid Encoding integrating the order and log encoding is used in Fun-sCOP.
  • 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

Setting for XCSP3 competitions

  • This Fun-sCOP solver will enter the main CSP track (sequential) with 2 solver configurations.

    • 1st one uses a SAT solver "kissat"
    • 2nd one uses a SAT solver "GlueMiniSat 2.2.10 193 Order Encoding Adapted Version"

  • Notations in the following

NAME Description
DIR It stands for the directory where you place scop
TMPDIR It is the directory where the solver is allowed to create temprary files
BENCHNAME It stands for the name of the instance file (with its extension)

Requirements for Fun-sCOP

  • Java 8
  • SAT Solvers and their requirements

How to install SAT solvers

You can use install-sat-solvers.sh. Or please read the following instructions.

  • (for Sequential CSP 1) Kissat 
cd DIR/kissat
./configure && make
  • (for Sequential CSP 2) GlueMiniSat 2.2.10 193 Order Encoding Adapted Version
    • Final products we need is the executable simp/glueminisat-simp-2.2.10-193oa-n-release
    • Its installation command is as follows:
cd DIR/glueminisat-2.2.10-193oa-n/simp/
make clean
make r
  • lzma (os command)
    • we assume an OS command 'lzma' is available for decomposing *.xml.lzma instances.
      • lzma is called from Fun-sCOP.
    • If there is no 'lzma' then simply give *.xml to Fun-sCOP.

How to run

  • (NOTE) Fun-sCOP performs better the larger the memory.

  • We here assume 32GB can be allocated to JVM. But larger heap size is better if possible.

    • assume that the following command is executed in the 'scop-for-xcsp23' directory.
    • (Sequential CSP 1) using Kissat DIR/scop.sh 11g DIR/scop.jar -hybrid DIR/kissat/build/kissat default TMPDIR BENCHNAME
    • (Sequential CSP 2) using GlueMiniSat with -order option DIR/scop.sh 11g DIR/scop.jar -order DIR/glueminisat-2.2.10-193oa-n/simp/glueminisat-simp-2.2.10-193oa-n-release -model:-verb=3:-elim-cl=5000000:-native-oa TMPDIR BENCHNAME

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

    • We here assume 32GB can be allocated to JVM. But larger heap size is better if possible.
    • assume that the following command is executed in the 'scop-for-xcsp23' directory.
./scop.sh 11g scop.jar -hybrid kissat/build/kissat default /tmp examples/AllInterval-007.xml

Contact

  • Scarab
    • a very light weight SAT-based CP system
  • Sat4j
    • SAT solver in Java.
  • 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
  • OscaR
    • OR in Scala
  • JaCoP
    • Constraint programming in Java and Scala
  • Choco
    • Constraint programming in Java
  • JSR 331
    • Java Specification Requests: Constraint Programming API
  • Picat
  • BEE
  • meSAT