CNF
As of version 1.16.0 ProB can directly open .cnf files encoding SAT problems in conjunctive normal form. These files get translated into a B model, which has an accompanying custom graph visualisation showing the variable incidence graph (VIG) and a VisB visualisation of the clauses showing the satisfying literals. The backend is also set to use B2SAT. The B translation also contains an encoding of the clauses.
VisB can be used to visualise the solutions. You can use the console to examine the clauses and the solution.
Take the following file KnightsKnavesSat.cnf encoding a Knights and Knaves puzzle by Raymond Smullyan:
c CanonicalCNFFormat p cnf 3 5 -1 -2 -3 0 1 2 0 1 3 0 1 -2 0 -1 2 0
Knights always tell the truth and knaves always lie and we know that A,B and C are either knights or knaves and we are given this information:
- 1: A says: “B is a knave or C is a knave”
- 2: B says “A is a knight”
What are A, B and C?
When loading the above file with ProB a new B machine KnightsKnavesSat.mch is automatically generated:
/*@generated */
MACHINE KnightsKnavesSat
/* Generated on 24/7/2026 at 14:32 using ProB version 1.16.0-nightly */
CONSTANTS
x
DEFINITIONS
SET_PREF_SOLVER_FOR_PROPERTIES == "sat";
SET_PREF_DOT_ENGINE == "fdp";
CUSTOM_GRAPH_NODES1 == {(i).i:1..3|rec(`id`:i, label:```x${i}```,color:IF x(i)=TRUE THEN "olivedrab2" ELSE "tomato" END,shape:"box",style:"rounded",penwidth:2)};
CUSTOM_GRAPH_NODES2 == {(c).c:1..5|rec(`id`:c+3, label:```Clause ${c}```,color:"blue",shape:"box")};
CUSTOM_GRAPH_EDGES1 == {(ci,c,i).ci|->c:CLAUSES & i:ran(c) & i>0 |rec(color:"black", style:IF x(i)=TRUE THEN "solid" ELSE "dotted" END, label:"+", dir:"none", penwidth:2,from:i,to:ci+3)};
CUSTOM_GRAPH_EDGES2 == {(ci,c,i).ci|->c:CLAUSES & i:ran(c) & i<0 |rec(color:"purple", style:IF x(-i)=FALSE THEN "solid" ELSE "dotted" END, label:"-", dir:"none", penwidth:2,from:-i,to:ci+3)};
WIDTH==6; HEIGHT==4;WIDTH1==WIDTH+1;HEIGHT1==HEIGHT+1;
MAXCLAUSESIZE == max({(i).i:dom(CLAUSES)|size(CLAUSES(i))});
VISB_SVG_BOX == rec(width:WIDTH1*MAXCLAUSESIZE,height:1+HEIGHT1*size(CLAUSES));
VISB_SVG_OBJECTS == {(i,j) . i:dom(CLAUSES) & j:dom(CLAUSES(i)) | VISB_LITERAL(i,j,CLAUSES(i)(j))};
VISB_LITERAL(i,j,lit) == (rec(svg_class:"rect",rx:1,width:WIDTH,height:HEIGHT,
fill:IF lit<0 & x(-lit)=FALSE THEN "lightgreen" ELSIF lit>0 & x(lit)=TRUE THEN "palegreen" ELSE "burlywood" END,
stroke:"gray", hovers:rec(stroke:"black"), `stroke-width`:0.2,
x:(j-1)*WIDTH1, y:1+(i-1)*HEIGHT1,title:```Literal ${j} in clause ${i}```),
rec(svg_class:"text",x:(j-1)*WIDTH1+WIDTH/2,y:1+(i-1)*HEIGHT1+HEIGHT/2,
`font-size`:2.0,`alignment-baseline`:"middle",`text-anchor`:"middle",
text:IF lit<0 THEN ```¬x${-lit}``` ELSE ```x${lit}```END));
CLAUSES ==
[
[-1,-2,-3],
[1,2],
[1,3],
[1,-2],
[-1,2]
]
PROPERTIES
x:1..3 --> BOOL &
(x(1) = FALSE or x(2) = FALSE or x(3) = FALSE) &
(x(1) = TRUE or x(2) = TRUE ) &
(x(1) = TRUE or x(3) = TRUE ) &
(x(1) = TRUE or x(2) = FALSE) &
(x(1) = FALSE or x(2) = TRUE )
END
END
After loading ProB finds a single solution with x(1)=x(2)=TRUE and x(3)=FALSE, i.e., A and B are knights and C is a knave.
The custom graph visualisation of the variable incidence graph (File:KnightsKnavesCustomGraph.pdf) can be seen here:
The VisB visualisation of the clauses can be seen here:
