Home | Examples | Documents | Advanced Usage | Tutorial | Apps |
日本語ページはこちら.
This page details Scarab, a prototyping tool for developing SAT-based systems. Features of Scarab are follows:
import jp.kobe_u.scarab._ ; import dsl._ var n: Int = 5 for (i <- 1 to n; j <- 1 to n) int('x(i,j),1,n) for (i <- 1 to n) { add(alldiff((1 to n).map(j => 'x(i,j)))) add(alldiff((1 to n).map(j => 'x(j,i)))) add(alldiff((1 to n).map(j => 'x(j,(i+j-1)%n+1)))) add(alldiff((1 to n).map(j => 'x(j,(i+(j-1)*(n-1))%n+1))))} if (find) println(solution.intMap)
scala -cp scarab<$version>.jar pls.sc
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! | |
Numberjack | Constraint Programming System in Python |
SCP | Constraint Programming in Scala using Z3 |
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 |
Created: 2019-02-11 月 15:01