Theory and Practice of SAT and Combinatorial Solving

How hard is it to figure out if there is a way to make a set of logical statements true at the same time by choosing appropriate truth values for their variables? This satisfiability problem is of immense importance both theoretically and practically, and lies right at the heart of mathematics and computer science. On the one hand, today so-called Boolean satisfiability (SAT) solvers are routinely and successfully used to solve large-scale real-world formulas in a wide range of application areas (such as hardware and software verification, electronic design automation, artificial intelligence research, cryptography, bioinformatics, operations research, and sometimes even pure mathematics). On the other hand, this problem is believed to be intractable in general --- though proving that this is so is so is one of the famous million dollar Clay Millennium Problems (the P vs. NP problem) --- and there are tiny formulas for which even the very best SAT solvers today fail miserably.

Topics: Boolean satisfiability (SAT)