Issue924

Title issues related to axioms and negative conditions
Priority meta Status chatting
Superseder Nosy List augusto, cedric, gabi, haz, jendrik, malte, salome, silvan
Assigned To Keywords translator
Optional summary
What needs to be done:
~~- Finish refactoring of axiom_rules.py (issue453).~~
~~- Try different options for axiom_rules.py (within issue453).~~
- Do something about the combinatorial explosion with the DNF conversion
  (e.g. issue450, issue111).
~~- Remove negated rules from the output and compute it in the search 
  component if needed (issue454).~~
- Remove axiom layers from the output and compute it in the search
  component if needed (issue978).
- Document that derived variables must be binary (issue54).
- Simplify axioms (issue161)
- See if the changes to the output format impact issue371.



Related issues and messages:
- issue54: non-binary derived variables currently not supported
- issue161: simplify axioms
- issue165: partly or fully the same thing as issue450 (see below)
- issue371: wishes for the output format
- issue450: negating axiom rules is implemented as a CNF-to-DNF conversion,
which can explode exponentially
- issue453: axiom semantics when negated are wrong because the idea of just
negating the formula that encodes the triggering conditions is semantically 
wrong
- issue454: about getting rid of negated axiom rules in the translator
- msg8204: explains the axiom code and contains notes and what could be improved
  (outdated after the merge of issue453)
- msg8235: lists which domains and search configurations are relevant when
dealing with the axioms
- issue98: support derived predicates properly in our heuristics
- issue111: Implement different ways to handle negative preconditions

Issues that have test cases that are important and we should consolidate:
- issue165
- issue450
- issue453
- issue862

Created on 2019-06-14.14:27:59 by malte, last changed by salome.

Summary
What needs to be done:
- Finish refactoring of axiom_rules.py (issue453).
- Try different options for axiom_rules.py (within issue453).
- Do something about the combinatorial explosion with the DNF conversion
  (e.g. issue450, issue111).
- Remove negated rules from the output and compute it in the search 
  component if needed (issue454).
- Remove axiom layers from the output and compute it in the search
  component if needed (issue978).
- Document that derived variables must be binary (issue54).
- Simplify axioms (issue161)
- See if the changes to the output format impact issue371.



Related issues and messages:
- issue54: non-binary derived variables currently not supported
- issue161: simplify axioms
- issue165: partly or fully the same thing as issue450 (see below)
- issue371: wishes for the output format
- issue450: negating axiom rules is implemented as a CNF-to-DNF conversion,
which can explode exponentially
- issue453: axiom semantics when negated are wrong because the idea of just
negating the formula that encodes the triggering conditions is semantically 
wrong
- issue454: about getting rid of negated axiom rules in the translator
- msg8204: explains the axiom code and contains notes and what could be improved
  (outdated after the merge of issue453)
- msg8235: lists which domains and search configurations are relevant when
dealing with the axioms
- issue98: support derived predicates properly in our heuristics
- issue111: Implement different ways to handle negative preconditions

Issues that have test cases that are important and we should consolidate:
- issue165
- issue450
- issue453
- issue862
Messages
msg11152 (view) Author: malte Date: 2023-07-21.14:34:32
Added issue111.
msg11149 (view) Author: malte Date: 2023-07-21.14:29:08
Add reference to issue98 and change title to also allow listing axiom issues in the search code.
msg9666 (view) Author: salome Date: 2020-07-22.13:37:19
I added a reference to several issues regarding axioms layers and translator output format that surfaced during the discussions in issue453.
msg8909 (view) Author: salome Date: 2019-06-14.18:22:31
Add option "overapproximate necessary literals" to the collection of options in
the summary
msg8905 (view) Author: malte Date: 2019-06-14.14:27:59
There is a tangled web of issues related to bugs related to axioms and negated
conditions. They have a somewhat messy overlap, so in this meta-issue we try to
introduce a bit of order and collect TODOs.
History
Date User Action Args
2024-07-19 13:27:30salomesetsummary: What needs to be done: ~~- Finish refactoring of axiom_rules.py (issue453).~~ ~~- Try different options for axiom_rules.py (within issue453).~~ - Do something about the combinatorial explosion with the DNF conversion (e.g. issue450, issue111). - Remove negated rules from the output and compute it in the search component if needed (issue454). - Remove axiom layers from the output and compute it in the search component if needed (issue978). - Document that derived variables must be binary (issue54). - Simplify axioms (issue161) - See if the changes to the output format impact issue371. Related issues and messages: - issue54: non-binary derived variables currently not supported - issue161: simplify axioms - issue165: partly or fully the same thing as issue450 (see below) - issue371: wishes for the output format - issue450: negating axiom rules is implemented as a CNF-to-DNF conversion, which can explode exponentially - issue453: axiom semantics when negated are wrong because the idea of just negating the formula that encodes the triggering conditions is semantically wrong - issue454: about getting rid of negated axiom rules in the translator - msg8204: explains the axiom code and contains notes and what could be improved (outdated after the merge of issue453) - msg8235: lists which domains and search configurations are relevant when dealing with the axioms - issue98: support derived predicates properly in our heuristics - issue111: Implement different ways to handle negative preconditions Issues that have test cases that are important and we should consolidate: - issue165 - issue450 - issue453 - issue862 -> What needs to be done: ~~- Finish refactoring of axiom_rules.py (issue453).~~ ~~- Try different options for axiom_rules.py (within issue453).~~ - Do something about the combinatorial explosion with the DNF conversion (e.g. issue450, issue111). ~~- Remove negated rules from the output and compute it in the search component if needed (issue454).~~ - Remove axiom layers from the output and compute it in the search component if needed (issue978). - Document that derived variables must be binary (issue54). - Simplify axioms (issue161) - See if the changes to the output format impact issue371. Related issues and messages: - issue54: non-binary derived variables currently not supported - issue161: simplify axioms - issue165: partly or fully the same thing as issue450 (see below) - issue371: wishes for the output format - issue450: negating axiom rules is implemented as a CNF-to-DNF conversion, which can explode exponentially - issue453: axiom semantics when negated are wrong because the idea of just negating the formula that encodes the triggering conditions is semantically wrong - issue454: about getting rid of negated axiom rules in the translator - msg8204: explains the axiom code and contains notes and what could be improved (outdated after the merge of issue453) - msg8235: lists which domains and search configurations are relevant when dealing with the axioms - issue98: support derived predicates properly in our heuristics - issue111: Implement different ways to handle negative preconditions Issues that have test cases that are important and we should consolidate: - issue165 - issue450 - issue453 - issue862
2024-06-26 05:45:32hazsetnosy: + haz
summary: What needs to be done: ~~- Finish refactoring of axiom_rules.py (issue453).~~ ~~- Try different options for axiom_rules.py (within issue453).~~ - Do something about the combinatorial explosion with the DNF conversion (e.g. issue450, issue111). - Remove negated rules from the output and compute it in the search component if needed (issue454). - Remove axiom layers from the output and compute it in the search component if needed (issue978). - Document that derived variables must be binary (issue54). - Simplify axioms (issue161) - See if the changes to the output format impact issue371. Related issues and messages: - issue54: non-binary derived variables currently not supported - issue161: simplify axioms - issue165: partly or fully the same thing as issue450 (see below) - issue371: wishes for the output format - issue450: negating axiom rules is implemented as a CNF-to-DNF conversion, which can explode exponentially - issue453: axiom semantics when negated are wrong because the idea of just negating the formula that encodes the triggering conditions is semantically wrong - issue454: about getting rid of negated axiom rules in the translator - msg8204: explains the axiom code and contains notes and what could be improved (outdated after the merge of issue453) - msg8235: lists which domains and search configurations are relevant when dealing with the axioms - issue98: support derived predicates properly in our heuristics - issue111: Implement different ways to handle negative preconditions Issues that have test cases that are important and we should consolidate: - issue165 - issue450 - issue453 - issue862 -> What needs to be done: ~~- Finish refactoring of axiom_rules.py (issue453).~~ ~~- Try different options for axiom_rules.py (within issue453).~~ - Do something about the combinatorial explosion with the DNF conversion (e.g. issue450, issue111). - Remove negated rules from the output and compute it in the search component if needed (issue454). - Remove axiom layers from the output and compute it in the search component if needed (issue978). - Document that derived variables must be binary (issue54). - Simplify axioms (issue161) - See if the changes to the output format impact issue371. Related issues and messages: - issue54: non-binary derived variables currently not supported - issue161: simplify axioms - issue165: partly or fully the same thing as issue450 (see below) - issue371: wishes for the output format - issue450: negating axiom rules is implemented as a CNF-to-DNF conversion, which can explode exponentially - issue453: axiom semantics when negated are wrong because the idea of just negating the formula that encodes the triggering conditions is semantically wrong - issue454: about getting rid of negated axiom rules in the translator - msg8204: explains the axiom code and contains notes and what could be improved (outdated after the merge of issue453) - msg8235: lists which domains and search configurations are relevant when dealing with the axioms - issue98: support derived predicates properly in our heuristics - issue111: Implement different ways to handle negative preconditions Issues that have test cases that are important and we should consolidate: - issue165 - issue450 - issue453 - issue862
2023-07-21 14:34:32maltesetmessages: + msg11152
summary: What needs to be done: ~~- Finish refactoring of axiom_rules.py (issue453).~~ ~~- Try different options for axiom_rules.py (within issue453).~~ - Do something about the combinatorial explosion with the DNF conversion (e.g. issue450). - Remove negated rules from the output and compute it in the search component if needed (issue454). - Remove axiom layers from the output and compute it in the search component if needed (issue978). - Document that derived variables must be binary (issue54). - Simplify axioms (issue161) - See if the changes to the output format impact issue371. Related issues and messages: - issue54: non-binary derived variables currently not supported - issue161: simplify axioms - issue165: partly or fully the same thing as issue450 (see below) - issue371: wishes for the output format - issue450: negating axiom rules is implemented as a CNF-to-DNF conversion, which can explode exponentially - issue453: axiom semantics when negated are wrong because the idea of just negating the formula that encodes the triggering conditions is semantically wrong - issue454: about getting rid of negated axiom rules in the translator - msg8204: explains the axiom code and contains notes and what could be improved (outdated after the merge of issue453) - msg8235: lists which domains and search configurations are relevant when dealing with the axioms - issue98: support derived predicates properly in our heuristics Issues that have test cases that are important and we should consolidate: - issue165 - issue450 - issue453 - issue862 -> What needs to be done: ~~- Finish refactoring of axiom_rules.py (issue453).~~ ~~- Try different options for axiom_rules.py (within issue453).~~ - Do something about the combinatorial explosion with the DNF conversion (e.g. issue450, issue111). - Remove negated rules from the output and compute it in the search component if needed (issue454). - Remove axiom layers from the output and compute it in the search component if needed (issue978). - Document that derived variables must be binary (issue54). - Simplify axioms (issue161) - See if the changes to the output format impact issue371. Related issues and messages: - issue54: non-binary derived variables currently not supported - issue161: simplify axioms - issue165: partly or fully the same thing as issue450 (see below) - issue371: wishes for the output format - issue450: negating axiom rules is implemented as a CNF-to-DNF conversion, which can explode exponentially - issue453: axiom semantics when negated are wrong because the idea of just negating the formula that encodes the triggering conditions is semantically wrong - issue454: about getting rid of negated axiom rules in the translator - msg8204: explains the axiom code and contains notes and what could be improved (outdated after the merge of issue453) - msg8235: lists which domains and search configurations are relevant when dealing with the axioms - issue98: support derived predicates properly in our heuristics - issue111: Implement different ways to handle negative preconditions Issues that have test cases that are important and we should consolidate: - issue165 - issue450 - issue453 - issue862
2023-07-21 14:29:08maltesettitle: translator issues related to axioms and negative conditions -> issues related to axioms and negative conditions
messages: + msg11149
summary: What needs to be done: ~~- Finish refactoring of axiom_rules.py (issue453).~~ ~~- Try different options for axiom_rules.py (within issue453).~~ - Do something about the combinatorial explosion with the DNF conversion (e.g. issue450). - Remove negated rules from the output and compute it in the search component if needed (issue454). - Remove axiom layers from the output and compute it in the search component if needed (issue978). - Document that derived variables must be binary (issue54). - Simplify axioms (issue161) - See if the changes to the output format impact issue371. Related issues and messages: - issue54: non-binary derived variables currently not supported - issue161: simplify axioms - issue165: partly or fully the same thing as issue450 (see below) - issue371: wishes for the output format - issue450: negating axiom rules is implemented as a CNF-to-DNF conversion, which can explode exponentially - issue453: axiom semantics when negated are wrong because the idea of just negating the formula that encodes the triggering conditions is semantically wrong - issue454: about getting rid of negated axiom rules in the translator - msg8204: explains the axiom code and contains notes and what could be improved (outdated after the merge of issue453) - msg8235: lists which domains and search configurations are relevant when dealing with the axioms Issues that have test cases that are important and we should consolidate: - issue165 - issue450 - issue453 - issue862 -> What needs to be done: ~~- Finish refactoring of axiom_rules.py (issue453).~~ ~~- Try different options for axiom_rules.py (within issue453).~~ - Do something about the combinatorial explosion with the DNF conversion (e.g. issue450). - Remove negated rules from the output and compute it in the search component if needed (issue454). - Remove axiom layers from the output and compute it in the search component if needed (issue978). - Document that derived variables must be binary (issue54). - Simplify axioms (issue161) - See if the changes to the output format impact issue371. Related issues and messages: - issue54: non-binary derived variables currently not supported - issue161: simplify axioms - issue165: partly or fully the same thing as issue450 (see below) - issue371: wishes for the output format - issue450: negating axiom rules is implemented as a CNF-to-DNF conversion, which can explode exponentially - issue453: axiom semantics when negated are wrong because the idea of just negating the formula that encodes the triggering conditions is semantically wrong - issue454: about getting rid of negated axiom rules in the translator - msg8204: explains the axiom code and contains notes and what could be improved (outdated after the merge of issue453) - msg8235: lists which domains and search configurations are relevant when dealing with the axioms - issue98: support derived predicates properly in our heuristics Issues that have test cases that are important and we should consolidate: - issue165 - issue450 - issue453 - issue862
2020-07-22 13:37:20salomesettitle: translator bugs related to axioms and negative conditions -> translator issues related to axioms and negative conditions
messages: + msg9666
summary: What needs to be done: - Finish refactoring of axiom_rules.py (issue453). - Try different options for axiom_rules.py (within issue453): - overapproximate negated axioms: 1) current way (negate = buggy), 2) trivially overapproximate; 3) trivially overapproximate for cycles, negate when there are no cycles - keep redundant positive axioms: yes/no (=> in the medium term, we would like to always have the positive form as the "real" form) - layers: use minimum number of layers (as currently) or maximum number of layer (=> in the medium term, we probably only want to decide on one of these two) - overapproximate necessary literals: 1) full relevance analysis 2) consider all non-derived literals as necessary 3) old implementation (The old implementation considered all positive literals as necessary, which is wrong but usually works well. Ideally we will decide between 1 and 3 or keep 1 and 3 as options) - Do something about the combinatiorial explosion with the DNF conversion (e.g. issue450). Related issues and messages: - issue165: partly or fully the same thing as issue450 (see below) - issue450: negating axiom rules is implemented as a CNF-to-DNF conversion, which can explode exponentially - issue453: axiom semantics when negated are wrong because the idea of just negating the formula that encodes the triggering conditions is semantically wrong - issue454: about getting rid of negated axiom rules in the translator - msg8204: explains the axiom code and contains notes and what could be improved - msg8235: lists which domains and search configurations are relevant when dealing with the axioms Issues that have test cases that are important and we should consolidate: - issue165 - issue450 - issue453 - issue862 -> What needs to be done: ~~- Finish refactoring of axiom_rules.py (issue453).~~ ~~- Try different options for axiom_rules.py (within issue453).~~ - Do something about the combinatorial explosion with the DNF conversion (e.g. issue450). - Remove negated rules from the output and compute it in the search component if needed (issue454). - Remove axiom layers from the output and compute it in the search component if needed (issue978). - Document that derived variables must be binary (issue54). - Simplify axioms (issue161) - See if the changes to the output format impact issue371. Related issues and messages: - issue54: non-binary derived variables currently not supported - issue161: simplify axioms - issue165: partly or fully the same thing as issue450 (see below) - issue371: wishes for the output format - issue450: negating axiom rules is implemented as a CNF-to-DNF conversion, which can explode exponentially - issue453: axiom semantics when negated are wrong because the idea of just negating the formula that encodes the triggering conditions is semantically wrong - issue454: about getting rid of negated axiom rules in the translator - msg8204: explains the axiom code and contains notes and what could be improved (outdated after the merge of issue453) - msg8235: lists which domains and search configurations are relevant when dealing with the axioms Issues that have test cases that are important and we should consolidate: - issue165 - issue450 - issue453 - issue862
2019-06-14 18:22:31salomesetmessages: + msg8909
summary: What needs to be done: - Finish refactoring of axiom_rules.py (issue453). - Try different options for axiom_rules.py (within issue453): - overapproximate negated axioms: 1) current way (negate = buggy), 2) trivially overapproximate; 3) trivially overapproximate for cycles, negate when there are no cycles - keep redundant positive axioms: yes/no (=> in the medium term, we would like to always have the positive form as the "real" form) - layers: use minimum number of layers (as currently) or maximum number of layer (=> in the medium term, we probably only want to decide on one of these two) - Do something about the combinatiorial explosion with the DNF conversion (e.g. issue450). Related issues and messages: - issue165: partly or fully the same thing as issue450 (see below) - issue450: negating axiom rules is implemented as a CNF-to-DNF conversion, which can explode exponentially - issue453: axiom semantics when negated are wrong because the idea of just negating the formula that encodes the triggering conditions is semantically wrong - issue454: about getting rid of negated axiom rules in the translator - msg8204: explains the axiom code and contains notes and what could be improved - msg8235: lists which domains and search configurations are relevant when dealing with the axioms Issues that have test cases that are important and we should consolidate: - issue165 - issue450 - issue453 - issue862 -> What needs to be done: - Finish refactoring of axiom_rules.py (issue453). - Try different options for axiom_rules.py (within issue453): - overapproximate negated axioms: 1) current way (negate = buggy), 2) trivially overapproximate; 3) trivially overapproximate for cycles, negate when there are no cycles - keep redundant positive axioms: yes/no (=> in the medium term, we would like to always have the positive form as the "real" form) - layers: use minimum number of layers (as currently) or maximum number of layer (=> in the medium term, we probably only want to decide on one of these two) - overapproximate necessary literals: 1) full relevance analysis 2) consider all non-derived literals as necessary 3) old implementation (The old implementation considered all positive literals as necessary, which is wrong but usually works well. Ideally we will decide between 1 and 3 or keep 1 and 3 as options) - Do something about the combinatiorial explosion with the DNF conversion (e.g. issue450). Related issues and messages: - issue165: partly or fully the same thing as issue450 (see below) - issue450: negating axiom rules is implemented as a CNF-to-DNF conversion, which can explode exponentially - issue453: axiom semantics when negated are wrong because the idea of just negating the formula that encodes the triggering conditions is semantically wrong - issue454: about getting rid of negated axiom rules in the translator - msg8204: explains the axiom code and contains notes and what could be improved - msg8235: lists which domains and search configurations are relevant when dealing with the axioms Issues that have test cases that are important and we should consolidate: - issue165 - issue450 - issue453 - issue862
2019-06-14 14:29:45silvansetnosy: + silvan
2019-06-14 14:27:59maltecreate