B2ASP

The current versions of ProB can make use the clingo ASP solver as an alternate way of solving constraints. This backend translates a subset of B formulas to SAT by encoding the formulas in ASP (Answer Set Programming) first and then using clingo to translate this to SAT and solve it.

Limitations:

• it can only translate first-order values (no sets of sets, no higher-order relations or functions)
• it cannot yet deal with nested existential quantifiers inside universal quantifiers

In contrast to the Kodkod backend, B2ASP can deal with arbitrary n-ary relations (and not just binary ones) and there are no issues with integer overflows.

Using B2ASP

B2ASP solving consists of the following phases:

• a CLP(FD) based bounds analysis to infer finite bounds for all variables,
• a translation of set theory and B to ASP programs (aka Horn clauses),
• using clingo to translate and solve ASP programs via SAT solving,
• a Prolog back-translation of ASP models to B values.

B2ASP (clingo) in the REPL

The backend can be used in the REPL of probcli:

>>> :clingo  pq = 1..2 /\ {2,4}
PREDICATE is TRUE
Solution: 
       pq = {2}

You can use :clingo #file=FILE to solve a predicate from a file. The command :clingo-double-check double checks the solution using ProB's default solver.

B2ASP (clingo) for PROPERTIES

You can also use SOLVER_FOR_PROPERTIES preference to specify clingo as backend for solving PROPERTIES (aka axioms) of B models. For example, you can put this into your DEFINITIONS section for this:

  SET_PREF_SOLVER_FOR_PROPERTIES == "clingo";

Here is an example using this preference to compute a dominating set of a graph:

MACHINE IceCream_Clingo
// Dominating set example:
// place ice cream vans so that every house (node) is at most one block away from a van
DEFINITIONS
  N == 24;
  CUSTOM_GRAPH == rec(layout:"dot", rankdir:"TB",
                     nodes: {j•j∈NODES |
                               rec(value:j, style:"filled",
                                fillcolor:IF ice(j)=TRUE THEN "mistyrose" ELSE "white" END
                                  )},
                     edges: rec(color:"gray", arrowhead:"odot",
                              arrowtail:"odot", dir:"both",
                              label:"edge",
                              edges: edge)
                    );
  bi_edge == (edge ∪ edge⁻¹);

  SET_PREF_SOLVER_FOR_PROPERTIES == "clingo";

  VISB_SVG_FILE == "IceCream.svg";
  VISB_SVG_UPDATES == {n • n∈NODES |
                        rec(`id`:n, fill: IF ice(n)=TRUE THEN "red" ELSE "LightBlue" END)}
SETS
  NODES = {n1,n2,n3,n4,n5,n6,n7,n8,n9,n10,
           n11,n12,n13,n14,n15,n16,n17,n18,n19,n20,n21,n22,n23,n24}
CONSTANTS edge, ice
PROPERTIES
 edge∈ NODES ↔ NODES ∧
 edge = { n1↦n2, n1↦n4,
          n2↦n3,
          n3↦n4, n3↦n5, n3↦n7,
          n4↦n7,
          n5↦n6, n5↦n9,
          n6↦n7, n6↦n8,
          n7↦n8,
          n8↦n10, n8↦n13,
          n9↦n10, n9↦n11, n9↦n12,
          n11↦n12, n11↦n14,
          n12↦n13,
          n13↦n16,
          n14↦n15, n14↦n17,
          n15↦n16, n15↦n17, n15↦n18, n15↦n21,
          n16↦n18, n16↦n19,
          n17↦n19,
          n18↦n19, n18↦n20, n18↦n21,
          n19↦n20, n19↦n21,
          n20↦n21, n20↦n22,
          n21↦n22, n21↦n23, n21↦n24,
          n22↦n23, n21↦n24,
          n23↦n24
          } ∧
 ice ∈ NODES→ BOOL ∧
 ∀x.(x∈NODES ⇒
      (ice(x)=TRUE or
        TRUE ∈ ice[edge[{x}] ∪ edge⁻¹[{x}]]
       )
    )

 ∧ card({x|x∈NODES ∧ ice(x)=TRUE})≤6
 /* minimal solution requires 6 vans */


OPERATIONS
  v <-- NrVans = BEGIN v := card(ice⁻¹[{TRUE}]) END;
  xx <-- Get(yy) = PRE yy∈NODES ∧ {CUSTOM_GRAPH} = ∅ THEN xx:= ice(yy) END;
  v <-- Vans = BEGIN v:= ice⁻¹[{TRUE}] END
END

Here is the graphical rendering of a solution using the custom graph definition above:

Article

The following article describes this backend in more detail:

• Michael Leuschel: Using Prolog to Translate Set Theory and B to SAT. PADL 2025: 143-160.

The article also has an accompanying Zenodo archive of benchmarks.