0

I try to place N rectangular blocsks with different sizes into a grid, by formulating it as a CSP propblem. The blocks should not overlap with each other, they can touch on the edges, and there can be empty places. For example place 4 rectangular blocks of size 2x2 into a 8x8 grid. (Vary the number of blocks, the sizes of the blocks, and the size of the grid.) I know the formula as enter image description here

I try to write a program or script generates the formula but I am confused too much I cant write in an SMT syntax. İf anyone helps I aprreciate too much. Thank you.

Promise89
  • 33
  • 6
  • 1
    To solve your (homework?) problem: Choose your decision variables; define type and value range per variable; define the constraints; translate your model into [SMT2](https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf) syntax; run Z3. If you get stuck on your way, post a specific question. – Axel Kemper Dec 05 '21 at 22:15
  • 1
    You might benefit from the [MinizInc model](https://stackoverflow.com/a/66918091/1911064) I posted for a [related question](https://stackoverflow.com/questions/66899645/finding-all-the-combinations-n-rectangles-inside-the-square/66918091#66918091). – Axel Kemper Dec 05 '21 at 22:43

1 Answers1

1

You should be specific about what you tried and what didn't work. If your problem is with syntax, then here's something to get you started:

(set-option :produce-models true)

(declare-fun xi () Int)
(declare-fun wi () Int)
(declare-fun xj () Int)
(declare-fun wj () Int)

(assert (or (<= (+ xi wi) xj)
            (<= (+ xj wj) xi)))

The above encodes the first two disjuncts in your formula. You can add the other variables and assert all the other conditions as required.

alias
  • 28,120
  • 2
  • 23
  • 40