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.

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.

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.

==

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";

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.