Understanding SAT by Implementing a Simple SAT Solver in Python (2014)

Re:Understanding SAT by Implementing a Simple SAT Solver in ... by The_rationalist on Saturday August 31, 2019 @07:45AM (#20845759)

I am trying to implement a natural language (English) logic checker. It would detect 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)

[ Parent | on HN ]

Re:Understanding SAT by Implementing a Simple SAT Solver in ... by CJefferson on Saturday August 31, 2019 @08:17AM (#20845866)

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.

[ Parent | on HN ]

Re:Understanding SAT by Implementing a Simple SAT Solver in ... by The_rationalist on Saturday August 31, 2019 @12:27PM (#20847269)

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.

[ Parent | on HN ]

Re:Understanding SAT by Implementing a Simple SAT Solver in ... by zzz95 on Saturday August 31, 2019 @04:05PM (#20848509)

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

[ Parent | on HN ]