3

I'm currently learning how to prove the unsatisfiability of first-order logic. I've learnd in my class that resolution is one way to solve the unsatisfiability problem, e.g., tools like Prolog achieve this by implementing SLDNF resolution to try to find contradiction (empty clause).

Recently I've found the topic of answer set programming (ASP) and that the implemention tools like Clingo can also solve the unsatisfiability problem.

So I'm confused with how the problem is solved in ASP. I'm sure the mechanism is quite different from logic programming. For me, it seems that what an ASP solver does is to enumerate all the possibilities until a satisfying model is found. Is this true? And is there any advantage of this method over resolution? Thanks!

Li Danyuan
  • 121
  • 8

1 Answers1

2

ASP is logic programming as well - but it is pure declarative whereas most prolog languages have a lot of imperative elements.
The idea (as far as I understood) is in principle to find a model, meaning a set of predicates which are True and is consistent with the rules of the program. The model property can be checked in polytime (through reduction), so the hard part is to "guess" a potential model.

An imperative programming language could possibly iterate trough all possible model candidates - and as far as I understood - this is what clingo does BUT it uses several shortcuts and other mechanics to do this way more efficient (see DPLL SAT solver). If you think of it as a search tree you can easily skip huge sub-trees if you know that these do not lead to a model.

So for an unsatifiable program ASP can be interpreted of building a search tree but every leaf formulates assumptions which violate rules of the logic program.

DuDa
  • 3,718
  • 4
  • 16
  • 36