Scarab: Documents

• Scarab DSL can concisely write constraint modelings with the help of rich functionalities of Scala.
• The expressiveness of Scarab will be also shown by some prototyping examples for an optimization version of Square Packing.

• Scarab can be efficient in the sense that it uses an optimized version of the order encoding which an award-winning CSP solver Sugar adopted.
• Scarab also can utilize current state-of-the-art SAT techniques.

• Scarab allows a programmer to customize his/her own constraints and to customize the search strategies.
• Scarab itself can be also customizable since it is 500 lines (800 lines in version 1.0.4) long without any comments.
• In particular, our core part of order encoding module is only 25 lines long.

• The current version of Scarab adopts Sat4j as the back-end SAT solver.
• The combination of Scarab and Sat4j makes it possible to develop portable SAT-based systems that run on any platform supporting Java.

• The process starts with a user program, which will first define Scarab objects
• Those definitions are typically done by the followng Scala program:

val csp = new CSP()
val satSolver = new Sat4j()
val encoder = new OrderEncoder(csp,satSolver)
val solver = new Solver(csp,satSolver,encoder)

• Each line creates a new CSP object (csp), SAT solver object (satSolver), Encoder object (encoder), and Solver object (solver), which are shown in the above figure.
• Initially, of course, the CSP object has nothing and the next task is to add contents of it
• To do that, Scarab DSL provides the following methods for constructing a CSP:
  • int, bool for adding integer variables and Boolean variables to the CSP object.
  • add for adding constraints to the CSP object.
  • The syntax of constraints in Scarab is given below in this page.

• A CSP object consists of the followings, which will be defined in the user program:
  1. integer variables
  2. Boolean variables
  3. domain function of integer variables
  4. constraints
• All objects above are defined as var objects. Totally, CSP is a mutable object.

• It encodes each element of a given CSP according to SAT encoding method (currently, order encoding)
• Simultaneously, encoded SAT clauses are passed to Sat4j solver on memory
• It also decodes assignments of SAT variables to assiginments of CSP variables by using a mapping object.

• Scarab provides an interface to Sat4j and can directly call it.
• Thus, we can use Sat4j without generating CNF files, invoking outer processes, and parsing output logs.
• After solving problems, we can obtain assignments of SAT variables

T  ::= V | -T | T + Int | T + T | T - Int | T - T | T * Int | Sum(V, ...) | Sum(Seq(V, ...))  
V  ::= Var(String, String, ...) | V(Any, ...)
C  ::= B | T op T | !C | C && C | C || C | alldiff(Seq(T, ...)) |  
      And(C, ...) | And(Seq(C, ...)) | Or(C, ...) | Or(Seq(C, ...))
op ::= <= | < | => | > | === | !==
B  ::= Bool(String, String, ...) | B(Any, ...)