3 ms·

SAT is best when there is one true logical answer. ANN are best when you want "best advice". A good guide (in my experience) -- with SAT while the answer is ha

SAT is best when there is one true logical answer. ANN are best when you want "best advice". A good guide (in my experience) -- with SAT while the answer is hard to find it's easy to check (like a Sudoku, or building a timetable with no clashes), while ANN give answers where verifying the answer isn't easy to perform computstionally (if I give you a translation of a text into Latin, verifying it is about as hard as just making a new one from scratch)

The_rationalist 7y ago
I am trying to implement a natural language (English) logic checker. It would detect https://en.m.wikipedia.org/wiki/Formal_fallacy https://en.m.wikipedia.org/wiki/Formal_fallacy How could a SAT/SMT help me in this task? I know it's already used for math theorem checking. E.g All men are mortal. Socrates is a man. Therefore Socrate is mortal. I have currently two way to solve syllogisms One hard-coded Disjonction of cases (but not flexible enough for non canonical forms of syllogisms) And a flexible one that generate a graph of transitivity. Both are 100% accurate. Could SAT/SMT give me a third way of determining if the conclusion is logically valid? (not non sequitur)
- CJefferson 7y ago
  This is exactly what SAT and SMT are for. SMT is some extra stuff on top of SAT. There are a few frameworks which extend SAT. I'd look at minizinc, it is a fairly easy to use language which can produce SAT (and SMT, and others) as output. Often encoding things in SAT directly gets arkward.
  - The_rationalist 7y ago
    Thank you but as you say, encoding is limiting. SMT are a progress versus SAT. But I believe I would need an SMT that take a graph and rules as input and verify if the graph or parts of the graph satisfy the rules/constraints. And output me the indexes of the satisfied parts of the graph. I believe such a thing does not yet exist.
    - zzz95 7y ago
      This is what model checkers are for. They internally (might) use SAT solvers to reason over transition graphs. The general problem for model checkers is of this form: System description: Transition system like automata or a guarded command language which induces a graph. System Property: Stated in some logic, CTL/LTL Output: Satisfied, or Unsatisfied with a counter example (usually a path in the graph which is false). If your problem can fit into such a framework, have a look at model checkers: https://en.wikipedia.org/wiki/List_of_model_checking_tools https://en.wikipedia.org/wiki/List_of_model_checking_tools
phonicwheel 7y ago
There are also probabilistic SAT solvers for cases where there isn't just one true logical answer, e.g., https://github.com/MatthiasNickles/delSAT https://github.com/MatthiasNickles/delSAT

The_rationalist 7y ago

I am trying to implement a natural language (English) logic checker. It would detect https://en.m.wikipedia.org/wiki/Formal_fallacy https://en.m.wikipedia.org/wiki/Formal_fallacy How could a SAT/SMT help me in this task? I know it's already used for math theorem checking. E.g All men are mortal. Socrates is a man. Therefore Socrate is mortal. I have currently two way to solve syllogisms One hard-coded Disjonction of cases (but not flexible enough for non canonical forms of syllogisms) And a flexible one that generate a graph of transitivity. Both are 100% accurate. Could SAT/SMT give me a third way of determining if the conclusion is logically valid? (not non sequitur)

CJefferson 7y ago
This is exactly what SAT and SMT are for. SMT is some extra stuff on top of SAT. There are a few frameworks which extend SAT. I'd look at minizinc, it is a fairly easy to use language which can produce SAT (and SMT, and others) as output. Often encoding things in SAT directly gets arkward.
- The_rationalist 7y ago
  Thank you but as you say, encoding is limiting. SMT are a progress versus SAT. But I believe I would need an SMT that take a graph and rules as input and verify if the graph or parts of the graph satisfy the rules/constraints. And output me the indexes of the satisfied parts of the graph. I believe such a thing does not yet exist.
  - zzz95 7y ago
    This is what model checkers are for. They internally (might) use SAT solvers to reason over transition graphs. The general problem for model checkers is of this form: System description: Transition system like automata or a guarded command language which induces a graph. System Property: Stated in some logic, CTL/LTL Output: Satisfied, or Unsatisfied with a counter example (usually a path in the graph which is false). If your problem can fit into such a framework, have a look at model checkers: https://en.wikipedia.org/wiki/List_of_model_checking_tools https://en.wikipedia.org/wiki/List_of_model_checking_tools

phonicwheel 7y ago

There are also probabilistic SAT solvers for cases where there isn't just one true logical answer, e.g., https://github.com/MatthiasNickles/delSAT https://github.com/MatthiasNickles/delSAT