Line 114: | Line 114: | ||
Here is the graphical rendering of a solution using the custom graph definition above: | Here is the graphical rendering of a solution using the custom graph definition above: | ||
[[File:IceCream_Generic.png| | [[File:IceCream_Generic.png|500px|center]] | ||
By choosing "Show Source Code Coverage" in the Debug menu of ProB Tcl/Tk you can see which parts of the properties were translated to SAT (in green) and which were processed entirely by ProB (in red-orange): | By choosing "Show Source Code Coverage" in the Debug menu of ProB Tcl/Tk you can see which parts of the properties were translated to SAT (in green) and which were processed entirely by ProB (in red-orange): | ||
[[File:IceCreamCoverage.png|700px|center]] | [[File:IceCreamCoverage.png|700px|center]] |
The current versions of ProB can make use of the new B2SAT backend as an alternate way of solving constraints. It translates a subset of B formulas to SAT and for solving by an external SAT solver. The new backend interleaves low-level SAT solving with high-level constraint solving performed by the default solver of ProB.
B2SAT solving consists of the following phases:
The following four commands are now available in REPL of probcli (start with probcli --repl):
Here is a simple example:
>>> :sat f:1..n --> BOOL & n=3 & f(1)=TRUE & !i.(i:2..n => f(i) /= f(i-1)) PREDICATE is TRUE Solution: f = {(1|->TRUE),(2|->FALSE),(3|->TRUE)} & n = 3
The new preference SOLVER_FOR_PROPERTIES can be used to specify solver for PROPERTIES (axioms) when setting up constants. The valid settings are: prob (the default), kodkod, z3, z3cns, z3axm, cdclt, sat, sat-z3.
The last two will use B2SAT, sat with Glucose as SAT solver and sat-z3 with Z3 as SAT solver.
Here is an example using this preference:
MACHINE IceCream_Generic // Dominating set example: // place ice cream vans so that every house (node) is at most one block away from a van // a version which can be solved by B2SAT 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_SMT == TRUE; SET_PREF_TIME_OUT == 50000; SET_PREF_SOLVER_STRENGTH == 300; SET_PREF_SOLVER_FOR_PROPERTIES == "sat"; 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, vans, neighbours 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 & neighbours = %x.(x:NODES|bi_edge[{x}]) & !x.(x:NODES => (ice(x)=TRUE or #neighbour.(neighbour: neighbours(x) & ice(neighbour)=TRUE) ) ) & vans = card(ice~[{TRUE}]) & card({x|x:NODES & ice(x)=TRUE})<=6 /* minimal solution requires 6 vans */ OPERATIONS v <-- NrVans = BEGIN v := vans END; xx <-- Get(yy) = PRE yy:NODES 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:
By choosing "Show Source Code Coverage" in the Debug menu of ProB Tcl/Tk you can see which parts of the properties were translated to SAT (in green) and which were processed entirely by ProB (in red-orange):
On the console you can also see feedback about which parts were translated and which ones not.
The solve command in the ProB Jupyter kernel now supports sat and satz3 as solvers. They use B2SAT with Glucose and Z3 as SAT solvers respectively.
Here is a simple example to solve a constraint:
This shows how you can use cardinality constraints to iteratively find a minimal dominating set D of a graph g: