Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Improve API for non-satisfiable problems #33

Open
wants to merge 2 commits into
base: master
Choose a base branch
from

Conversation

barreeeiroo
Copy link

@barreeeiroo barreeeiroo commented May 18, 2023

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

When a problem cannot return any solution because of a given time limit, allow to still yield stats without providing any valid model.
Allows developers to gather information on why a valid solution could not be provided. It allows to differentiate a timeout (UNKNOWN) from an actual irresoluble problem (UNSATISFIABLE).
@barreeeiroo
Copy link
Author

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

1 participant