clyngor icon indicating copy to clipboard operation
clyngor copied to clipboard

Improve API for non-satisfiable problems

Open barreeeiroo opened this issue 1 year ago • 1 comments

Related to #32, I was playing around with clyngor a little bit more, and noticed that when a problem resolution times out, it actually generates some stats (if grounding took place). However, clyngor does not support this, because there was no difference from the API perspective on when a problem fails to return an answer because of being unsatisfiable or unknown (actual timeout).

This PR implements the following functionality:

  • Allows yielding stats on UNKNOWN status (basically, when resolution times out).
  • Allows developers to differentiate timeouts from unsatisfiable problems in the API.
models = clyngor.solve(inline="")
next(models) # It is needed to first iterate and try to search for a valid answer

assert models.is_unknown is True # is_unknown will be True if a timeout happens
assert models.is_unsatisfiable is True # is_unsatisfiable will be True if an unsatisfiable problem is provided

Note that it is impossible for both is_unknown and is_unsatisifiable to be True at the same time.
Also, statistics will be available on both statuses now.

Unit tests provided:

  • test_api::test_unsatisfiable: Now it also checks for both attributes.
  • test_api::test_unsatisfiable_statistics: Now it also checks for both attributes.
  • test_api::test_unknown: New test case using the Queens problem and a 1-second time limit to validate the unknown stats behaviour.
  • test_api::test_unknown_statistics: Like the previous one, but checking stats as well.
  • test_parsing::test_unknown: Checks the correct parsing and yielding of the UNKNOWN status.
  • test_parsing::test_unknown_statistics: Like the previous one, but checking that it yields stats when needed.

image

barreeeiroo avatar May 18 '23 14:05 barreeeiroo

While working on these changes, I noticed that some room for improvement: unify how result statuses are handled.

Here is the original source on the result status report from clasp: https://github.com/potassco/clasp/blob/17c4e466111c0b9da173f9097786a0d22b70e1c4/src/clasp_output.cpp#L638

As you can notice, it has 4 possible statuses:

  • UNKNOWN
  • UNSATISFIABLE
  • SATISFIABLE
  • OPTIMUM FOUND

The first two statuses are now available as an attribute to the Answers class. However, to differentiate and handle the last two, the OPTIMUM FOUND status is yielded with the answers iterator.
It would be interesting to provide an enum with those 4 statuses, then access it like models.result_status and remove the optimum_found yield. The problem is that removing this last variable would probably break some implementations though.

barreeeiroo avatar May 18 '23 14:05 barreeeiroo