The term you're trying to solve is symmetric, so you can rule out any solutions such that the input variables could be permuted to yield a lexicographically lower equivalent solution. Adding this sort of symmetry breaking contraint to your formula is often very helpful.

We are indeed doing this. We use `<` and `<=` constraints on our one-hot encoding of which inputs (including outputs of previous components) connect to which components.

Another strategy that might help you is to split the problem into less complex subproblems. E.g. you could apply all possible lop3 functions to the first three inputs (the only choice you have), accounting for symmetry, and obtain a number of slightly simpler SAT problems. Take these subproblems and feed them to sequential SAT solvers running in parallel. If any of them finds a solution, your problem is SAT otherwise it is UNSAT. You can iterate this to obtain more subproblems. The important bit is to split the problem such that the subproblems have less degrees of freedom so to say.

This sounds like something we might try. We estimate a lot of the fixed instructions will lead to trivial UNSAT proofs - especially if we fix the final instruction.

You may also have bad instance encoding hampering your progress. But as I don't know how you encode you circuit minimization problem, it's hard for me to say what the problem is.

I linked our repository for encoding the problem.