3 ms·

SAT solvers are used a lot for NP-complete problems, but they don't use the 3-SAT representation of clauses. 3-SAT is only interesting from a theoretical POV. N

SAT solvers are used a lot for NP-complete problems, but they don't use the 3-SAT representation of clauses. 3-SAT is only interesting from a theoretical POV. Nobody uses it in practice. There are also intermediate representations. For instance, pseudo-boolean retains most of the power of SAT solvers, while at the same time making problems much easier to express in terms of number of constraints needed. For instance, your Alldifferent(X11, X12, X13, X14, X15, X16, X17, X18, X19) constraint would be written as "x11 + x12 + x13 + x14 + x15 + x16 + x17 + x18 + x19 = 1". Same expressive power, on this problem.

dragontamer 4y ago
> For instance, your Alldifferent(X11, X12, X13, X14, X15, X16, X17, X18, X19) constraint would be written as "x11 + x12 + x13 + x14 + x15 + x16 + x17 + x18 + x19 = 1". Same expressive power, on this problem. I'm more comfortable with constraint-programming than 3SAT / SMT / etc. etc. So I'm probably getting something wrong here. I don't think you're correct on this issue? "x11 + x12 = 1" means that "x11 or x12 are 1, and the other is zero". EDIT: That is, the 9-set of solutions you described is: {1, 0, 0, 0, 0, 0, 0, 0, 0} {0, 1, 0, 0, 0, 0, 0, 0, 0} {0, 0, 1, 0, 0, 0, 0, 0, 0} {0, 0, 0, 1, 0, 0, 0, 0, 0} {0, 0, 0, 0, 1, 0, 0, 0, 0} {0, 0, 0, 0, 0, 1, 0, 0, 0} {0, 0, 0, 0, 0, 0, 1, 0, 0} {0, 0, 0, 0, 0, 0, 0, 1, 0} {0, 0, 0, 0, 0, 0, 0, 0, 1} Meanwhile, Alldifferent(X11, X12, X13, X14, X15, X16, X17, X18, X19) represents the following 9-factorial set of solutions: {1, 2, 3, 4, 5, 6, 7, 8, 9} {1, 2, 3, 4, 5, 6, 7, 9, 8} {1, 2, 3, 4, 5, 6, 9, 8, 7} {1, 2, 3, 4, 5, 6, 9, 7, 8} {1, 2, 3, 4, 5, 9, 6, 7, 8} {1, 2, 3, 4, 5, 9, 6, 8, 7} {1, 2, 3, 4, 5, 9, 7, 6, 8} {1, 2, 3, 4, 5, 9, 7, 8, 6} {1, 2, 3, 4, 5, 9, 8, 6, 7} {1, 2, 3, 4, 5, 9, 8, 7, 6} .... {9, 8, 7, 6, 5, 4, 3, 2, 1} That is, the entire set of permutations of the domain of all 9 variables participating in the constraint. What I've listed above is a *complete* Sudoku solver within the constraint-programming mindset. -------- In most of the 3SAT / SMT solvers for Sudoku I've seen, you set up the variables as: "X111, X112, X113, X114...", which means "X11 == 1", and "X11 == 2", etc. etc. So you then do "X111 + X112 + X113... X119 == 1", meaning "X11 is either 1, 2, 3, 4, 5... 9". Meanwhile, this entire process is simply "Domain of X11 = {1, 2, 3, 4, 5, 6, 7, 8, 9}" in the constraint-processing world, because variables can have arbitrarily sized (though finite) domains in constraint programming. That is to say, I'm pretty sure you need 999 == 729 variables to brute-force represent the problem in 3SAT / SMT? Meanwhile, Constraint Solver trivially represents it with 81-variables (but each of these 81 variables, X11 through X99, have a domain of size 9: {1, 2, 3, 4, 5, 6, 7, 8, 9}). There might be an easier way to represent Sudoku in 3SAT/SMT world, but again, I'm not very good with that world. I "just" know that 3SAT / SMT is a "similar but different" kind of solver and barely have used them. -------- One can argue that "constraint programming" is simply 3SAT / SMT-solving except with arbitrarily sized domains. Rather than solely using 0 and 1 or boolean functions. I've been told that "because everything is {0, 1}, more optimizations / inferences can be discovered" in 3SAT/SMT solvers compared to constraint programmers. Meanwhile, constraint programmers benefit from generic constraints that have a polynomial class subsolution (ie: using maximum flow, or other simpler algorithms to solve the subproblem). It'd take a rather well-studied expert to know whether 3SAT/SMT is better for a particular problem vs constraint-programming.
- sacado2 4y ago
  > I don't think you're correct on this issue? "x11 + x12 = 1" means that "x11 or x12 are 1, and the other is zero". and > In most of the 3SAT / SMT solvers for Sudoku I've seen, you set up the variables as: "X111, X112, X113, X114...", which means "X11 == 1", and "X11 == 2", etc. etc. So you then do "X111 + X112 + X113... X119 == 1", meaning "X11 is either 1, 2, 3, 4, 5... 9". Yes, I've been a bit to fast here. You're absolutely right. > I've been told that "because everything is {0, 1}, more optimizations / inferences can be discovered" in 3SAT/SMT solvers compared to constraint programmers. Meanwhile, constraint programmers benefit from generic constraints that have a polynomial class subsolution (ie: using maximum flow, or other simpler algorithms to solve the subproblem). Yes. SAT solvers very often outperform CSP solvers nowadays. But SAT solvers tend to lose the structure of the problem because they are so low-level. The most famous problem they fail to solve is the pigeonhole problem. If you have, say, the problem "is there a way to put 4 pigeons into 3 different holes, knowing that there can be at most 1 pigeon per hole and at least 1 hole per pigeon?", the answer is obviously "no", but if you try to use a propositional logic representation (in other words, using a SAT solver), the solving track will grow exponentially (4 vs 3 workds well, but SAT solvers will struggle to solve 11 vs 10 in a reasonable amount of time). Pseudo-boolean solvers will be able to using "cutting-planes" strategies that work well for this specific set of problems, but these are slower in the general case. Plus, modeling your problem in CNF to feed it to a SAT solver is usually incredibly complex and can lead to gigantic formulas if you're not careful. So most of the time, it really makes sense to first use a CSP representation, and fall back to a CNF representation if you're not satisfied with the results for some reason.

dragontamer 4y ago

> For instance, your Alldifferent(X11, X12, X13, X14, X15, X16, X17, X18, X19) constraint would be written as "x11 + x12 + x13 + x14 + x15 + x16 + x17 + x18 + x19 = 1". Same expressive power, on this problem. I'm more comfortable with constraint-programming than 3SAT / SMT / etc. etc. So I'm probably getting something wrong here. I don't think you're correct on this issue? "x11 + x12 = 1" means that "x11 or x12 are 1, and the other is zero". EDIT: That is, the 9-set of solutions you described is: {1, 0, 0, 0, 0, 0, 0, 0, 0} {0, 1, 0, 0, 0, 0, 0, 0, 0} {0, 0, 1, 0, 0, 0, 0, 0, 0} {0, 0, 0, 1, 0, 0, 0, 0, 0} {0, 0, 0, 0, 1, 0, 0, 0, 0} {0, 0, 0, 0, 0, 1, 0, 0, 0} {0, 0, 0, 0, 0, 0, 1, 0, 0} {0, 0, 0, 0, 0, 0, 0, 1, 0} {0, 0, 0, 0, 0, 0, 0, 0, 1} Meanwhile, Alldifferent(X11, X12, X13, X14, X15, X16, X17, X18, X19) represents the following 9-factorial set of solutions: {1, 2, 3, 4, 5, 6, 7, 8, 9} {1, 2, 3, 4, 5, 6, 7, 9, 8} {1, 2, 3, 4, 5, 6, 9, 8, 7} {1, 2, 3, 4, 5, 6, 9, 7, 8} {1, 2, 3, 4, 5, 9, 6, 7, 8} {1, 2, 3, 4, 5, 9, 6, 8, 7} {1, 2, 3, 4, 5, 9, 7, 6, 8} {1, 2, 3, 4, 5, 9, 7, 8, 6} {1, 2, 3, 4, 5, 9, 8, 6, 7} {1, 2, 3, 4, 5, 9, 8, 7, 6} .... {9, 8, 7, 6, 5, 4, 3, 2, 1} That is, the entire set of permutations of the domain of all 9 variables participating in the constraint. What I've listed above is a *complete* Sudoku solver within the constraint-programming mindset. -------- In most of the 3SAT / SMT solvers for Sudoku I've seen, you set up the variables as: "X111, X112, X113, X114...", which means "X11 == 1", and "X11 == 2", etc. etc. So you then do "X111 + X112 + X113... X119 == 1", meaning "X11 is either 1, 2, 3, 4, 5... 9". Meanwhile, this entire process is simply "Domain of X11 = {1, 2, 3, 4, 5, 6, 7, 8, 9}" in the constraint-processing world, because variables can have arbitrarily sized (though finite) domains in constraint programming. That is to say, I'm pretty sure you need 999 == 729 variables to brute-force represent the problem in 3SAT / SMT? Meanwhile, Constraint Solver trivially represents it with 81-variables (but each of these 81 variables, X11 through X99, have a domain of size 9: {1, 2, 3, 4, 5, 6, 7, 8, 9}). There might be an easier way to represent Sudoku in 3SAT/SMT world, but again, I'm not very good with that world. I "just" know that 3SAT / SMT is a "similar but different" kind of solver and barely have used them. -------- One can argue that "constraint programming" is simply 3SAT / SMT-solving except with arbitrarily sized domains. Rather than solely using 0 and 1 or boolean functions. I've been told that "because everything is {0, 1}, more optimizations / inferences can be discovered" in 3SAT/SMT solvers compared to constraint programmers. Meanwhile, constraint programmers benefit from generic constraints that have a polynomial class subsolution (ie: using maximum flow, or other simpler algorithms to solve the subproblem). It'd take a rather well-studied expert to know whether 3SAT/SMT is better for a particular problem vs constraint-programming.

sacado2 4y ago
> I don't think you're correct on this issue? "x11 + x12 = 1" means that "x11 or x12 are 1, and the other is zero". and > In most of the 3SAT / SMT solvers for Sudoku I've seen, you set up the variables as: "X111, X112, X113, X114...", which means "X11 == 1", and "X11 == 2", etc. etc. So you then do "X111 + X112 + X113... X119 == 1", meaning "X11 is either 1, 2, 3, 4, 5... 9". Yes, I've been a bit to fast here. You're absolutely right. > I've been told that "because everything is {0, 1}, more optimizations / inferences can be discovered" in 3SAT/SMT solvers compared to constraint programmers. Meanwhile, constraint programmers benefit from generic constraints that have a polynomial class subsolution (ie: using maximum flow, or other simpler algorithms to solve the subproblem). Yes. SAT solvers very often outperform CSP solvers nowadays. But SAT solvers tend to lose the structure of the problem because they are so low-level. The most famous problem they fail to solve is the pigeonhole problem. If you have, say, the problem "is there a way to put 4 pigeons into 3 different holes, knowing that there can be at most 1 pigeon per hole and at least 1 hole per pigeon?", the answer is obviously "no", but if you try to use a propositional logic representation (in other words, using a SAT solver), the solving track will grow exponentially (4 vs 3 workds well, but SAT solvers will struggle to solve 11 vs 10 in a reasonable amount of time). Pseudo-boolean solvers will be able to using "cutting-planes" strategies that work well for this specific set of problems, but these are slower in the general case. Plus, modeling your problem in CNF to feed it to a SAT solver is usually incredibly complex and can lead to gigantic formulas if you're not careful. So most of the time, it really makes sense to first use a CSP representation, and fall back to a CNF representation if you're not satisfied with the results for some reason.