sCOP: a SAT-based CP System

Overview of sCOP

sCOP is a Sat-based COnstraint Programming system written in Scala 2.12.
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 sCOP.
- Encoding of extensional constraints is different between the two systems.
- Some of encoding heuristics is different between the two systems.
- Log encoding (from CSP into SAT) is implemented by using the BDD encoding (Een and Sorensson).
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.

sCOP: SAT-based Constraint Programming System. Takehide Soh, Daniel Le Berre, Mutsunori Banbara, Naoyuki Tamura. In Proceedings of XCSP3 Competition 2018, 93–94, 2018. http://www.cril.univ-artois.fr/XCSP18/files/XCSP3_2018_Proceedings.pdf

scop.jar
- It is a fat jar containing all resources except SAT solvers
  - XCSP3-Java-Tools (https://github.com/xcsp3team/XCSP3-Java-Tools)
  - scop
  - scala standard libraries (version 2.12)
scop.sh
- It is a wrapper for XCSP18.
MapleCOMSPS
- It is an award-winning SAT solver downloaded from the following URL.
- Note that there are several versions of MapleCOMSPS in the official web page. The one we used is only available in the exactly the same URL as follows.
- Note again, we used “simp” not “core”.
- https://sites.google.com/a/gsd.uwaterloo.ca/maplesat/MapleCOMSPS.zip
glucose-syrup
- It is an award-winning SAT solver downloaded from the following URL.
- Note that we used the version submitted to the SAT competition 2017.
- https://baldur.iti.kit.edu/sat-competition-2017/solvers/parallel/syrup.zip

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

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

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

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

cd DIR/syrup
make clean
make

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

(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

(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

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