Skip to content

Carlos Iriarte

This page shows a small proof of concept using an SAT solver.

From wikipedia:

In logic and computer science, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated SATISFIABILITY or SAT) is the problem of determining if there exists an interpretation that satisfies a given Boolean formula. In other words, it asks whether the variables of a given Boolean formula can be consistently replaced by the values TRUE or FALSE in such a way that the formula evaluates to TRUE. If this is the case, the formula is called satisfiable. On the other hand, if no such assignment exists, the function expressed by the formula is FALSE for all possible variable assignments and the formula is unsatisfiable. For example, the formula "a AND NOT b" is satisfiable because one can find the values a = TRUE and b = FALSE, which make (a AND NOT b) = TRUE. In contrast, "a AND NOT a" is unsatisfiable.

After researching this topic to see if there's a way we can use this powerful tool to help during the COVID-19 pandemic by alleviating the burden of scheduling a team of nurses.

I've setup an artificial test case below, and a calendar with a possible solution. This calendar shows the shifts that were requested in blue, and the shifts that were not requested in orange:


References
  • Patrick Doherty and Jonas Kvarnström, Handbook of Knowledge Representation, 2008.
  • ORTools by Google