3 ms·

No, not really. A SAT solver checks if there's a model in which a formula is true, while this program checks if the formula is true in every model. It's believe

by jkabrg 8y ago

No, not really. A SAT solver checks if there's a model in which a formula is true, while this program checks if the formula is true in every model. It's believed that there's no efficient reduction from one to the other, because otherwise NP=coNP.

vilhelm_s 8y ago
However, modern sat-solvers do both. That is, although they are called "sat-solvers", they can actually output both "sat" and "unsat". In software verification they are used for the "unsat" side: you produce a logical formula P stating that your software is correct, and then you ask the sat-solver about ¬P. Hopefully it returns "unsat", meaning that it has proved P is true; otherwise it will return a satisfying assignment, which is a counterexample to your proposed theorem. So I guess you could say that a theorem prover for propositional logic, like Logic Theorist, is "half" of a modern solver like Z3, it can produce proofs but not counterexamples. :)
leeeeech 8y ago
What does that look like? A SAT problem takes a bunch of unknown variables (v_1, v_2 ... V_n) and logic operators (''not, and, or'' for example would be enough) to form a formula that combines these operators and variables, to asks us for an assignment (traditionally ''true'' or ''false'') to each variable respectively, so that the formula is satisfied; For example given the rules of sudoku find a filled sudoku. Or for xx+nx+m=0, and a given n and m, find x. Then what is the model theoretic problem? Is it, if f(a,b)=((a and not b) or (b and not a)) is satisfied by e.g. (a=1,b=0), then we want to know all configs that satisfy it? The way I understand your post, you are saying we want to know if all combinations of a and b over {0, 1} satisfy the formula. I'm not sure that's not the same thing from a different perspective. I started a course on abstract algebra once, but actually I am still limited to boolean logic. while they mentioned Galois Theory, functions as points in a metric space, graph coloring problems and many things that sound interesting but quickly have me getting lost in details. It's the same effect as with other machine learning ... coff coff.

by jkabrg 8y ago

vilhelm_s 8y ago

However, modern sat-solvers do both. That is, although they are called "sat-solvers", they can actually output both "sat" and "unsat". In software verification they are used for the "unsat" side: you produce a logical formula P stating that your software is correct, and then you ask the sat-solver about ¬P. Hopefully it returns "unsat", meaning that it has proved P is true; otherwise it will return a satisfying assignment, which is a counterexample to your proposed theorem. So I guess you could say that a theorem prover for propositional logic, like Logic Theorist, is "half" of a modern solver like Z3, it can produce proofs but not counterexamples. :)

leeeeech 8y ago

What does that look like? A SAT problem takes a bunch of unknown variables (v_1, v_2 ... V_n) and logic operators (''not, and, or'' for example would be enough) to form a formula that combines these operators and variables, to asks us for an assignment (traditionally ''true'' or ''false'') to each variable respectively, so that the formula is satisfied; For example given the rules of sudoku find a filled sudoku. Or for xx+nx+m=0, and a given n and m, find x. Then what is the model theoretic problem? Is it, if f(a,b)=((a and not b) or (b and not a)) is satisfied by e.g. (a=1,b=0), then we want to know all configs that satisfy it? The way I understand your post, you are saying we want to know if all combinations of a and b over {0, 1} satisfy the formula. I'm not sure that's not the same thing from a different perspective. I started a course on abstract algebra once, but actually I am still limited to boolean logic. while they mentioned Galois Theory, functions as points in a metric space, graph coloring problems and many things that sound interesting but quickly have me getting lost in details. It's the same effect as with other machine learning ... coff coff.