![]() Since all sigils together exactly fill the frame, this is enough. The better idea was to say that every sigil was used at least once. But with 8×8 or so frames, the number of combinations simply explodes to above several million, which brings my harddrive size and z3 to an end. So if a sigil occupies 4 tiles, then every combination of 5 tiles needs to evaluate to false. First I thought I want to express that every sigil is used exactly once by excluding that for one sigil there are more fields assigned to it then the sigil contains parts. This can be achieved by asserting for each tile and each pair of different sigil (numbers), that not both of the two hold: ![]() In the SMT2 code it would look like (assert (or x_i_j_1 x_i_j_2. Let us go through them one by one: Every field has at least on sigil on it
0 Comments
Leave a Reply. |
Details
AuthorWrite something about yourself. No need to be fancy, just an overview. ArchivesCategories |