Unsatisfiable Constraints

Unsatisfiable constraints are the constraint rules that fire for an unsatisfiable ASP program. Identifying these can be very helpful for understanding why the program is unsatisfiable in particular in debugging scenarios. clingexplaid provides an easy way to find these for any given ASP program.

Finding Unsatisfiable Constraints

The following example shows how to find unsatisfiable constraints using clingexplaid.

from clingexplaid.unsat_constraints import UnsatConstraintComputer

PROGRAM = """
a(1..3).
{b(4..6)}.

a(X) :- b(X).

:- a(X), X>=3.
"""

ucc = UnsatConstraintComputer()
ucc.parse_string(PROGRAM)
unsat_constraints = ucc.get_unsat_constraints()

for uc_id, unsat_constraint in unsat_constraints.items():
    print(f"Unsat Constraint {uc_id}:", unsat_constraint)