I'm new to z3 and trying to use it to solve logic puzzles. The puzzle type I'm working on, Skyscrapers, includes given constraints on the number of times that a new maximum value is found while reading a series of integers.
For example, if the constraint given was 3, then the series [2,3,1,5,4] would satisfy the constraint as we'd detect the maximums '2', '3', '5'.
I've implemented a recursive solution, but the rule does not apply correctly and the resulting solutions are invalid.
for (int i = 0; i < clues.Length; ++i)
{
IntExpr clue = c.MkInt(clues[i].count);
IntExpr[] orderedCells = GetCells(clues[i].x, clues[i].y, clues[i].direction, cells, size);
IntExpr numCells = c.MkInt(orderedCells.Length);
ArrayExpr localCells = c.MkArrayConst(string.Format("clue_{0}", i), c.MkIntSort(), c.MkIntSort());
for (int j = 0; j < orderedCells.Length; ++j)
{
c.MkStore(localCells, c.MkInt(j), orderedCells[j]);
}
// numSeen counter_i(index, localMax)
FuncDecl counter = c.MkFuncDecl(String.Format("counter_{0}", i), new Sort[] { c.MkIntSort(), c.MkIntSort()}, c.MkIntSort());
IntExpr index = c.MkIntConst(String.Format("index_{0}", i));
IntExpr localMax = c.MkIntConst(String.Format("localMax_{0}", i));
s.Assert(c.MkForall(new Expr[] { index, localMax }, c.MkImplies(
c.MkAnd(c.MkAnd(index >= 0, index < numCells), c.MkAnd(localMax >= 0, localMax <= numCells)), c.MkEq(c.MkApp(counter, index, localMax),
c.MkITE(c.MkOr(c.MkGe(index, numCells), c.MkLt(index, c.MkInt(0))),
c.MkInt(0),
c.MkITE(c.MkOr(c.MkEq(localMax, c.MkInt(0)), (IntExpr)localCells[index] >= localMax),
1 + (IntExpr)c.MkApp(counter, index + 1, (IntExpr)localCells[index]),
c.MkApp(counter, index + 1, localMax)))))));
s.Assert(c.MkEq(clue, c.MkApp(counter, c.MkInt(0), c.MkInt(0))));
Or as an example of how the first assertion is stored:
(forall ((index_3 Int) (localMax_3 Int))
(let ((a!1 (ite (or (= localMax_3 0) (>= (select clue_3 index_3) localMax_3))
(+ 1 (counter_3 (+ index_3 1) (select clue_3 index_3)))
(counter_3 (+ index_3 1) localMax_3))))
(let ((a!2 (= (counter_3 index_3 localMax_3)
(ite (or (>= index_3 5) (< index_3 0)) 0 a!1))))
(=> (and (>= index_3 0) (< index_3 5) (>= localMax_3 0) (<= localMax_3 5))
a!2))))
From reading questions here, I get the sense that defining functions via Assert should work. However, I didn't see any examples where the function had two arguments. Any ideas what is going wrong? I realize that I could define all primitive assertions and avoid recursion, but I want a general solver not dependent on the size of the puzzle.
Stack-overflow works the best if you post entire code segments that can be independently run to debug. Unfortunately posting chosen parts makes it really difficult for people to understand what might be the problem.
Having said that, I wonder why you are coding this in C/C# to start with? Programming z3 using these lower level interfaces, while certainly possible, is a terrible idea unless you've some other integration requirement. For personal projects and learning purposes, it's much better to use a higher level API. The API you are using is extremely low-level and you end up dealing with API-centric issues instead of your original problem.
Based on this, I'd strongly recommend using a higher-level API, such as from Python or Haskell. (There are bindings available in many languages; but I think Python and Haskell ones are the easiest to use. But of course, this is my personal bias.)
The "skyscraper" constraint can easily be coded in the Python API as follows:
from z3 import *
def skyscraper(clue, xs):
# If list is empty, clue has to be 0
if not xs:
return clue == 0;
# Otherwise count the visible ones:
visible = 1 # First one is always visible!
curMax = xs[0]
for i in xs[1:]:
visible = visible + If(i > curMax, 1, 0)
curMax = If(i > curMax, i, curMax)
# Clue must equal number of visibles
return clue == visible
To use this, let's create a row of skyscrapers. We'll make the size based on a constant you can set, which I'll call N:
s = Solver()
N = 5 # configure size
row = [Int("v%d" % i) for i in range(N)]
# Make sure row is distinct and each element is between 1-N
s.add(Distinct(row))
for i in row:
s.add(And(1 <= i, i <= N))
# Add the clue, let's say we want 3 for this row:
s.add(skyscraper(3, row))
# solve
if s.check() == sat:
m = s.model()
print([m[i] for i in row])
else:
print("Not satisfiable")
When I run this, I get:
[3, 1, 2, 4, 5]
which indeed has 3 skyscrapers visible.
To solve the entire grid, you'd create NxN variables and add all the skyscraper assertions for all rows/columns. This is a bit of coding, but you can see that it's quite high-level and a lot easier to use than the C-encoding you're attempting.
For reference, here's the same problem encoded using the Haskell SBV library, which is built on top of z3:
import Data.SBV
skyscraper :: SInteger -> [SInteger] -> SBool
skyscraper clue [] = clue .== 0
skyscraper clue (x:xs) = clue .== visible xs x 1
where visible [] _ sofar = sofar
visible (x:xs) curMax sofar = ite (x .> curMax)
(visible xs x (1+sofar))
(visible xs curMax sofar)
row :: Integer -> Integer -> IO SatResult
row clue n = sat $ do xs <- mapM (const free_) [1..n]
constrain $ distinct xs
constrain $ sAll (`inRange` (1, literal n)) xs
constrain $ skyscraper (literal clue) xs
Note that this is even shorter than the Python encoding (about 15 lines of code, as opposed to Python's 30 or so), and if you're familiar with Haskell quite a natural description of the problem without getting lost in low-level details. When I run this, I get:
*Main> row 3 5
Satisfiable. Model:
s0 = 1 :: Integer
s1 = 4 :: Integer
s2 = 5 :: Integer
s3 = 3 :: Integer
s4 = 2 :: Integer
which tells me the heights should be 1 4 5 3 2, again giving a row with 3 visible skyscrapers.
Once you're familiar with the Python/Haskell APIs and have a good idea on how to solve your problem, you can code it in C# if you like. I'd advise against it though, unless you've a really good reason to do so. Sticking the Python or Haskell is your best bet not to get lost in the details of the API.