Support for tagging constraints?

[greg-gelfond]

Are there any plans to allow for tagging of constraints to allow us to see which constraints were violated and therefore see why a program might be unsatisfiable?

[bramucas]

Hi @greg-gelfond,

indeed, from version 2.0b14 onwards (the latest today is 2.0b17) that feature is already included.

If called from the command line, xclingo will only automatically use the feature when the result is UNSAT: after finding that the problem is UNSAT, the tagged constraints will be relaxed (a.k.a. an auxiliary head is written for tagged constraints). xclingo then runs again, but this time will try to explain (only) those auxiliary atoms.

Of course, this means it will only work for tagged constraints. If no constraint is tagged, xclingo won't try to explain a UNSAT problem.

A (very simple) example:

% example.lp
% The annotations syntax of this example corresponds to version 2.0b17
a. b.
c :- a,b.
%!trace_rule {"constraint was violated"}.
:- c.

The output after calling xclingo -n 0 0 example.lp --auto-tracing=all is:

xclingo version 2.0b17
Reading from kk
UNSATISFIABLE
Relaxing constraints... (mode=minimize)
Answer: 1
##Explanation: 1.1
  *
  |__"constraint was violated";_xclingo_violated_constraint(3,())
  |  |__c
  |  |  |__a
  |  |  |__b

##Total Explanations:   1
Models: 1

This can also be done directly (without the first UNSAT call) if done through the Python package API. I can also inform you on how to do that if you are interested.

Thank you for your interest 😁.

[greg-gelfond]

Does the constraint tagging only support a subset of the allowed syntax for constraints? For example, I can't obtain explanations for this program:

p(a).
p(b).

%!trace_rule {"There can only be at most on value satisfying p"}
:- #count{ X : p(X) } > 1.

[greg-gelfond]

Oh - I see, I'm running xclingo 2.0b12.

[greg-gelfond]

Actually @bramucas running xclingo 2.0b14 still shows no explanations when I use the cardinality constraint. Similarly, if I use this program:

p(a).
p(b).

%!trace_rule {"There can only be at most one value satisfying p"}
:- p(X), p(Y), X != Y.

No explanations are given.

[bramucas]

Hi @greg-gelfond,

if you are playing with that feature, I recommend installing the latest beta. Just typing python -m pip install xclingo==2.0b17 should do the trick.

Regarding the syntax for the oldest versions: yes, it has changed.

If you navigate to the develop branch in the repository, you will find updated examples in the examples folder. I leave here this link that goes directly there.

In short words, now all the annotations have a similar syntax to theory atoms. Therefore, you have to keep in mind that they behave the same as any other ASP thing:

1.They must end with a dot ..
2. Head and body of any %!trace or %!show_trace annotation is separated by :-.
3. Variables must be safe
4. etc.

If you just add a dot at the end of the %!trace_rule annotation in your code:
I also added some variables to see the effect

%greg_issue.lp
p(a).
p(b).

%!trace_rule {"There can only be at most one value satisfying p | p(%), p(%)", X, Y}.
:- p(X), p(Y), X != Y.

then run xclingo -n 0 0 greg_issue.lp and you should get:

xclingo version 2.0b17
Reading from kk
UNSATISFIABLE
Relaxing constraints... (mode=minimize)
Answer: 1
##Explanation: 1.1
  *
  |__"There can only be at most one value satisfying p | p(b), p(a)"

  *
  |__"There can only be at most one value satisfying p | p(a), p(b)"

##Total Explanations:   1
Models: 1

Please let me know if you need more help 😀😀.

[greg-gelfond]

Hello again @bramucas. It seems that I found a bug in the current beta (version xclingo 2.0b17). I'm using the drunk driving example program:

person(gabriel;clare).

drive(gabriel).
alcohol(gabriel, 40).
resist(gabriel).

drive(clare).
alcohol(clare, 5).

%!trace_rule {"% drove drunk", P}.
punish(P) :- drive(P), alcohol(P,A), A>30, person(P).

%!trace_rule {"% resisted to authority", P}.
punish(P) :- resist(P), person(P).

%!trace_rule {"% goes to prison",P}.
sentence(P, prison) :- punish(P).

%!trace_rule {"% is innocent by default",P}.
sentence(P, innocent) :- person(P), not punish(P).

%!trace {alcohol(P,A), "% alcohol's level is %",P,A} :- alcohol(P,A).
%!trace {alcohol(P,A), "% was drunk",P} :- alcohol(P,A).

%!show_trace {sentence(P,S)} :- sentence(P,S).
#show sentence/2.

Here is the output exception I get when running the command xclingo -n 0 0 on the program:

xclingo version 2.0b17
Reading from drunk-driving.lp
Traceback (most recent call last):
  File "/Users/gregory/Projects/UDRI/ASP/xclingo/xclingo/bin/xclingo", line 8, in <module>
    sys.exit(main())
             ^^^^^^
  File "/Users/gregory/Projects/UDRI/ASP/xclingo/xclingo/lib/python3.11/site-packages/xclingo/__main__.py", line 195, in main
    ground_solve_explain(args, unknown_args, programs)
  File "/Users/gregory/Projects/UDRI/ASP/xclingo/xclingo/lib/python3.11/site-packages/xclingo/__main__.py", line 157, in ground_solve_explain
    xclingo_control = _init_xclingo_control(args, unknown_args, programs)
                      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/Users/gregory/Projects/UDRI/ASP/xclingo/xclingo/lib/python3.11/site-packages/xclingo/__main__.py", line 54, in _init_xclingo_control
    xclingo_control.add("base", [], program)
  File "/Users/gregory/Projects/UDRI/ASP/xclingo/xclingo/lib/python3.11/site-packages/xclingo/_main.py", line 72, in add
    name, parameters, self.pre_explaining_pipeline.translate(name, program)
                      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/Users/gregory/Projects/UDRI/ASP/xclingo/xclingo/lib/python3.11/site-packages/xclingo/preprocessor/_pipeline.py", line 20, in translate
    translation = p.process_program(translation)
                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/Users/gregory/Projects/UDRI/ASP/xclingo/xclingo/lib/python3.11/site-packages/xclingo/preprocessor/_preprocessor.py", line 64, in process_program
    parse_string(
  File "/Users/gregory/Projects/UDRI/ASP/xclingo/xclingo/lib/python3.11/site-packages/clingo/ast.py", line 1322, in parse_string
    _handle_error(
  File "/Users/gregory/Projects/UDRI/ASP/xclingo/xclingo/lib/python3.11/site-packages/clingo/_internal.py", line 71, in _handle_error
    raise handler.error[0](handler.error[1]).with_traceback(handler.error[2])
  File "/Users/gregory/Projects/UDRI/ASP/xclingo/xclingo/lib/python3.11/site-packages/clingo/ast.py", line 1210, in _pyclingo_ast_callback
    callback(AST(ast))
  File "/Users/gregory/Projects/UDRI/ASP/xclingo/xclingo/lib/python3.11/site-packages/xclingo/preprocessor/_preprocessor.py", line 66, in <lambda>
    lambda ast: self._add_to_translation(self.preprocess_rule(ast)),
                ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/Users/gregory/Projects/UDRI/ASP/xclingo/xclingo/lib/python3.11/site-packages/xclingo/preprocessor/_preprocessor.py", line 45, in _add_to_translation
    for ra in rule_asts:
  File "/Users/gregory/Projects/UDRI/ASP/xclingo/xclingo/lib/python3.11/site-packages/xclingo/preprocessor/_preprocessor.py", line 264, in preprocess_rule
    for r in self.translate_rule(rule_id, 0, rule_ast.head, rule_ast.body):
  File "/Users/gregory/Projects/UDRI/ASP/xclingo/xclingo/lib/python3.11/site-packages/xclingo/preprocessor/_preprocessor.py", line 200, in translate_rule
    for translated_rule in self._support_translator.translate(
  File "/Users/gregory/Projects/UDRI/ASP/xclingo/xclingo/lib/python3.11/site-packages/xclingo/preprocessor/_translator.py", line 87, in translate
    yield self._rule(
          ^^^^^^^^^^^
  File "/Users/gregory/Projects/UDRI/ASP/xclingo/xclingo/lib/python3.11/site-packages/xclingo/preprocessor/xclingo_ast/_xclingo_ast.py", line 137, in __init__
    super().__init__(**kwargs)
  File "/Users/gregory/Projects/UDRI/ASP/xclingo/xclingo/lib/python3.11/site-packages/xclingo/preprocessor/xclingo_ast/_xclingo_ast.py", line 111, in __init__
    super().__init__(**kwargs)
  File "/Users/gregory/Projects/UDRI/ASP/xclingo/xclingo/lib/python3.11/site-packages/xclingo/preprocessor/xclingo_ast/_xclingo_ast.py", line 89, in __init__
    super().__init__(func_name=_SUP_HEAD, **kwargs)
  File "/Users/gregory/Projects/UDRI/ASP/xclingo/xclingo/lib/python3.11/site-packages/xclingo/preprocessor/xclingo_ast/_xclingo_ast.py", line 80, in __init__
    [rule_id, disjunction_id, head, list(collect_free_vars(body))],
                                    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/Users/gregory/Projects/UDRI/ASP/xclingo/xclingo/lib/python3.11/site-packages/xclingo/preprocessor/xclingo_ast/_ast_shortcuts.py", line 123, in collect_free_vars
    if lit.atom.left.ast_type == ASTType.Variable:
       ^^^^^^^^^^^^^
  File "/Users/gregory/Projects/UDRI/ASP/xclingo/xclingo/lib/python3.11/site-packages/clingo/ast.py", line 970, in __getattr__
    raise AttributeError(f"no attribute: {name}")
AttributeError: no attribute: left

In addition, here is the current list of pip packages I have (if it helps):

Package                   Version
------------------------- --------
attrs                     23.1.0
cffi                      1.16.0
clingo                    5.6.2
clingraph                 1.1.1
Clorm                     1.4.2
graphviz                  0.20.1
importlib-resources       6.1.0
Jinja2                    3.1.2
jsonschema                4.19.1
jsonschema-specifications 2023.7.1
MarkupSafe                2.1.3
networkx                  3.1
pip                       23.2.1
pycparser                 2.21
referencing               0.30.2
rpds-py                   0.10.4
setuptools                68.2.2
wheel                     0.41.2
xclingo                   2.0b17

[bramucas]

Hi @greg-gelfond,

The compatibility with clingo 5.6 is not finished yet. Try downgrading clingo to 5.5 and see if it fixes it.
python -m pip install 'clingo<5.6' should do the trick.

I would bet it's that. If the error persists, then yes 🎉🎉 we have found something new haha.

[greg-gelfond]

Thanks! That seems to have resolved the issue.

…

-- Gregory Gelfond ***@***.***

On Tue, Oct 10, 2023, at 5:52 AM, Brais Muñiz Castro wrote: Hi @greg-gelfond <https://github.com/greg-gelfond>, The compatibility with clingo 5.6 is not finished yet. Try downgrading `clingo` to 5.5 and see if it fixes it. `python -m pip install 'clingo<5.6'` should do the trick. I would bet it's that. If the error persists, then yes 🎉🎉 we have found something new haha. — Reply to this email directly, view it on GitHub <#12 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AUSEZPZFODRZXE6AU65TQCLX6USFTAVCNFSM6AAAAAA5TAFNVCVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTONJVGAZDOMBUGM>. You are receiving this because you were mentioned.Message ID: ***@***.***>

[greg-gelfond]

@bramucas - out of curiosity, is it possible to only output explanations pertaining to violated constraints if the program has no answer sets? The current example I'm working with prints out all of the explanations, and not just the ones pertaining to constraint violations.

[bramucas]

That is planned to be included in further versions ✌️.

The plan is to suppress non-constraint-related explanations when explaining a UNSAT result but also to include a flag that the user could use to check the rest of the explanations.

I'll prioritize that given that you are interested. I'll let you know when it's available.