I am a student starting an undergrad math project. I was instructed to read Donald Knuth's Fascicle 6: Satisfiability and come up with ideas for a project from this material.

enter image description here

I have 13 weeks to do the project.

I have carefully read the Example applications section of the book and over Christmas I managed to encode Conway's Game of Life into Boolean Logic and search for interesting seeds that evolve into predetermined patterns.

enter image description here

enter image description here

Today I am struggling to think of a research question (or project idea) involving this material that I can answer or complete under my time constraints.

I could provide encodings to Boolean Logic for every example application Knuth discusses.

I could translate all the applications in the Example applications section into python 3.

Here are the applications Knuth discusses in the Example Applications section. A recipe book for boolean encodings for these could be useful to future readers?

  1. The Waerden Function
  2. Exact covering
  3. Four Color Theorem
  4. Fault Testing
  5. Machine Learning
  6. Game of Life
  7. Mutual Exclusion
  8. Digital Tomography

Perhaps I could solve some new problem using a SAT solver?


Suggest an undergrad research project involving SAT solvers and Boolean encoding

Due to my inexperience I am struggling to come up with a decent research question.

I would love to add a tiny leaf to the tree of knowledge.

  • $\begingroup$ Welcome to Computer Science! Unfortunately, your question is probably not a good fit for the Stack Exchange format. We prefer questions that have objectively correct answers that will be useful both to the asker and others who have the same question in the future. What is or is not a suitable topic for study, projects or research is very much a matter of opinion and depends crucially on the interests and skills of the person who will be doing the work and the support that will be available to them. This is a question that you should be asking your professors. $\endgroup$ – D.W. Jan 14 at 17:09
  • 1
    $\begingroup$ Here's one idea for an advanced project: you could experiment with learning a finite automaton (DFA) that recognizes some given set of words -- see cs.stackexchange.com/q/109583/755, cstheory.stackexchange.com/q/29119/5038. I haven't been able to find anything in the literature that studies this, so if you learned something about the effectiveness and scalability of this approach (say, compared to some existing alternative) you'd be advancing knowledge. $\endgroup$ – D.W. Jan 14 at 17:15
  • $\begingroup$ @D.W. Thanks, that looks interesting. I will look into it. $\endgroup$ – Conor Cosnett Jan 14 at 22:09
  • 2
    $\begingroup$ There are many problems in discrete math that you might like, but it might be challenging to find a problem for which you can (easily) make a dent with SAT solvers. For example, have a look at snake-in-a-box or Ramsey numbers. $\endgroup$ – Juho Jan 17 at 19:04
  • $\begingroup$ @Juho, thank you I will have a look at both of those! $\endgroup$ – Conor Cosnett Jan 17 at 19:43

Your Answer

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

Browse other questions tagged or ask your own question.