Get@FileNameJoin[{DirectoryName@NotebookFileName[],"Z3Interop.wl"}]

$ContextPath=DeleteDuplicates@Append[$ContextPath,"Z3Interop`Nonogram`"];

Parse out the structure

Here follows some ghastly, though at least pure, XLSX-parsing code.

Clear[fixColour];
fixColour["FFFF0000"]=Red;
fixColour["FFFFFF00"]=Yellow;
fixColour["FFFFFFFF"]=Black;
fixColour["FF0070C0"]=Blue;
fixColour[x_]:=Throw[x];

extractSi[XMLElement["si",{},xs_List]]:=Select[
If[Length[#[[3]]]==1,{fixColour@"FFFFFFFF",First@Cases[#,XMLElement["t",_,{x_}]:>(FromDigits[#,10]&/@StringSplit[x]),All]},With[{style=Cases[#[[3,1]],XMLElement["rPr",{},{___,XMLElement["color",{"rgb"->r_},___],___}]:>r,All],text=Cases[#[[3,2]],XMLElement["t",_,{t_}]:>t,All]},{If[style==={},fixColour@"FFFFFFFF",Assert[Length@style]==1;fixColour@First@style],Assert[Length@text==1];FromDigits[#,10]&/@StringSplit[First@text]}]]&/@xs,Length@Last[#]>0&]

xlsx=FileNameJoin[{DirectoryName@NotebookFileName[],"nauseator.xlsx"}];

extracted=extractSi/@Import[xlsx,{"ZIP","xl/sharedStrings.xml"}][[2,3]];

colStringIds=1+FromDigits[#,10]&@*First@*Last@*First@*Last/@Most@Rest[Import[xlsx,{"ZIP","xl/worksheets/sheet1.xml"}][[2]][[3,5,3,1,3]]]

rowStringIds=1+FromDigits[#[[3,1,3,1,3,1]],10]&/@Import[xlsx,{"ZIP","xl/worksheets/sheet1.xml"}][[2]][[3,5,3,2;;-2]]

rowsIn=Map[Reverse,Flatten[#,1]&/@Map[Thread,Extract[extracted,List/@rowStringIds],{2}],{2}];

colsIn=Map[Reverse,Flatten[#,1]&/@Map[Thread,Extract[extracted,List/@colStringIds],{2}],{2}];

For example:

colsIn[[1]]

Construct a system of constraints

For more detail, see the z3interop.nb example notebook.

Define an arbitrary mapping of colours to numbers, so that we can represent the problem in integers.

mapping=With[{colours=Union@Cases[rowsIn,_?ColorQ,All]},Assert[FreeQ[colours,White]];MapIndexed[#1->First@#2&,Append[colours,White]]]

constrainedColumns:=MapIndexed[gapsToConstraints[#1,First@#2,Length@rowsIn,colGap]&,colsIn];

constrainedRows:=MapIndexed[gapsToConstraints[#1,First@#2,Length@colsIn,rowGap]&,rowsIn];

additionalConstraints:=constrainedCells[rowGap,colGap,cell,rowsIn,colsIn,constrainedRows,constrainedColumns,mapping];

Form the program:

vars:=DeleteDuplicates@Flatten@{Cases[{constrainedCells,constrainedColumns,constrainedRows},colGap[_,_],Infinity],Cases[{additionalConstraints,constrainedColumns,constrainedRows},rowGap[_,_],Infinity],Cases[{additionalConstraints,constrainedColumns,constrainedRows},cell[_,_],Infinity]};

constraints:=Assertion/@Flatten[{additionalConstraints,constrainedColumns,constrainedRows}]

declared:=Declare[#,Integer]&/@vars

symbols={colGap->"colGap",rowGap->"rowGap",cell->"cell"};

program:=Riffle[toString[symbols,#]&/@Flatten@{declared,constraints,CheckSat,GetModel},"\n"]//StringJoin;

This is an example where the built-in Z3Interop `toString` does not know how to perform addition. Teach it:

toString[symbols_,a_+b_]:=StringJoin["(+ ",toString[symbols,a]," ",toString[symbols,b],")"]

Write and run the program:

s=OpenWrite[FormatType->OutputForm,PageWidth->Infinity];Write[s,program];outputLocation=Close[s]

output=RunProcess[{"z3",outputLocation},ProcessEnvironment-><|"PATH"->"/usr/local/bin"|>]["StandardOutput"];

StringCases[output,RegularExpression["(un)?sat"]]

Parse out the solution (sorry about the rendered PDF being so blurry):

answer=getDefinitions[symbols,output];

Table[cell[i,j],{i,1,Length@rowsIn},{j,1,Length@colsIn}]/.answer/.(Reverse/@mapping)//Image