Simplify embeddability check implementation

[curtisbright]

I dislike how the embeddability check generates a string containing the embeddability constraints and then calls exec on the string.

It makes the code messy because you do string conversions all over the place and using exec is unnecessarily complex. It's better to just call directly call Z3 on the constraints -- I converted main.py so that you can see what I mean. However, because there could have been an error in the translation please double-check that all the embeddability constraints are specified correctly.

Also, you need to update the complex embeddability checker in the same way. It still uses the old nested cross product so that should be removed too.

[BrianLi009]

complex checker updated, not closing the issue just yet, still testing the new implementation

[BrianLi009]

reruning order 10 minimal unembeddable graph check to verify new implementation

[curtisbright]

The check should be much faster than it is currently; I noticed the following issues slowing it down:

• The degree constraint is checked after the enumeration instead of doing the enumeration on a smaller search space.
• Python and all the modules you are using are unloaded and reloaded on every single check.

[BrianLi009]

• The degree constraint is checked after the enumeration instead of doing the enumeration on a smaller search space.

Yes definitely, this can be done through additional encoding on degrees of vertices.

• Python and all the modules you are using are unloaded and reloaded on every single check.

Right now check_embedability.sh and generate_nonembed_sat.sh only calls Python once on the entire exhaust file, so I don't think all the modules are unloaded and reloaded on every single check, are you referring to something else?

[curtisbright]

Ok, I didn't see that the script had been updated recently because when I checked the bash script was calling Python in a loop. The complex embeddability script should be updated in the same way.

Yes, I suggest only enumerating the squarefree graphs with a minimum vertex degree of 2 before computing the minimal unembeddable subgraphs up to a given order - this should be faster as I mentioned before.

[BrianLi009]

Sounds good, I'm going to focus on the incremental cubing implemention first, will circle back to this.

[BrianLi009]

Update: currently, complex embedability check is fast for embeddable graph, but it is slow to determine unembedability. Experimenting with some potential optimizations.

[curtisbright]

I would not optimize fixing variables to zero (unless it is necessary) because fixing variables makes it easy to introduce a mistake; it is best if the code generating the constraints is as self-evident as possible.

The obvious next step is to determine exactly why the solver is so much slower, given the minimal unembeddable graphs of order 10 were previously be shown to be unembeddable easily. Worst case you just go back to those constraints, but you want the most self-evident form of those constraints ideally.

[BrianLi009]

The variable fixing technique was initially suggested, since if a vertex is orthogonal to a standard vector, we know that one of its coordinate must be 0. I experimented with it and it doesn't provide a great speedup, as I suspect it is fairly easy for Z3 to derive this by itself. I can remove it.

[curtisbright]

Yes, I believe we talked about this a while ago. They should be easy for the solver to derive, they make the code more complex, and it would be catastrophic if there was a typo, so from a cost-benefit perspective we are better off ignoring them.

[BrianLi009]

I've changed the encoding to be exactly the same as before, but it is still not outputting UNSAT. The only difference is that now we are using s.add interface in python, instead of writing the z3 script into a separate file and calling it.

Using s.add(), when we call cross_c, it create a very long expression of cross product. In comparison the old approach write to a stringIO file, and the cross_c function is called within the stringIO file.

I don't know if this is the cause, but it seems to be the only difference now.

[BrianLi009]

The unembeddable graphs are solvable now, though it took a few tries using different assignments. It's not as fast as the old implementation, but still shows good improvement compared to yesterday.

Let me do more experiments and come back with a more concrete conclusion.

[curtisbright]

I'm confused by your two messages from 5 hours ago; "it is still not outputting UNSAT" and "The unembeddable graphs are solvable now" seem contradictory. Generating a python script in a string and then calling exec should not be faster; I can't think of why you would want to do that at all.

[BrianLi009]

Initially the script "is not outputting UNSAT", upon some modifications, the script can decide that unembeddable graphs are UNSAT. The runtime is comparable with the old script. Apologies for the confusion, will push the changes once it's cleaned.

[curtisbright]

Initially the script "is not outputting UNSAT", upon some modifications, the script can decide that unembeddable graphs are UNSAT. The runtime is comparable with the old script. Apologies for the confusion, will push the changes once it's cleaned.

What modifications were necessary?

[BrianLi009]

Yesterday, if v_i is adjacent to v_j and v_k, we encode (V_i = V_j cross V_k) or (V_i = V_j cross V_k), and V_i lives on the northern hemisphere.

Now, if v_i is adjacent to v_j and v_k, we directly assign the variable V_i to be V_j cross V_k, and remove the northerm hemisphere condition. (As long as the non-colinear condition is enforced)

This new encoding is consistent to what we initially had couple months back, as well as Bas and Sander's approach using nested for loop.

We will update the paper accordingly to be consistent with our encoding, I will work on that tomorrow. Thank you, Curtis!