Prototype it with SAT!

For years, SAT solvers have been the plaything of academics, and ignored by industry. However nerdy and pointless *boolean satisfiability* sounds, they are actually really useful! Whether you're a tiny startup trying to scrape together an MVP, or an established behemoth churning out prototypes, SAT can help. Boolean Satisfiaiblity (aka SAT) is a simple problem: given a boolean formula, how can we set the inputs to make it output true? However, SAT's not as simple as it sounds - in fact it's one of the hardest problems in computer science. Given a problem that is easier than SAT (i.e. most of them), we can rewrite it as a SAT problem and use a SAT solver to find the solution. This session introduces the concept of SAT solvers and how they can be used. Then, we'll explore how you can quickly prototype your ideas with a SAT solver. In a live demonstration, we'll program a SAT solver to create meal plans. We'll refine that solution incrementally, adding more inputs for the solver to consider to improve the output quality. Comparing our SAT-based approach to a one-off algorithm, we'll discuss the pros and cons of each. There are trade-offs in terms of development speed, execution speed, result quality, and the long-term cost of maintenance and improvement. By thinking about those trade-offs, you'll gain an intuitive understanding of when a SAT solver is the right tool for the job. The session will leave you with an understanding of what SAT solvers are, when they are useful, and how to start prototyping your ideas with SAT.