A Peek Inside SAT Solvers - Jon Smock

[@RickeyBowers]

A comprehensive overview explained in a very accessible manner, wow!

[@BlueMesaCable]

I feel like this is an incredibly powerful and yet developing field with little discussion about it online. Perhaps it's the domain of universities and corporations besides those few interested on the side - I must admit, I don't know where I'd use this myself - but it's really compelling.

[@ayushrastogi6176]

Thanks Jon, one of most comprehensive stuff for beginners, really good !!

[@ElliotPotts]

Awesome talk, got me really intrigued by SAT!

[@anthonyapm]

Awesome talk. Very comprehensive.

[@user-nj1qc7uc9c]

this is an insanely good talk!

[@varunvarma5424]

Really nice slides.

[@SaulloCarvalho]

Awesome talk! Thank you.

[@darksaga2006]

Awesome talk thank you

[@holf99]

what did you mean by keeping the clauses after we restart? if we keep the same clauses then what is different between before the restart and after? Thanks for the great video btw it's a lot of help.

[@stathissideris]

I think he meant that CDCL learns some clauses that were not in the initial instance, then we backtrack to the route (restart) but keep the learned clauses, so we start from a better place.

[@Madsy9]

Late reply, but the idea is that the clause database contains a lot of knowledge that the SAT solver has learned about the problem. That is, given sets of both guessed and inferred literal values, we can infer a set of clause collisions (collisions/contradictions among literals lead to empty clauses). Then when you 'restart' (which means to restart the depth-first search), all you have done is to start your guessing from the beginning, but you keep the clause collision database. So, now you have more knowledge about which guesses to avoid, which hopefully will lead you on a different branch than before. This really helps getting SAT-solvers 'unstuck' when they are searching deep in an obviously bad branch of the graph. If your SAT-solver does not support restarts, then its clause database might at some point contain enough information to deduce that it is on the wrong deep path altogether, but it can't make use of that fact until it is done searching the whole graph sub-tree currently under consideration.

[@catmacopter8545]

Hello from AlphaPhoenix

[@andersseruppoulsen7010]

If we suppose there is an algorithm for P vs NP, would it have to be able to find solutions where we now use trial and error? In harder Sudokus, for example, there are times when you have two or more possible numbers and need to guess whereafter you work the rest of the numbers through to see if what you guessed is right. There is a distinction between problems where the solution is given by the process of elimination and problems where you have to guess. Does P vs NP concern the former only or also the latter? An answer would be very much appreciated!

[@albins0]

I know this is coming a bit late, but I'll answer anyway! That is precisely the case. You can think of it like this: NP is the domain of problems that are fast (polynomial time) to check, but (probably) hard to compute. It stands for "Nondeterministically polynomial". That means that these problems would be solved in poly-time by a nondeterministic machine. Such a machine would indeed "find solutions" instead of searching; in principle it would make all choices at once and only use the correct ones. What we do when we search in the case of NP-complete problems is effectively emulating a non-deterministic machine. IF we could reduce NP to P, that means we could re-cast the search problem to one that does not require searching, and therefore we would not need trial and error. However, even if we theoretically could do such a reduction, it is not guaranteed to be viable in practice, as all the quantifiers are asymptotic. In practice, this means that we might re-cast our problem as something in p, say n^k, where k is a constant. The lower bound on that constant could be the number of atoms in the universe, and we would still be in P without having something we could actually use.

[@quosswimblik4489]

If you match 2 cells possible paths in sudoku then a crab with 2 claws is more efficient than 1 or 3. You could make a game out of the problem where by with a 16 by 16 grid the sudoku auto fills as far as possible with basic rules then you each pick 2 squares to compare and the one with the most partial solutions 0.5 and solved squares 1 point by the time the problem folds wins

[@JB-vd9hg]

In his run through DPLL, after the x1=false branch gets a contradiction, he sets x1=true. On that branch how does he get that x2=true? Using line one, which is "(or x1 x2)", I would assume that if x1 is true then that x2 is actually false... which contradicts what the video shows. Any help would be appreciated.

[@RickeyBowers]

Look at the truth table for OR - if x1=true, then x2 can be any value, one true value is sufficient to make the whole clause true.

[@keejay98195]

The clause is (or x1 x2). It means either x1 is true, or x2 is true, or both are true. The order in which he finds out x2 is true is not actually just by finding out that x1 is true, he just skipped a few steps there to save some time.

[@at1with0]

SAT becomes what problem when completeness turns it to syntactic theorem proving?

[@Madsy9]

Not exactly sure what you mean, but you can think of 3-SAT as the unit NP-complete problem from which all NP complete-problems are defined. That is, any NP-complete problem can be (and must be) convertible into any other NP-complete problem, where 3-SAT historically bootstrapped the first problem classifications under this definition. This is known as Cook's theorem.