Constraint solving for Alloy

• From Alloy to SAT
• The SAT problem
  • Encoding Sudoku as SAT
• SAT solving
• Translating Alloy goals into SAT

Readings

• Writings on the board:
  • Board for the overview of leveraging SAT solvers
  • Board for SAT solving
  • Board for Alloy encoding into SAT
• State-of-the-art SAT solving:
  • Slides by João Marques-Silva and Mikoláš Janota
  • Slides by Marijn Heule
• Automating Alloy solving, paper by Daniel Jackson.

Recommended readings

• Kodkod: A Relational Model Finder
• Alloy*: A General-Purpose Higher-Order Relational Constraint Solver

From Alloy to SAT

Determining if an Alloy specification has an instance (within the given bounds) that respects the established restrictions is encoded as a SAT problem (see below). If this problem is satisfiable, the corresponding solution is decoded into an Alloy instance and exhibited.

Similarly, checking whether an assertion is valid (i.e., it is always true within the given bounds) is also encoded negatively as a SAT problem. If this SAT problem is unsatisfiable, then the assertion is valid (within the bounds), otherwise the problem is satisfiable and the corresponding is decoded into an Alloy counterexample.

The SAT problem

The satisfiability problem consists of determining if there exists a valuation to the variables of a propositional formula (i.e., a formula in propositional logic).

Encoding Sudoku as SAT

• Sudoku as a SAT problem

• SAT problems can be solved with SAT solvers

• Solving via Minisat: This requires having Minisat installed. This python program takes a file containing a sudoku problem like

0 0 5 0 0 0 8 7 0
3 0 6 0 7 8 4 0 0
8 7 0 0 0 0 0 9 6
0 1 0 3 0 7 0 0 0
0 2 0 0 0 0 0 3 0
0 0 0 8 0 6 0 1 0
5 3 0 0 0 0 0 4 9
0 0 9 4 5 0 1 0 7
0 8 7 0 0 0 3 0 0

and producing another file containing the problem solved (where each 0 will be replaced by a number between 1 and 9 following the sudoku rules).

SAT solving

SAT solvers implement the conflict-driven clause learning (CDCL) calculus.

Translating Alloy goals into SAT

Let’s consider a specification of a pigeonhole problem in Alloy. First we model that we may have pigeons, holes and pigeons may be nested in holes.

sig Hole {}
sig Pigeon {nest : set Hole}

The property to be respected is that no pigeon is in more than one hole and every pigeon is in a hole. The above formulation is not enough to guarantee this. We can check it:

check {no h : Hole | #nest.h > 1 and no p : Pigeon | no p.nest }

This check will produce counterexamples. To avoid this we can force the restrictions that every pigeon is exactly one hole and that all holes have at most one pigeon:

fact {
  all p : Pigeon | one p.nest
  all h : Hole | lone nest.h
}

Now every execution of a run command will yield an instance respecting the pigeonhole principle. All is well, but how are such instances found? We know that Alloy solving is done via SAT solving. But how? What is the propositional formula that is fed into a SAT solver and whose satisfying assignment can be mapped back into the Alloy instance being searched?

Now consider adding this predicate

pred hasSubNest {
  some subNest : Pigeon -> Hole | some subNest and #subNest < #nest and subNest in nest
}

run {hasSubNest} for exactly 3 Hole, exactly 3 Pigeon