In the code below
% Facts
a.
% Rules
-a :- a, not not p.
Adding the fact p. to the above would cause it to be UNSAT. Is there a way in clingo to add a rule to show this? Something like
q :- Assuming p causes UNSAT.
Solutions like adding the rule
{p; q} = 1.
Wouldn't work. It would give q. in the answer set if p. causes UNSAT, as I'd want. But, it would give p. and q. as answer sets when p. doesn't cause UNSAT. In the case of p. not causing UNSAT I wouldn't want q. in the answer set.
I'd like to be able to check whether certain facts causes a certain complex condition to not hold. For example, suppose one part of a problem requires you to check that a graph does NOT contain a Hamiltonian cycle. A program that finds Hamiltonian cycles would return UNSAT if the graph satisfies the condition, but I wouldn't want the program to end, since there would be other calculations to do.
You can probably treat it as an optimisation problem. So something that would normally be a constraint is turned into a special predicate which you then seek to minimise. Basically you have something of the form:
err(err1) :- some-bad-condition.
err(err2) :- some-other-bad-condition.
#minimize{ 1,XXX: err(XXX) }.
Here the XXX is a unique identifier for each error condition. The optimisation statement finds a model that minimises the number of errs.
The only caveat is that this increases the complexity of the problem; you're now solving an optimisation problem instead of a decision problem. It is a useful trick when debugging asp programs, but for large/difficult problems it may be too slow.