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.

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

[https://link.springer.com/chapter/10.1007/978-3-032-15981-6_9 Michael Leuschel: Using Prolog to Translate Set Theory and B to SAT. PADL 2025: 143-160.]

Zenodo archive of benchmarks.