B2ASP - Revision history

Michael Leuschel at 13:43, 19 March 2026

2026-03-19T13:43:13Z

← Older revision		Revision as of 13:43, 19 March 2026
Line 1:		Line 1:
	The current versions of ProB can make use the clingo ASP solver as an alternate way of solving constraints.		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.		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 ==		== Using B2ASP ==

Michael Leuschel at 13:39, 19 March 2026

2026-03-19T13:39:20Z

← Older revision		Revision as of 13:39, 19 March 2026
Line 113:		Line 113:
	== Article ==		== Article ==

	[https://link.springer.com/chapter/10.1007/978-3-032-15981-6_9 Michael Leuschel:		The following [https://link.springer.com/chapter/10.1007/978-3-032-15981-6_9 article] describes this backend in more detail:
	Using Prolog to Translate Set Theory and B to SAT. PADL 2025: 143-160.]		* Michael Leuschel: Using Prolog to Translate Set Theory and B to SAT. PADL 2025: 143-160.
			The article also has an accompanying [https://zenodo.org/records/17660151 Zenodo archive of benchmarks].
	[https://zenodo.org/records/17660151 Zenodo archive of benchmarks].

Michael Leuschel: /* B2ASP (clingo) for PROPERTIES */

2026-03-19T13:38:25Z

B2ASP (clingo) for PROPERTIES

@@ Line 32: / Line 32: @@
    SET_PREF_SOLVER_FOR_PROPERTIES == "clingo";
 </pre>
 == Article ==

Michael Leuschel at 13:35, 19 March 2026

2026-03-19T13:35:40Z

← Older revision		Revision as of 13:35, 19 March 2026
Line 2:		Line 2:
	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.		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:		B2ASP solving consists of the following phases:
Line 9:		Line 10:
	* a Prolog back-translation of ASP models to B values.		* a Prolog back-translation of ASP models to B values.

	The backend can be used in the REPL of probcli:		=== B2ASP (clingo) in the REPL ===

			The backend can be used in the REPL of [[Using_the_Command-Line_Version_of_ProB\|probcli]]:

	<pre>		<pre>
Line 21:		Line 24:
	The command <tt>:clingo-double-check</tt> double checks the solution using ProB's default solver.		The command <tt>:clingo-double-check</tt> 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.		You can also use SOLVER_FOR_PROPERTIES preference to specify clingo as backend for solving PROPERTIES (aka axioms) of B models.

Michael Leuschel at 13:34, 19 March 2026

2026-03-19T13:34:03Z

← Older revision		Revision as of 13:34, 19 March 2026
Line 21:		Line 21:
	The command <tt>:clingo-double-check</tt> double checks the solution using ProB's default solver.		The command <tt>:clingo-double-check</tt> 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.		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:
			<pre>
			SET_PREF_SOLVER_FOR_PROPERTIES == "clingo";
			</pre>

			== Article ==
	## Article ##

	[https://link.springer.com/chapter/10.1007/978-3-032-15981-6_9 Michael Leuschel:		[https://link.springer.com/chapter/10.1007/978-3-032-15981-6_9 Michael Leuschel:

Michael Leuschel: Created page with "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 c..."

2026-03-19T13:31:37Z

Created page with "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 c..."

New page

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:

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

You can use <tt>:clingo #file=FILE</tt> to solve a predicate from a file.
The command <tt>:clingo-double-check</tt> 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.

## 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.]

[https://zenodo.org/records/17660151 Zenodo archive of benchmarks].