Questions/Suggestions

[joachim-j]

Hi,

I read a little through the code and it seems like you're translating everything into CNF, which means you're potentially not using some of the more cutting edge solving techniques.

There are alternative approaches where, instead of writing a script in e.g., Python to generate clauses, you write your "constraints" into a language that is specifically designed to express those constraints. These languages are generally based on 1st order predicate logic. An example of such a system can be found here: https://potassco.org/doc/start/. There's other systems available, but not all of them are well-documented, since systems like these generally find no use outside of academia (yet :p).

The long and short of it is: there are constraint solving systems that allow you to write your clauses using not only boolean variables, but also constructs of other kinds, like numerical variables. The hope is that for the majority of the problems that deal with problems that feature numerical concepts (like grid coordinates), this extra expressive power allows a reasoner to more efficiently go through the search space.

If my assumptions above are correct, I'd take some time and prototype an encoding that could serve as an alternative. My time to spend on this is limited, so if you feel like me pointing you towards resources where you can learn this yourselves is more efficient, I could do that as well.

[R-O-C-K-E-T]

Sounds interesting, if the problem could be encoded at a higher level efficiently that would be sweet. I'm not sure that a more numerical perspective will help all that much. For your grid coordinate example, if a region of the balancer has been proven that it is or isn't something. To apply this result to other areas of the balancer the solver would need to consider how the position in the balancer has affected the region (e.g. if the region is at the top, then belts can't go up). No global translational symmetry.

The interchange problem might be a good benchmark to use. If you can get some reasonable performance, then I'll definitely switch over.

[joachim-j]

The interchange problem, where is that encoded? Are you talking about clauses added by def prevent_intersection(self, edge_mode: EdgeModeType):? I couldn't really understand those. Would it be possible for you to explain the constraint(s) expressed by those clauses?

[R-O-C-K-E-T]

The interchange problem is to design a belt layout that takes input from two different balancers with n outputs and mixes them together. Such that a final layer of splitters can be added to form a combined balancer with 2n outputs. In other words the first column should have two different types of belts where the types are initially grouped and the last column the belt types should be alternating. interchange.py currently solves this problem. No splitters are required, which should simplify the implementation.

As for how prevent_intersection works.

# For all orthogonal directions
for direction in range(4):
    # For all pairs of tiles where tile_a points into tile_b along direction
    for tile_a, tile_b in self.iterate_tile_lines(direction_to_vec(direction), 2, edge_mode): 
        # Ignore any tile that goes past the end of the balancer
        if tile_b is None: 
            continue
                
        # Adds a requirement that tile_a outputs along direction if and only if tile_b inputs along that same direction, hence these two literals are the same
        self.clauses += literals_same(tile_a.output_direction[direction], tile_b.input_direction[direction])

        # Annoying edge case specific to splitters that have an unused output so don't output along direction, but do prevent some belt combinations
        # How it works: it just lists the incompatible belt arrangements ¯\_(ツ)_/¯
        ...

[joachim-j]

What is the memory footprint of the interchange problem associated with N=8 (like in your picture)? Are we talking about more than a gigabyte?
I'm writing up a small program as an initial test. Would be good to have an idea of the memory (and runtime?) footprint of some of the 'smaller' problems to see where I land.

Edit: is there documentation on how to generate a picture based on the solver output?

[R-O-C-K-E-T]

I've provided a table of values below (options used are --alternating --underground-length 8). Memory and time values are self reported by kissat. The remaining time+space should be linear in the size of the input is fairly negligible for larger problems. For bigger N's the solver has taken too long to find the largest UNSAT width, so they are not included.

N	Width	Memory (MB)	Time (s)	Answer
8	7	6	0.02	SAT
8	6	6	0.10	UNSAT
9	7	6	0.15	SAT
9	6	6	0.13	UNSAT
10	8	6	0.10	SAT
10	7	14	23.58	UNSAT
11	8	7	0.18	SAT
11	7	18	36.50	UNSAT
12	9	12	5.33	SAT
13	9	21	25.34	SAT
14	10	17	16.85	SAT
15	10	26	72.68	SAT

Without any optimisation tricks.

N	Width	Memory (MB)	Time (s)	Answer
8	7	6	0.10	SAT
8	6	6	0.15	UNSAT
9	7	6	0.02	SAT
9	6	6	0.17	UNSAT
10	8	6	0.27	SAT
10	7	19	55.02	UNSAT
11	8	6	0.05	SAT
11	7	21	90.39	UNSAT
12	9	9	5.25	SAT
13	9	8	3.15	SAT
14	10	10	7.42	SAT
15	10	22	95.30	SAT

As for generating gifs, pipe the output into render.py with the option --export-format gif (e.g. python interchange.py ... | python render.py --export-format gif), then press "s". FFmpeg needs to be installed. FFmpeg doesn't make the best gifs, so using the default mp4 export then converting them into gifs, with a tool such as gifski, produces nicer results.

[joachim-j]

I'd have to look at the internals of render.py to understand what the output format of kissat is? If I want to emulate with my own solver, I'd have to transform my output into the same one as kissat if I want to re-use render.py.

The runs with my initial encoding are much worse than the performance you posted. I haven't taken all measures in optimizing yet, but the prospect is not hopeful at this moment. I'm mentioning this specifically because I don't think I will be able to give an update improving my performance soon. So this issue may be dormant for a while.

[R-O-C-K-E-T]

Great that you got it to work. I do have some spare time, so I may be able to help out some.

The format is not too complex. I've linked an image of a belt layout with its corresponding encoding, which should cover the format features.

[
    [
        {
           // Tile to draw may be any of the tiles declared in tile.py
            "tile": {
                "type": "belt", // Discriminator attribute
                "input_direction": 0,
                "output_direction": 0
            },
           // Underground connections that can be shown with the --show-underground option, may be omitted
            "underground": [
                false,
                false,
                false,
                false
            ],
            // Index of the tile's colour, may be omitted
            "colour": 0,
            // Index of the tile's underground connection colours, may be omitted
            "colour_ux": 0, 
            "colour_uy": 0,
            // Other properties can be added and displayed with the show-raw option (e.g. --show-raw some_prop)
           "some_prop": 7
        },
        {
            "tile": {
                "type": "belt",
                "input_direction": 0,
                "output_direction": 1
            },
           "colour": 0
        }
    ],
    [
        {
            "tile": {
                "type": "underground_belt",
                "direction": 0,
                "is_input": true
            },
           "colour": 1
        },
        {
            "tile": {
                "type": "empty"
            },
           "colour": 0
        }
    ]
]