WEBVTT 00:00:00.000 --> 00:00:03.319 In 2016, a computer generated a mathematical 00:00:03.319 --> 00:00:08.000 proof that was 200 terabytes inside. 200 terabytes. 00:00:08.279 --> 00:00:11.980 Yeah. It was so massively complex, so unimaginably 00:00:11.980 --> 00:00:14.880 vast, that no human being could ever actually 00:00:14.880 --> 00:00:16.800 read the entire thing. Right. I mean, you'd need 00:00:16.800 --> 00:00:18.980 multiple lifetimes just to scroll through it. 00:00:19.140 --> 00:00:21.640 Exactly. But we know it's mathematically flawless. 00:00:22.280 --> 00:00:24.699 And the engine that built it, the software that 00:00:24.699 --> 00:00:27.239 basically ground through that monumental task, 00:00:27.699 --> 00:00:29.920 was really doing nothing more than answering 00:00:29.920 --> 00:00:32.399 millions upon millions of true or false questions. 00:00:32.640 --> 00:00:34.880 That's the wild part, yeah. Just true or false. 00:00:35.159 --> 00:00:37.750 Welcome to the Deep Dive. Today we are pulling 00:00:37.750 --> 00:00:40.630 from a really comprehensive Wikipedia article 00:00:40.630 --> 00:00:43.429 on something called a SAT solver. Which I know 00:00:43.429 --> 00:00:46.270 sounds like some obscure piece of computer science 00:00:46.270 --> 00:00:48.710 architecture. It does. But our mission for you 00:00:48.710 --> 00:00:52.570 today is to demystify this tool because it is 00:00:52.570 --> 00:00:55.130 actually this mind -bending mathematical engine 00:00:55.130 --> 00:00:58.189 capable of solving problems that theoretically 00:00:58.189 --> 00:01:00.049 should outlast the lifespan of the universe. 00:01:00.149 --> 00:01:02.170 They really should. It's fascinating. Okay, let's 00:01:02.170 --> 00:01:05.010 unpack this. We are talking about the Boolean 00:01:05.010 --> 00:01:09.200 Satisfiability Problem. or SAT. And for anyone 00:01:09.200 --> 00:01:11.480 listening who follows computer science, you already 00:01:11.480 --> 00:01:13.140 know the stakes here. Right. You already know 00:01:13.140 --> 00:01:15.359 what a Boolean variable is. It's just a switch 00:01:15.359 --> 00:01:17.819 that can only be true or false. Just up or down. 00:01:18.060 --> 00:01:20.400 Exactly. And you know the fundamental logic gates, 00:01:20.799 --> 00:01:26.150 like A and D or R and not. So A Essay Tolver 00:01:26.150 --> 00:01:28.849 is simply a program that takes a massive formula 00:01:28.849 --> 00:01:32.049 made of those variables and gates and asks one 00:01:32.049 --> 00:01:34.829 question. Right. It asks, is there any possible 00:01:34.829 --> 00:01:37.650 combination of true and false assignments that 00:01:37.650 --> 00:01:39.950 satisfies every single rule? Yeah, and makes 00:01:39.950 --> 00:01:43.170 the whole formula true. If there is, it spits 00:01:43.170 --> 00:01:45.230 out the exact assignments. If not, it proves 00:01:45.230 --> 00:01:48.150 the formula is completely unsatisfiable. But 00:01:48.150 --> 00:01:50.310 the foundational tension from our source material 00:01:50.310 --> 00:01:52.129 relies on a concept you're likely familiar with, 00:01:52.290 --> 00:01:54.150 which is the Cooke -Levin theorem. Oh, yeah, 00:01:54.310 --> 00:01:56.250 the Cooke -Levin theorem. Right. It proved that 00:01:56.250 --> 00:02:00.090 Boolean satisfiability is like the defining NP 00:02:00.090 --> 00:02:02.670 -complete problem. Which is a huge deal. We don't 00:02:02.670 --> 00:02:04.950 need to define NP -complete from scratch for 00:02:04.950 --> 00:02:07.030 you, but we do need to acknowledge the brutal 00:02:07.030 --> 00:02:09.319 reality of the math here. Brutal is the right 00:02:09.319 --> 00:02:12.080 word. I mean, we generally only have algorithms 00:02:12.080 --> 00:02:15.199 with exponential worst case complexity to solve 00:02:15.199 --> 00:02:17.439 these things. Meaning every time you add a single 00:02:17.439 --> 00:02:19.900 new variable to the formula, the search space 00:02:19.900 --> 00:02:22.159 basically doubles. It doubles. So by the time 00:02:22.159 --> 00:02:25.740 you reach just 100 variables, you are dealing 00:02:25.740 --> 00:02:28.400 with more combinations than there are drops of 00:02:28.400 --> 00:02:31.740 water in the ocean. Wow. It is a terrifying exponential 00:02:31.740 --> 00:02:34.120 wall. I mean, if you just sat there testing every 00:02:34.120 --> 00:02:36.900 possible combination of variables, what we call 00:02:36.900 --> 00:02:40.219 naive brute force, the sun would explode before 00:02:40.219 --> 00:02:42.460 you evaluated even a fraction of an industrial 00:02:42.460 --> 00:02:44.460 scale formula. OK, wait, which brings me to this 00:02:44.460 --> 00:02:46.280 glaring contradiction in the text that I really 00:02:46.280 --> 00:02:48.590 want to push back on right away. Sure. The math 00:02:48.590 --> 00:02:52.569 literally dictates that this problem scales exponentially 00:02:52.569 --> 00:02:55.430 into completely impossible territory. Right. 00:02:55.770 --> 00:02:58.909 Yet the source explicitly states that modern 00:02:58.909 --> 00:03:02.650 SAT solvers are routinely handling problem instances 00:03:02.650 --> 00:03:05.500 with tens of thousands of variables and millions 00:03:05.500 --> 00:03:07.659 of constraints. Billions. Yeah. How can both 00:03:07.659 --> 00:03:10.159 things be true? You can't just ignore the mathematical 00:03:10.159 --> 00:03:12.439 bounds of an NP -complete problem. Well, that's 00:03:12.439 --> 00:03:14.759 the central paradox of this entire field, and 00:03:14.759 --> 00:03:17.379 it's a brilliant observation. Over the last two 00:03:17.379 --> 00:03:20.419 decades, computer scientists didn't somehow break 00:03:20.419 --> 00:03:22.840 the fundamental laws of mathematics, you know? 00:03:23.000 --> 00:03:25.280 Right. An exponential curve is still an exponential 00:03:25.280 --> 00:03:28.620 curve. Exactly. Instead, they just got incredibly, 00:03:29.479 --> 00:03:31.860 almost outrageously clever. So they cheated. 00:03:32.199 --> 00:03:35.159 Basically. They didn't find a magic bullet to 00:03:35.159 --> 00:03:38.500 solve NP -complete problems in polynomial time. 00:03:38.860 --> 00:03:42.060 They built this towering stack of heuristics 00:03:42.060 --> 00:03:45.860 and algorithms and engineering optimizations 00:03:45.860 --> 00:03:49.000 to essentially cheat that exponential wall in 00:03:49.000 --> 00:03:51.639 practice. Okay, so they figured out how to mathematically 00:03:51.639 --> 00:03:54.819 prove that vast, vast swaths of the search space 00:03:54.819 --> 00:03:57.080 are just impossible without ever actually searching 00:03:57.080 --> 00:03:59.259 them. That's exactly it. And to understand how 00:03:59.259 --> 00:04:01.379 solvers cheat that math. We need to take a look 00:04:01.379 --> 00:04:03.120 under the hood. We need to go into the engine 00:04:03.120 --> 00:04:05.439 room, basically, and trace the evolution of these 00:04:05.439 --> 00:04:07.780 algorithms. Right. We have to start in the 1960s. 00:04:07.919 --> 00:04:09.780 Yeah. The source starts us off in the early 60s 00:04:09.780 --> 00:04:12.560 with DPLL, which stands for the Davis -Putnam 00:04:12.560 --> 00:04:15.080 -Lodgeman -Lovelland algorithm. A bit of a mouthful, 00:04:15.159 --> 00:04:17.819 but DPLL is the foundational algorithm here. 00:04:18.240 --> 00:04:21.920 It relies on a systematic backtracking search 00:04:21.920 --> 00:04:24.639 procedure. Right. It introduces something called 00:04:24.639 --> 00:04:27.139 unit propagation. So if you have a rule that 00:04:27.139 --> 00:04:31.790 says, AORB must be true. And you've already guessed 00:04:31.790 --> 00:04:34.329 that A is false. Well, B is suddenly forced to 00:04:34.329 --> 00:04:38.050 be true. Exactly. B has to be true. DPLL cascades 00:04:38.050 --> 00:04:40.529 these forced choices. But eventually, you know, 00:04:40.870 --> 00:04:43.170 it has to guess. It runs out of obvious moves. 00:04:43.350 --> 00:04:46.009 Right. So it explores the space of variable assignments. 00:04:46.110 --> 00:04:48.209 And if it hits a conflict like a dead end where 00:04:48.209 --> 00:04:51.050 a rule is broken, it systematically backtracks 00:04:51.050 --> 00:04:54.040 to its last guess and flips it. Okay, I like 00:04:54.040 --> 00:04:56.180 to think of it like navigating a massive dark 00:04:56.180 --> 00:04:58.920 maze. You make a choice at a fork in the road, 00:04:59.240 --> 00:05:01.639 you walk down the path leaving breadcrumbs, and 00:05:01.639 --> 00:05:03.439 if you hit a brick wall, you walk back to the 00:05:03.439 --> 00:05:05.420 last intersection and try the other path. That's 00:05:05.420 --> 00:05:07.740 a great analogy. It's systematic. It's guaranteed 00:05:07.740 --> 00:05:09.759 to find the exit eventually, but... But as we 00:05:09.759 --> 00:05:13.560 know, the maze of an MP complete problem is just 00:05:13.560 --> 00:05:15.939 way too big. Way too big. Even with that unit 00:05:15.939 --> 00:05:18.699 propagation trick, the exponential math catches 00:05:18.699 --> 00:05:21.459 up. Right. And what's fascinating here is how 00:05:21.459 --> 00:05:23.939 the field responded to that bottleneck in the 00:05:23.939 --> 00:05:27.160 2000s. The source introduces a massive paradigm 00:05:27.160 --> 00:05:30.860 shift called CDCL. Conflict Driven Clause Learning. 00:05:31.379 --> 00:05:34.139 Yes. State -of -the -art solvers today almost 00:05:34.139 --> 00:05:37.779 universally run on this CDCL framework. It takes 00:05:37.779 --> 00:05:40.379 that basic DPL search we just talked about and 00:05:40.379 --> 00:05:43.129 fundamentally rewires it. Yeah, the text lists 00:05:43.129 --> 00:05:46.350 its key features as back -jumping, clause learning, 00:05:46.810 --> 00:05:49.730 and this deeply optimized form of unit propagation 00:05:49.730 --> 00:05:52.089 called two -watched literals. Let's stick with 00:05:52.089 --> 00:05:54.290 your maze analogy to really get at the mechanics 00:05:54.290 --> 00:05:56.970 of CDCL, because it's not just leaving breadcrumbs 00:05:56.970 --> 00:05:59.509 anymore. With CDCL, you walk down a path and 00:05:59.509 --> 00:06:01.689 hit a dead end. But instead of just walking back 00:06:01.689 --> 00:06:04.790 to the last fork, the solver stops and analyzes 00:06:04.790 --> 00:06:07.350 the implication graph. It looks at the exact 00:06:07.350 --> 00:06:09.930 sequence of variables that actually forced the 00:06:09.930 --> 00:06:12.319 contradiction. Precisely. It performs conflict 00:06:12.319 --> 00:06:14.639 analysis. It traces the logical roots of its 00:06:14.639 --> 00:06:16.579 own failure. And this is where the learning part 00:06:16.579 --> 00:06:19.019 happens, right? Yeah. It realizes, like, ah, 00:06:19.420 --> 00:06:21.759 it's not just this specific path that's bad. 00:06:22.060 --> 00:06:24.439 The combination of flipping switch 12 up and 00:06:24.439 --> 00:06:26.879 switch 400 down fundamentally breaks the entire 00:06:26.879 --> 00:06:29.180 system. Right, regardless of what the other 10 00:06:29.180 --> 00:06:32.720 ,000 switches are doing. So. It dynamically writes 00:06:32.720 --> 00:06:35.939 a brand new rule, a newly learned clause, and 00:06:35.939 --> 00:06:38.540 adds it to the original rule book. It's amazing. 00:06:38.740 --> 00:06:41.259 It's literally like putting up a massive blazing 00:06:41.259 --> 00:06:44.300 neon sign at the entrance to that whole section 00:06:44.300 --> 00:06:48.139 of the maze saying, never do 12 UP and 400 down. 00:06:48.300 --> 00:06:50.079 Which is such a good way to put it. Right. And 00:06:50.079 --> 00:06:52.519 that leads directly to the back jumping feature 00:06:52.519 --> 00:06:54.959 you mentioned. Oh, right. Because it learned 00:06:54.959 --> 00:06:57.300 the fundamental root of the conflict, it doesn't 00:06:57.300 --> 00:07:00.149 just backtrack one single step. It back jumps. 00:07:00.589 --> 00:07:02.970 It teleports all the way back up the search tree 00:07:02.970 --> 00:07:06.370 to the exact decision level where that newly 00:07:06.370 --> 00:07:08.649 learned rule would have changed its behavior. 00:07:08.790 --> 00:07:12.269 Oh, wow. So it skips evaluating millions of intermediate 00:07:12.269 --> 00:07:14.790 combinations because it mathematically proved 00:07:14.790 --> 00:07:17.750 they all share that exact same fatal flaw. Exactly. 00:07:17.910 --> 00:07:20.350 It aggressively prunes the exponential tree. 00:07:20.449 --> 00:07:22.300 I mean. If you're listening to this and thinking 00:07:22.300 --> 00:07:24.500 it sounds incredibly complex to actually program, 00:07:24.620 --> 00:07:27.459 you are totally right. But here's a staggering 00:07:27.459 --> 00:07:28.879 detail from the text. Oh, I know what you're 00:07:28.879 --> 00:07:31.800 going to say. Minisat, right. It was this highly 00:07:31.800 --> 00:07:35.819 successful CDCL solver from the 2005 SAT competition 00:07:35.819 --> 00:07:38.660 that basically set the standard for the industry. 00:07:38.910 --> 00:07:42.449 It achieves all of this complex, teleporting, 00:07:42.610 --> 00:07:45.730 clause -learning logic in only about 600 lines 00:07:45.730 --> 00:07:49.389 of code. 600 lines. It is an absolute masterclass 00:07:49.389 --> 00:07:52.670 in algorithmic density. Seriously. But CDCL solvers 00:07:52.670 --> 00:07:55.970 also use a memory trick called two -watched literals. 00:07:56.089 --> 00:07:58.350 Because when you have millions of rules constantly 00:07:58.350 --> 00:08:00.709 checking every single rule every time a variable 00:08:00.709 --> 00:08:03.389 changes, well, it just takes too much processing 00:08:03.389 --> 00:08:05.470 power. It would lag the whole system. Yeah. So 00:08:05.470 --> 00:08:08.189 the solver lazily watches just two variables 00:08:08.189 --> 00:08:10.139 per... rule. As long as those two haven't been 00:08:10.139 --> 00:08:12.180 forced to false, the solver ignores the rule 00:08:12.180 --> 00:08:14.579 entirely. It dramatically reduces the memory 00:08:14.579 --> 00:08:17.379 overhead. That's so smart. But as brilliant as 00:08:17.379 --> 00:08:20.300 CDCL is, the source text highlights a really 00:08:20.300 --> 00:08:23.439 stubborn flaw. Unpredictability. Exactly. There 00:08:23.439 --> 00:08:25.800 is no reliable way to predict which heuristic 00:08:25.800 --> 00:08:28.339 or which algorithm will solve a specific SAT 00:08:28.339 --> 00:08:30.800 instance quickly. Not at all. You could have 00:08:30.800 --> 00:08:33.259 solver A breeze through a massive formula in 00:08:33.259 --> 00:08:36.879 three seconds while solver B stalls out and runs 00:08:36.879 --> 00:08:39.940 for a literal month. But then on the very next 00:08:39.940 --> 00:08:42.799 formula, solver B finishes instantly and solver 00:08:42.799 --> 00:08:45.529 A is stuck forever. It's the volatile nature 00:08:45.529 --> 00:08:48.610 of heuristics. I mean, they are essentially educated 00:08:48.610 --> 00:08:51.429 guesses about which variable to flip next. Right. 00:08:51.629 --> 00:08:53.809 Sometimes the guess aligns perfectly with the 00:08:53.809 --> 00:08:55.990 hidden structure of the problem, and sometimes 00:08:55.990 --> 00:08:58.590 it leads the solver straight into an exponentially 00:08:58.590 --> 00:09:01.070 massive tar pit. And if you're an engineer waiting 00:09:01.070 --> 00:09:03.549 for a system verification, you really can't afford 00:09:03.549 --> 00:09:07.370 to guess wrong. You can't. So to fix this unpredictability, 00:09:07.669 --> 00:09:10.190 developers team up. They use parallel processing 00:09:10.190 --> 00:09:12.889 primarily through a parallel portfolio approach. 00:09:13.550 --> 00:09:16.620 meaning you aren't trying to build... one god 00:09:16.620 --> 00:09:18.860 -like solver, you're running a whole diverse 00:09:18.860 --> 00:09:21.220 set of them all at once. Exactly. You take a 00:09:21.220 --> 00:09:24.820 tool like PPfolio or Plindling or Hordesat. Plindling 00:09:24.820 --> 00:09:27.120 is such a great name. It really is. You load 00:09:27.120 --> 00:09:29.480 up different algorithms, or even the exact same 00:09:29.480 --> 00:09:32.240 CDCL algorithm just initialized with different 00:09:32.240 --> 00:09:35.159 random seed values, and you run them simultaneously 00:09:35.159 --> 00:09:38.000 on different processing cores. It is a drag race. 00:09:38.220 --> 00:09:41.000 It's a total drag race. The moment the first 00:09:41.000 --> 00:09:43.460 solver crosses the finish line and finds the 00:09:43.460 --> 00:09:46.850 answer, It flags the system, and all the other 00:09:46.850 --> 00:09:49.389 solvers are instantly terminated. OK, wait. I 00:09:49.389 --> 00:09:50.970 have to challenge the efficiency of this, though. 00:09:51.009 --> 00:09:53.070 Let's say I'm running a 24 -core workstation. 00:09:53.850 --> 00:09:57.889 All 24 cores are grinding away at maximum capacity 00:09:57.889 --> 00:10:01.289 on the exact same problem. Right. One finishes, 00:10:01.929 --> 00:10:04.429 and the other 23 just dump their progress in 00:10:04.429 --> 00:10:07.860 the trash. Isn't that a massive, inefficient 00:10:07.860 --> 00:10:11.080 waste of computing power? We're talking about 00:10:11.080 --> 00:10:14.720 incredibly intensive duplicate work. On the surface, 00:10:14.879 --> 00:10:17.700 yeah, absolutely. And the text actively concedes 00:10:17.700 --> 00:10:20.019 that the amount of duplicate work is the primary 00:10:20.019 --> 00:10:22.600 drawback of portfolios. It has to be. But there 00:10:22.600 --> 00:10:25.279 is a very clever architectural workaround to 00:10:25.279 --> 00:10:27.679 mitigate that waste, which is clause sharing. 00:10:27.779 --> 00:10:29.639 Clause sharing. Remember those neon signs we 00:10:29.639 --> 00:10:31.929 talked about, the learned clauses? Oh! the new 00:10:31.929 --> 00:10:33.929 rules that solvers write when they hit a conflict. 00:10:34.149 --> 00:10:36.389 Right. In a sophisticated parallel portfolio 00:10:36.389 --> 00:10:38.789 like quartzat, those independent solvers actually 00:10:38.789 --> 00:10:42.210 communicate? Yeah. When one solver gets stuck 00:10:42.210 --> 00:10:45.080 in a tar pit, analyzes the conflict, and learns 00:10:45.080 --> 00:10:48.500 a mathematically vital new clause, it broadcasts 00:10:48.500 --> 00:10:51.320 that clause to the other 23 parallel solvers. 00:10:51.539 --> 00:10:54.100 Oh, wow. So even though they are exploring total 00:10:54.100 --> 00:10:56.139 different branches of the search space, they're 00:10:56.139 --> 00:10:57.960 constantly sharing their maps with each other. 00:10:58.240 --> 00:11:01.879 Exactly. Solver A avoids a dead end because solver 00:11:01.879 --> 00:11:04.279 B already mapped it and shared the warning sign. 00:11:05.000 --> 00:11:07.620 This radical sharing of information fundamentally 00:11:07.620 --> 00:11:10.399 changes the efficiency of the entire portfolio. 00:11:10.700 --> 00:11:12.899 OK, so they aren't completely siloed. That makes 00:11:12.899 --> 00:11:15.139 a lot more sense. But the portfolio isn't the 00:11:15.139 --> 00:11:17.799 only way to team up. If you have one massive 00:11:17.799 --> 00:11:20.879 monolithic problem that is so dense that no single 00:11:20.879 --> 00:11:23.120 algorithm can crack it even with shared maps, 00:11:23.639 --> 00:11:25.679 sharing just isn't enough. You need to physically 00:11:25.679 --> 00:11:27.860 fracture the problem. Right. And the text points 00:11:27.860 --> 00:11:30.039 to a strategy called the cube and conquer paradigm. 00:11:30.340 --> 00:11:32.659 Yes. This is a really modern application of the 00:11:32.659 --> 00:11:35.200 classic divide and conquer technique. You split 00:11:35.200 --> 00:11:37.179 the big problem into smaller pieces and hand 00:11:37.179 --> 00:11:40.419 them out. But the text notes that with SAT solving, 00:11:40.879 --> 00:11:43.419 traditional splitting creates absolute load balancing 00:11:43.419 --> 00:11:45.940 nightmares. Because of the unpredictability again. 00:11:46.320 --> 00:11:48.100 Exactly. If you just blindly chop the formula 00:11:48.100 --> 00:11:51.059 in half, core one might get a piece that evaluates 00:11:51.059 --> 00:11:54.820 in two seconds. Well, core two gets a chunk of 00:11:54.820 --> 00:11:56.419 the problem that is mathematically dense and 00:11:56.419 --> 00:12:00.600 takes five years. Core one sits idle. and you've 00:12:00.600 --> 00:12:02.840 gained nothing. Right, it's totally unbalanced. 00:12:03.480 --> 00:12:05.740 So Cube and Conqueror introduces a two -phase 00:12:05.740 --> 00:12:08.179 approach to intelligently fracture the problem. 00:12:08.580 --> 00:12:11.100 Phase one is the cube phase. And they don't use 00:12:11.100 --> 00:12:13.539 a CDCL solver for this part, do they? No, they 00:12:13.539 --> 00:12:15.240 use a completely different architecture called 00:12:15.240 --> 00:12:17.740 a look -ahead solver. Look -ahead solvers are 00:12:17.740 --> 00:12:19.639 generally too slow to solve huge problems on 00:12:19.639 --> 00:12:22.059 their own, but they are meticulously good at 00:12:22.059 --> 00:12:25.120 measuring the search space. They evaluate exactly 00:12:25.120 --> 00:12:27.720 how much the problem simplifies if you assign 00:12:27.720 --> 00:12:30.799 a specific variable. The lookahead solver basically 00:12:30.799 --> 00:12:34.340 acts as the surveyor. The text details that use 00:12:34.340 --> 00:12:37.379 a battery of heuristics here. A decision heuristic 00:12:37.379 --> 00:12:39.779 chooses which variable creates the most balanced 00:12:39.779 --> 00:12:42.440 fracture, a direction heuristic decides whether 00:12:42.440 --> 00:12:45.620 to assign true or false first, and a cutoff heuristic 00:12:45.620 --> 00:12:47.539 decides when a specific piece of the formula 00:12:47.539 --> 00:12:50.120 is finally small enough to stop chopping. It 00:12:50.120 --> 00:12:52.799 meticulously maps the fault lines. It chops the 00:12:52.799 --> 00:12:55.679 massive problem into thousands, sometimes millions, 00:12:56.379 --> 00:13:00.720 of smaller, roughly equally complex sub -problems. 00:13:00.980 --> 00:13:02.799 These are the cubes. These are the cubes. Once 00:13:02.799 --> 00:13:05.139 the problem is perfectly fractured, phase two 00:13:05.139 --> 00:13:08.539 begins, which is the conquer phase. Right. Those 00:13:08.539 --> 00:13:11.240 millions of cubes are handed off to independent 00:13:11.240 --> 00:13:14.799 CDCL solvers to tackle concurrently. Because 00:13:14.799 --> 00:13:17.419 the cubes are relatively uniform in difficulty, 00:13:18.000 --> 00:13:21.120 the parallel processors stay perfectly load balanced. 00:13:21.320 --> 00:13:23.799 And if even one of those solvers finds a satisfying 00:13:23.799 --> 00:13:26.440 assignment for its cube, the entire original 00:13:26.440 --> 00:13:28.779 problem is solved. Exactly. I just love the mechanics 00:13:28.779 --> 00:13:31.159 of Cube and Conquer. So intensely structured, 00:13:31.580 --> 00:13:33.419 you know, mapping the fault lines, optimizing 00:13:33.419 --> 00:13:35.799 the load balance, but the text actually takes 00:13:35.799 --> 00:13:37.899 a sharp pivot right after this. It does, yeah. 00:13:38.039 --> 00:13:40.720 We go from this highly logical, methodical division 00:13:40.720 --> 00:13:43.340 of labor into an entirely different philosophy 00:13:43.340 --> 00:13:45.940 of problem solving. We move from rigid logic 00:13:45.940 --> 00:13:49.490 to stochastic guessing. the stochastic and randomized 00:13:49.490 --> 00:13:51.649 algorithms. This is a massive departure from 00:13:51.649 --> 00:13:53.570 everything we've discussed so far. Here's where 00:13:53.570 --> 00:13:55.769 it gets really interesting. You and I are talking 00:13:55.769 --> 00:13:58.289 about evaluating perfectly rigid mathematical 00:13:58.289 --> 00:14:01.929 formulas, but the text reveals that sometimes 00:14:01.929 --> 00:14:05.330 injecting pure unadulterated randomness into 00:14:05.330 --> 00:14:08.690 the process is actually the fastest way to the 00:14:08.690 --> 00:14:11.149 answer. I mean, it feels completely counterintuitive, 00:14:11.190 --> 00:14:14.080 but it's essential. Why? Because systematic search 00:14:14.080 --> 00:14:17.279 algorithms, even CDCL with all its fancy clause 00:14:17.279 --> 00:14:20.039 learning, can get trapped. They get stuck in 00:14:20.039 --> 00:14:22.840 what we call local minima. OK, what is that? 00:14:22.940 --> 00:14:25.039 It's like they wander into a massive plateau 00:14:25.039 --> 00:14:27.340 in the search space where every single logical 00:14:27.340 --> 00:14:30.100 deduction just leads to another million strong 00:14:30.100 --> 00:14:32.500 branch of useless variables. They just get bogged 00:14:32.500 --> 00:14:35.360 down. Right. To escape that gravitational pull, 00:14:35.860 --> 00:14:38.039 algorithms that use stochastic local search, 00:14:38.279 --> 00:14:41.759 like WoxAsset, just abandon systematic backtracking 00:14:41.759 --> 00:14:44.419 entirely. So how does WoxAsset operate differently? 00:14:44.639 --> 00:14:46.559 Instead of building an assignment variable by 00:14:46.559 --> 00:14:49.740 variable, WoxAsset assigns a value to every single 00:14:49.740 --> 00:14:52.600 variable right at the start. Really? Just completely 00:14:52.600 --> 00:14:54.500 at random? Completely at random. Then it looks 00:14:54.500 --> 00:14:56.519 at the clauses that are currently unsatisfied, 00:14:56.620 --> 00:14:58.379 and it just starts flipping variables trying 00:14:58.379 --> 00:15:01.700 to fix them. Huh. Sometimes, to fix one clause, 00:15:01.960 --> 00:15:04.779 it has to temporarily break another clause. It 00:15:04.779 --> 00:15:07.000 actually tolerates worsening the overall state 00:15:07.000 --> 00:15:09.600 to escape those local minima. And the source 00:15:09.600 --> 00:15:12.039 also breaks down a randomized algorithm called 00:15:12.039 --> 00:15:15.360 PPSZ. This one fascinated me. Oh. It doesn't 00:15:15.360 --> 00:15:17.799 just randomly flip things like walk S -T? No, 00:15:17.799 --> 00:15:19.840 it's a bit different. It tries to set variables 00:15:19.840 --> 00:15:22.789 in a random order. But it uses a heuristic called 00:15:22.789 --> 00:15:26.250 bounded with resolution to infer forced choices 00:15:26.250 --> 00:15:28.470 based on what's already been set Yeah, so it 00:15:28.470 --> 00:15:30.970 uses logic to deduce what a variable must be 00:15:30.970 --> 00:15:34.110 right, but if that bounded with resolution fails 00:15:34.490 --> 00:15:36.789 Like, if the logic isn't clear, it literally 00:15:36.789 --> 00:15:39.090 just rolls the dice. It randomly guesses true 00:15:39.090 --> 00:15:41.389 or false. It moves on. And we really have to 00:15:41.389 --> 00:15:43.389 look at the incredible mathematical efficiency 00:15:43.389 --> 00:15:45.590 of this guided guessing. The text highlights 00:15:45.590 --> 00:15:48.950 a 2019 modification of the PPSZ algorithm by 00:15:48.950 --> 00:15:52.509 Hansen, Kaplan, Zemier, and Zwick. Yeah. By refining 00:15:52.509 --> 00:15:55.289 this balance of logical deduction and pure randomness, 00:15:55.629 --> 00:15:58.870 they achieved a runtime bound of O of 1 .307 00:15:58.870 --> 00:16:01.690 to the power of n for three SAT problems. OK, 00:16:01.690 --> 00:16:04.240 let's contextualize that bound for you. O of 00:16:04.240 --> 00:16:06.899 2 to the power of n is the nightmare scenario 00:16:06.899 --> 00:16:09.200 we talked about at the beginning, where the complexity 00:16:09.200 --> 00:16:11.840 doubles with every variable. Right, the exponential 00:16:11.840 --> 00:16:13.879 wall. Getting that base number down from 2 to 00:16:13.879 --> 00:16:17.720 1 .307 might look like a minor tweak on paper, 00:16:18.299 --> 00:16:21.320 but exponentially it is a staggering reduction 00:16:21.320 --> 00:16:24.269 in processing time. It is currently the fastest 00:16:24.269 --> 00:16:26.370 known algorithm for these types of problems. 00:16:27.009 --> 00:16:29.250 It mathematically proves that statistically, 00:16:29.850 --> 00:16:32.710 by guessing intelligently and injecting pure 00:16:32.710 --> 00:16:35.570 randomness when your logic fails, you will actually 00:16:35.570 --> 00:16:37.929 reach the correct solution faster than if you 00:16:37.929 --> 00:16:40.330 methodically mapped out every single consequence. 00:16:40.690 --> 00:16:43.090 So logic's best friend is literally a roll of 00:16:43.090 --> 00:16:45.409 the dice. Sometimes randomness is the ultimate 00:16:45.409 --> 00:16:48.289 shortcut through NP -complete space. That is 00:16:48.289 --> 00:16:50.409 just brilliant. But let's bring this down from 00:16:50.409 --> 00:16:52.440 the theoretical algorithmic cloud. and anchor 00:16:52.440 --> 00:16:54.759 it back to reality for a second. Good idea. We've 00:16:54.759 --> 00:16:57.200 sped this deep dive exploring how solvers use 00:16:57.200 --> 00:17:00.039 teleporting back jumps, parallel clause sharing, 00:17:00.580 --> 00:17:03.240 and stochastic dice rolls to shatter the exponential 00:17:03.240 --> 00:17:06.200 wall. What are we actually using these superpowers 00:17:06.200 --> 00:17:08.559 for? Like, think about the device you're listening 00:17:08.559 --> 00:17:11.720 to us on right now. How do SAT solvers impact 00:17:11.720 --> 00:17:14.240 that? If we connect this to the bigger picture, 00:17:14.440 --> 00:17:16.619 The applications listed in the source material 00:17:16.619 --> 00:17:18.940 are really the foundation of modern technology. 00:17:19.700 --> 00:17:22.359 First and foremost is verification and automated 00:17:22.359 --> 00:17:25.559 planning. SAT solvers are the core engine inside 00:17:25.559 --> 00:17:29.440 what we call SMT solvers, or Satisfiability Modulo 00:17:29.440 --> 00:17:32.220 Theories. And SMT solvers are what hardware and 00:17:32.220 --> 00:17:34.400 software giants use to verify their systems. 00:17:34.700 --> 00:17:36.880 Exactly. I mean, when a company designs a new 00:17:36.880 --> 00:17:39.599 microchip architecture or writes the software 00:17:39.599 --> 00:17:41.920 that controls a commercial airliner's autopilot, 00:17:42.140 --> 00:17:45.099 they cannot afford a single Obviously not. You 00:17:45.099 --> 00:17:47.319 can't just run a billion test cases and hope 00:17:47.319 --> 00:17:49.579 for the best because a billion tests won't cover 00:17:49.579 --> 00:17:51.579 even a fraction of the possible states. So what 00:17:51.579 --> 00:17:54.700 do they do? They translate the entire logic of 00:17:54.700 --> 00:17:57.799 the hardware design into a massive Boolean formula 00:17:57.799 --> 00:18:00.900 and they feed it to a SAT solver with one simple 00:18:00.900 --> 00:18:04.670 question. Is there any possible combination of 00:18:04.670 --> 00:18:07.930 inputs, no matter how chaotic, that causes this 00:18:07.930 --> 00:18:10.450 system to violate its safety parameters? Wow. 00:18:11.009 --> 00:18:14.289 So if the solver says unsatisfiable, you have 00:18:14.289 --> 00:18:16.609 mathematical proof your chip is completely safe. 00:18:16.670 --> 00:18:19.250 Yes. If it says satisfiable and spits out an 00:18:19.250 --> 00:18:21.859 assignment, well... You just found a catastrophic 00:18:21.859 --> 00:18:24.000 bug before the chip ever went to manufacturing. 00:18:24.640 --> 00:18:27.119 Exactly. It's also used heavily in operations 00:18:27.119 --> 00:18:29.740 research, you know, translating unimaginably 00:18:29.740 --> 00:18:32.140 complex factory scheduling or logistical routing 00:18:32.140 --> 00:18:34.859 into Boolean constraints just to find the single 00:18:34.859 --> 00:18:37.240 most efficient path. But the applications push 00:18:37.240 --> 00:18:40.279 way beyond just industry. SAT solvers are actively 00:18:40.279 --> 00:18:42.359 advancing human knowledge in pure mathematics. 00:18:42.480 --> 00:18:44.480 They really are. They're generating proofs that 00:18:44.480 --> 00:18:46.559 human mathematicians simply cannot construct 00:18:46.559 --> 00:18:48.279 on their own. Which brings us back to the hook 00:18:48.279 --> 00:18:50.779 we started with, the 2016 example from the tech. 00:18:50.799 --> 00:18:53.339 Oh, yes. Three researchers, Huell, Coleman, and 00:18:53.339 --> 00:18:55.599 Merrick, used a SAT solver to crack the Boolean 00:18:55.599 --> 00:18:57.920 Pythagorean triples problem. Yeah, the problem 00:18:57.920 --> 00:19:00.440 asked a pretty simple sounding question. Is it 00:19:00.440 --> 00:19:02.859 possible to color every integer starting from 00:19:02.859 --> 00:19:07.680 1 up to 7825 either red or blue in such a way 00:19:07.680 --> 00:19:10.599 that no set of Pythagorean triples like 3, 4, 00:19:10.640 --> 00:19:13.640 and 5 where a squared plus b squared equals c 00:19:13.640 --> 00:19:15.779 squared are all the same color? And to solve 00:19:15.779 --> 00:19:17.950 it... They used the cube and conquer method we 00:19:17.950 --> 00:19:20.109 discussed earlier. They fractured the search 00:19:20.109 --> 00:19:22.750 space of those thousands of integers into millions 00:19:22.750 --> 00:19:25.450 of cubes, fed them to a supercomputer running 00:19:25.450 --> 00:19:28.769 SAT solvers, and asked it to find a valid coloring 00:19:28.769 --> 00:19:31.329 combination. And the solver crunched the logic 00:19:31.329 --> 00:19:33.630 and proved that no, there is no way to do it. 00:19:33.750 --> 00:19:36.569 It is mathematically unsatisfiable. And it generated 00:19:36.569 --> 00:19:39.859 a 200 terabyte proof to verify its work. We are 00:19:39.859 --> 00:19:42.279 using true and false algorithms to map the fundamental 00:19:42.279 --> 00:19:44.880 bounds of numbers themselves. It's computer -assisted 00:19:44.880 --> 00:19:47.400 proof at a scale that redefines mathematics entirely. 00:19:48.400 --> 00:19:50.339 But perhaps the most surprising application detailed 00:19:50.339 --> 00:19:52.559 in our source text is in social choice theory. 00:19:52.880 --> 00:19:55.279 Oh, this part is wild. I was absolutely fixated 00:19:55.279 --> 00:19:57.539 on this part of the text. Using rigid Boolean 00:19:57.539 --> 00:20:00.400 logic to analyze the messy reality of human voting 00:20:00.400 --> 00:20:02.980 systems. It's a fascinating intersection, isn't 00:20:02.980 --> 00:20:05.900 it? Social choice theory deals with how groups 00:20:05.900 --> 00:20:09.000 of people aggregate their preferences to make 00:20:09.000 --> 00:20:11.440 a single decision. Like, how do you design a 00:20:11.440 --> 00:20:14.000 perfectly fair election? Exactly. And it turns 00:20:14.000 --> 00:20:16.720 out you can mathematically model a voting system. 00:20:17.319 --> 00:20:20.220 You create Boolean variables that represent concepts 00:20:20.220 --> 00:20:23.640 like voter A prefers candidate X over candidate 00:20:23.640 --> 00:20:26.559 Y. OK. You add constraints to enforce logic, 00:20:26.759 --> 00:20:30.059 like transitivity. So if X beats Y and Y beats 00:20:30.059 --> 00:20:33.480 Z, then X must beat Z. So you essentially translate 00:20:33.480 --> 00:20:36.240 the rules of the election itself into a massive 00:20:36.240 --> 00:20:38.920 Boolean formula. Yes. And researchers have used 00:20:38.920 --> 00:20:41.890 SAT solvers. to definitively prove impossibility 00:20:41.890 --> 00:20:44.630 theorems regarding these human structures. Precisely. 00:20:44.670 --> 00:20:47.309 They analyze things like Arrow's theorem or the 00:20:47.309 --> 00:20:49.910 no -show paradox or the impossibility of fair 00:20:49.910 --> 00:20:52.349 fractional social choice. The SAT solver takes 00:20:52.349 --> 00:20:54.609 the constraints of what we demand a fair election 00:20:54.609 --> 00:20:57.289 to be, crunches the combinations, and spits back 00:20:57.289 --> 00:21:00.250 the answer. Unsatisfiable. It mathematically 00:21:00.250 --> 00:21:04.019 proves that under certain constraints, A voting 00:21:04.019 --> 00:21:07.660 system that is entirely fair to everyone is not 00:21:07.660 --> 00:21:10.299 just difficult to design, it is fundamentally 00:21:10.299 --> 00:21:13.319 impossible. The logic inherently contradicts 00:21:13.319 --> 00:21:14.960 itself. That's incredible. So what does this 00:21:14.960 --> 00:21:17.819 all mean? We started this deep dive looking at 00:21:17.819 --> 00:21:21.740 a simple concept, true or false, endy or not. 00:21:21.799 --> 00:21:24.619 It's just logic gates. We confronted the terrifying, 00:21:25.079 --> 00:21:27.279 seemingly insurmountable wall of exponential 00:21:27.279 --> 00:21:30.299 complexity that comes with NP -complete problems. 00:21:30.650 --> 00:21:33.670 And we saw how computer science refuses to accept 00:21:33.670 --> 00:21:35.569 defeat. They just cheat the math. We learned 00:21:35.569 --> 00:21:38.390 how CDCL analyzes its own failures to leave neon 00:21:38.390 --> 00:21:40.890 warning signs, how Cuban Conqueror intelligently 00:21:40.890 --> 00:21:43.410 fractures mountains of data, and how stochastic 00:21:43.410 --> 00:21:46.309 algorithms like WACASAT use randomness to escape 00:21:46.309 --> 00:21:48.609 the gravitational pull of local minima. All to 00:21:48.609 --> 00:21:51.009 find that one satisfying assignment. Exactly. 00:21:51.259 --> 00:21:53.819 We use these mind -bending engines to verify 00:21:53.819 --> 00:21:56.359 the silicon on our phones, optimize our logistics, 00:21:56.960 --> 00:21:59.319 compute 200 terabyte mathematical proofs, and 00:21:59.319 --> 00:22:01.779 even evaluate the inherent fairness of our democracies. 00:22:02.140 --> 00:22:05.359 It really is a profound testament to how far 00:22:05.359 --> 00:22:07.779 we can push the boundaries of mechanized logic. 00:22:08.359 --> 00:22:10.720 And this actually raises an important question, 00:22:10.839 --> 00:22:12.700 a final thought for you to mull over as we wrap 00:22:12.700 --> 00:22:15.599 up today. What's that? Well, if we are currently 00:22:15.599 --> 00:22:18.200 using SAT solvers to evaluate the constraints 00:22:18.200 --> 00:22:21.160 of human voting rules and mathematics proving 00:22:21.160 --> 00:22:23.619 that certain systems we desire are just logically 00:22:23.619 --> 00:22:27.119 impossible, where else could we apply this? Oh, 00:22:27.119 --> 00:22:29.980 wow. What if we could translate the broader structures 00:22:29.980 --> 00:22:33.240 of our society, like our municipal legal systems, 00:22:33.460 --> 00:22:36.980 our complex tax codes, or even our ethical and 00:22:36.980 --> 00:22:39.900 regulatory frameworks into massive sets of Boolean 00:22:39.900 --> 00:22:42.039 constraints? Just feed the whole legal code into 00:22:42.039 --> 00:22:44.609 a solver. Yeah. Could we one day feed the laws 00:22:44.609 --> 00:22:47.730 of our society into a SAT solver and have it 00:22:47.730 --> 00:22:49.970 spit back a mathematical proof that our legal 00:22:49.970 --> 00:22:52.950 code inherently contradicts itself? Could a computer 00:22:52.950 --> 00:22:55.390 prove that the rules governing our society are, 00:22:55.390 --> 00:22:58.190 at their core, fundamentally unsatisfiable? It's 00:22:58.190 --> 00:23:00.490 a wild thought to leave on. Trying to find the 00:23:00.490 --> 00:23:03.180 bugs in the code of our own civilization. But 00:23:03.180 --> 00:23:05.859 until we start feeding the tax code into a supercomputer, 00:23:06.359 --> 00:23:08.519 the next time you tap a screen or flip a switch, 00:23:08.880 --> 00:23:11.039 just remember the millions of invisible logic 00:23:11.039 --> 00:23:13.859 puzzles being solved every single second to keep 00:23:13.859 --> 00:23:16.140 the silicon humming and the math checking out. 00:23:16.619 --> 00:23:18.039 Thanks for joining us and we'll catch you on 00:23:18.039 --> 00:23:18.920 the next deep dive.