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