First things first: What is SAT?
It uses something called a propositional formula, which you can imagine as a very big sudoku board. In every cell, you only have two options: only one or zero, standing for true or false. You also have the rules, or constraints, about how many zeros or ones can be in each row or column. Can you put in all the zeros and ones such that all those constraints are satisfied?
Despite its simplicity, this formulation is remarkably powerful. A wide variety of important problems, including hardware and software verification, scheduling, and even areas of pure mathematics, can be translated into SAT.
That just sounds like binary computation. How is SAT-solving different from anything else a digital computer does?
What SAT tools do is fundamentally different from ordinary computation. A standard program takes input and carries out a sequence of operations to produce output. A SAT tool is not computing with the zeros and ones. Instead, it is searching for a combination of them that satisfies all the constraints.
That makes it more like solving a puzzle: You explore possibilities, rule out large portions of the space using clever reasoning, and keep going until you either find a satisfying assignment or conclude that none exists.
What can generative AI add to the power of SAT solvers?
Once you’ve figured out the right representation of a problem, called the encoding, SAT tools are extremely powerful. One of my skills is that I’m really good at coming up with the right representation. I’ve really studied how these tools reason; I know what is required so that you can get everything out of them. But ideally, you wouldn’t need this knowledge. I would really like to take myself out of the equation — then the technology could really shine.
Source link
