CODEWITHSUNDEEP
z3
darthbob88
darthbob88

Reputation: 91

Z3 Towers Solver

I'm trying to write a solver using Z3's .NET library for the Towers puzzle format. Adding the constraints for "every row and column has a distinct permutation of 1-5" is simple enough, especially cribbing from the Sudoku solver provided as an example for Z3. However, I am stuck on the "Exactly X towers are visible from the left/right/top/bottom of each row/column" constraint, and specifically checking how many towers are visible from each point. It should be as simple as

int tallestSoFar = 0;
int towersSoFar = 0;
int[] section = X[i];
for (int ii = 0; ii < section.Length; ii++)
{
    if (section[ii] > tallestSoFar)
    {
        tallestSoFar = section[ii];
        towersSoFar++;
    }
}

However, this does not work when X and section are made of IntExpr's rather than actual ints. How would I express this in the syntax Z3 would recognize?

Upvotes: 1

Views: 75

Answers (1)

alias
alias

Reputation: 30525

The main issue here is that if of the host language only works on "concrete" values. Instead, you'll have to use the if-then-else construct to represent a symbolic choice. In different bindings, this is called a different name. In z3py, it's If. In .NET it's MkITE. Each host language will have a slightly different name/calling convention.

The idea is to represent the conditional using a symbolic expression. (For instance, tallestSoFar will have to be an expression built out of MkITE nodes that represent its value.

As a side note, I'd recommend using a much friendlier API, like that of z3py for instance, instead of .NET, especially if you're new to Z3. Symbolic programming can be tricky, and API's in C/C++/.NET tend to be a lot more verbose and harder to use correctly. Prefer z3py, or perhaps a binding in some other high-level language like Haskell or Racket. APIs from .NET/C/C++ should only be preferred if you really have to program in those languages for some other reason, as they tend to be much lower level.

Upvotes: 2

Related Questions