How to access why a clingo program is unsatisfiable

72 Views Asked by At

Is it possible for clingo to return the reasons why a given program is unsatisfiable?

For example the following code prints "UNSAT" but I would also like to get access to why.

from clingo.control import Control

program = """
blue("Bob").
-blue("Bob").
"""

ctl = Control()
ctl.add("base", [], program)
ctl.ground([("base", [])])

result = ctl.solve()

print(result)

I have seen in the docs that SolveHandle has a core method which was added following a related discussion (https://github.com/potassco/clasp/issues/59). However I can't quite work out how to use it.

My best guess is below but it prints an empty list, rather than indicating which rules/facts were in contradiction.

from clingo import SolveHandle
from clingo.control import Control

program = """
blue("Bob").
-blue("Bob").
"""

ctl = Control()
ctl.add("base", [], program)
ctl.ground([("base", [])])

assumptions = [x.literal for x in list(ctl.symbolic_atoms)]

result = ctl.solve(assumptions=assumptions, yield_=True)

if isinstance(result, SolveHandle):
    print(result.core())

Any help would be much appreciated

0

There are 0 best solutions below