Created on 20190614.14:27:59 by malte, last changed by salome.
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, issue1152).
 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: nonbinary 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
 issue1152: negating axiom rules is implemented as a CNFtoDNF conversion,
which can explode exponentially (formerly issue450)
 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
 issue1153: implement an exact computation for axioms from derived variables
with cycles
Issues that have test cases that are important and we should consolidate:
 issue165
 issue450
 issue453
 issue862
 issue1155

msg11152 (view) 
Author: malte 
Date: 20230721.14:34:32 

Added issue111.

msg11149 (view) 
Author: malte 
Date: 20230721.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: 20200722.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: 20190614.18:22:31 

Add option "overapproximate necessary literals" to the collection of options in
the summary

msg8905 (view) 
Author: malte 
Date: 20190614.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 metaissue we try to
introduce a bit of order and collect TODOs.


Date 
User 
Action 
Args 
20241002 13:43:39  salome  set  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, issue1152).
~~ 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: nonbinary 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
 issue1152: negating axiom rules is implemented as a CNFtoDNF conversion,
which can explode exponentially (formerly issue450)
 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
 issue1153: implement an exact computation for axioms from derived variables
with cycles
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, issue1152).
~~ 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: nonbinary 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
 issue1152: negating axiom rules is implemented as a CNFtoDNF conversion,
which can explode exponentially (formerly issue450)
 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
 issue1153: implement an exact computation for axioms from derived variables
with cycles
Issues that have test cases that are important and we should consolidate:
 issue165
 issue450
 issue453
 issue862
 issue1155 
20240917 16:23:23  calittle  set  nosy:
+ calittle 
20240917 15:50:01  simon  set  nosy:
+ simon 
20240917 15:25:31  salome  set  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: nonbinary 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 CNFtoDNF 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, issue1152).
~~ 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: nonbinary 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
 issue1152: negating axiom rules is implemented as a CNFtoDNF conversion,
which can explode exponentially (formerly issue450)
 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
 issue1153: implement an exact computation for axioms from derived variables
with cycles
Issues that have test cases that are important and we should consolidate:
 issue165
 issue450
 issue453
 issue862 
20240719 13:27:30  salome  set  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: nonbinary 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 CNFtoDNF 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: nonbinary 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 CNFtoDNF 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 
20240626 05:45:32  haz  set  nosy:
+ 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: nonbinary 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 CNFtoDNF 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: nonbinary 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 CNFtoDNF 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 
20230721 14:34:32  malte  set  messages:
+ 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: nonbinary 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 CNFtoDNF 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: nonbinary 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 CNFtoDNF 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 
20230721 14:29:08  malte  set  title: 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: nonbinary 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 CNFtoDNF 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: nonbinary 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 CNFtoDNF 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 
20200722 13:37:20  salome  set  title: 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 nonderived 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 CNFtoDNF 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: nonbinary 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 CNFtoDNF 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 
20190614 18:22:31  salome  set  messages:
+ 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 CNFtoDNF 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 nonderived 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 CNFtoDNF 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 
20190614 14:29:45  silvan  set  nosy:
+ silvan 
20190614 14:27:59  malte  create  
