Introduction

Motivation

• Human solutions to constraint problems works when there are a reasonable number of constraints. Humans can solve Sudoku problems, but sometimes it takes a while. That’s a maximum of 81 variables and roughly 27 constraints (there are 9 rows, 9 columns, and 9 squares).

• Industrial problems like checking to see if a printed circuit board correctly implements a specification will take a lot more variables. (The technique could even be applied to the internal “wiring” of a single semiconductor chip.)

• Repetitive solution of similar problems is also unattractive to humans.

Application: Firewall Updating

Microsoft Azure updating firewall rules with a simplified version. It would be a costly disaster if the new “simplified” version of the firewall rules blocked something required for the business to function, so they used a logic solver to prove that the old and new firewalls let through exactly the same packets.

A writeup of the firewall rule-replacement process is posted online in a Microsoft Research blog entry by Andrew Helwer.