| Line 29: | Line 29: | ||
The valid settings are: prob (the default), kodkod, z3, z3cns, z3axm, cdclt, sat, sat-z3. | The valid settings are: prob (the default), kodkod, z3, z3cns, z3axm, cdclt, sat, sat-z3. | ||
The last two will use B2SAT. | The last two will use B2SAT, {\tt sat} with Glucose as SAT solver and {\tt sat-z3} with Z3 as SAT solver. | ||
Here is an example using this preference: | Here is an example using this preference: | ||
| Line 36: | Line 36: | ||
// Dominating set example: | // Dominating set example: | ||
// place ice cream vans so that every house (node) is at most one block away from a van | // 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 | // a version which can be solved by B2SAT | ||
DEFINITIONS | DEFINITIONS | ||
N == 24; | N == 24; | ||
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.
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, {\tt sat} with Glucose as SAT solver and {\tt 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: