I want to generate a bunch of graphs of about 100 nodes, where each node is a categorial variable. I want the graphs to satisfy complex properties, like, "if a node of type A is connected to a node of type B, that node of type B should also be either connected to both a node of type C and a node of type D, or should be connected to a node of type E" and "no nodes of type F and G can be connected to the same node." How do I go about generating such structures? I was thinking of using an SMT solver, but even then I'm not exactly sure how to proceed. For instance, is there a way to do it using only BitVectors?


I would use a SAT solver. Use one boolean variable per edge to encode whether that edge is present or not. Encode the type of a node via a one-hot encoding ($k$ variables per node, where $k$ is the number of possible types). Then each constraint you mention should translate directly into a simple formula on a few of these boolean variables.

I like Z3 for ease of programming.

I see no reason nor benefit to using bitvectors or SMT; plain SAT should suffice.

| cite | improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.