Import the Z3Interop package.

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

Set up the problem: Sudoku

A sudoku problem has 81 integer variables.

vars=Flatten@Table[a[i,j],{i,1,9},{j,1,9}];

Some of those variables have known values.

input=Partition[FromDigits/@Characters["008007060000609500000000031900005008702000405600800002140000000006401000050900100"],9];

known:=Cases[Flatten[Thread/@Thread[input==Table[a[i,j],{i,1,9},{j,1,9}]]],Equal[i_Integer?(#>0&), a[_,_]]]

All of those variables are between 1 and 9.

bounded=Flatten[{0<#,#<10}&/@vars];

Each row must contain the numbers 1 through 9 at least once, and likewise for each column.

rows=Flatten[Function[{x},Or@@@Table[a[i,#]==x&/@Range[1,9],{i,1,9}]]/@Range[1,9]];
cols=Flatten[Function[{x},Or@@@Table[a[#,i]==x&/@Range[1,9],{i,1,9}]]/@Range[1,9]];

Each 3x3 box must contain the numbers 1 through 9 at least once.

boxesF[row_,col_]:=Function[{x},Or@@Flatten@Table[a[i,j]==x,{i,row,row+2},{j,col,col+2}]]/@Range[9]

boxes=Flatten@Table[boxesF[i,j],{i,1,9,3},{j,1,9,3}];

The above constraints are the complete set of assertions we make about the variables.

constraints:=Assertion/@Flatten[{bounded,known,rows,cols,boxes}];

Declare the variables to be integers.

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

Construct the program by concatenating the variable declaration section, constraint section, command to check satisfiability, and command to obtain a satisfaction.

symbols={a->"a"};

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

Run Z3

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

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

Is that instance satisfied?

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

Parse the output

Obtain a model in which the constraints are satisfied, by parsing Z3’s output.

answer=getDefinitions[symbols,output];

Table[a[i,j],{i,1,9},{j,1,9}]/.answer//Grid

Set up the problem: Nonogram

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

Suppose we have as input a collection of row and column data. We will allow for multiple colours, although in this example the only colour is black.

rowsIn={{{1,Black},{3,Black}},{{2,Black},{1,Black}},{{3,Black},{1,Black}},{{1,Black}},{{1,Black}}};
colsIn={{{4,Black}},{{2,Black}},{{1,Black},{1,Black},{1,Black}},{{1,Black}},{{3,Black}}};

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

The constraints on a row are of the following form.
Suppose the input is the following:

col={{4,},{2,},{2,},{5,},{1,},{4,},{4,},{12,}};

Find the positions of colour changes x1,x2,x3,x4,… such that:
1<=x1
x1+4<=x2
x2+2<=x3
x3+2<x4
x4+5<=x5
x5+1<x6
x6+4<x7
x7+4<=x8
x8+12<=#rows

We represent this as the list of left-hand sides (x1+4, x2+2, …, x8+12), right-hand sides (x2, x3, …, x9), and operations (<=, <=, <, …), then prepend the first line and append the last.

gapsToConstraints[col,1,60,colGap]

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

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

And tie together the row and column constraints.
The cell at index {row, column} is of colour colsIn[[column, i, 2]] if colGap[column, i] <= row < colGap[column, i]+colsIn[[column,i,1]], and of colour white otherwise.
Similarly for the rows.

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:

answer=getDefinitions[symbols,output];

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