This is a research heavy seminar with the aim to achieve publishable results. The goal is to design, implement, and evaluate an efficient generator for (scale-free) SAT instances with underlying geometry.
Although SAT is hard, it's easy in practice and there is an ongoing effort to understand why. Read about it here. When generating random instances you typically want two properties: a power-law distribution of the variable occurences and some kind of community structure or clustering. A generator should be efficient (meaning subquadratic) and have multiple input parameters to tune number of clauses, number of variables, power-law exponent, amount of clustering and clause degrees.
In the field of network science there exists a random graph model that fits our needs. It's called Hyperbolic Ranom Graphs and you can read about it here. We have an efficient implementation, but there are some steps missing to make it into a SAT generator. For example it's not designed to generate bipartite graphs (which SAT instances are). Also, the degrees of nodes can only by specified in expectation which could result in clauses with only one or two variables (which makes SAT too easy).
Enrollment is limited to 1-3 students.
Grading will include a presentation and a written report hopefully in the form of a publication.
