Undurchsichtige Validierung von LegalCNFConfig

[owestphal]

Die Aufgabe zum Erkennen wohlgeformter KNF ist in der Praxis äußerst umständlich zu konfigurieren.

Die Parameter minStringSize und maxStringSize scheinen nicht wirklich wählbar zu sein sonder müssen eher experimentell auf den richtigen Wert gesetzt werden.

Darüber hinaus gibt es die Fehlermeldung "Menge an Formeln ist zu groß. Eine Formeln könnte mehrfach generiert werden.", die keinerlei Informationen enthält, wie dieses Problem (welches ist das überhaupt?) behoben werden könnte.

[owestphal]

Eventuell steuern die Hinweise zur Konfiguration einen auch in eine sub-optimale Richtung. Zum Beispiel wollte ich folgede Konfiguration in eine vielfältigere Variante abwandeln:

LegalCNFConfig
  { cnfConfig = CnfConfig
      { baseConf = BaseConfig
          { minClauseLength = 2, maxClauseLength = 4, usedLiterals = "ABCD" }
      , minClauseAmount = 2
      , maxClauseAmount = 5
      }
  , formulas = 8
  , externalGenFormulas = 2
  , illegals = 2
  , includeFormWithJustOneClause = True
  , includeFormWithJustOneLiteralPerClause = True
  , maxStringSize = 50
  , minStringSize = 12
  , allowArrowOperators = False
  , extraText = Nothing
  }

Ein Hinzufügen von E zu den verwendeten Literalen führt zu "Nicht immer genug Platz für alle Literale in der Formel. (Mögliche Lösung: Eine der unteren Schranken erhöhen)".

Unvorsichtiges erhöhen von minClauseLength und minClauseAmount (z.B. beide +1) führt dann aber zu "Menge an Formeln ist zu groß. Eine Formeln könnte mehrfach generiert werden.".

Ehöhung von nur einer unteren Schranke, z.B. um 1, führt zu Problemen mit minStringSize, welche dann mind. 22 sein muss. Warum ist aus Sicht des Aufgabenstellers nicht nachvollziehbar.

[jvoigtlaender]

Der Punkt

Die Parameter minStringSize und maxStringSize scheinen nicht wirklich wählbar zu sein sonder müssen eher experimentell auf den richtigen Wert gesetzt werden.

ließe sich ja bestimmt dadurch adressieren, dass die entsprechenden config-Checker nicht einfach nur etwas in der Art sagen wie "minStringSize ist zu niedrig gesetzt", sondern "angesichts der Werte für minClauseAmount und ... müsste minStringSize mindestens 42 sein". Dann ist es weniger Trial-and-Error, sich an passende Werte heranzutasten.

[jvoigtlaender]

Man könnte auch überlegen, statt der "String-Größe" einen anderen Steuerungsparameter einzuführen. Allerdings ist nicht so recht klar, welcher das sein sollte. Für legale KNFs ist die String-Größe einfach ein Proxy für die Gesamtzahl der auftretenden Literale in der Formel. Also wenn etwa (minClauseAmount, maxClauseAmount) = (2,4) und auch (minClauseLength, maxClauseLength) = (2,4), dann könnte es ja in einer generierten KNF zwischen 4 und 16 Literalen geben. Wenn man das nicht so unbalanciert haben möchte (aber dennoch sowohl Fälle mit eher wenigen aber längeren Klauseln einerseits und Fälle mit eher mehr aber kürzeren Klauseln haben möchte), dann könnte man zusätzlich zu (minClauseAmount, maxClauseAmount) = (minClauseLength, maxClauseLength) = (2,4) noch etwas wie (minLiteralsAmount, maxLiteralsAmount) = (9,13) setzen. Das wäre vielleicht beim Konfigurieren sinnvoller zu interpretieren.

Aber das Problem damit ist, dass man diese Kontrolle auch über nicht-korrekte KNFs ausüben muss. Denn es werden in die Instanz ja am Ende zur Auswahl Dinge gepackt, die generiert wurden per:

• Tasks.LegalCNF.GenerateIllegal.genIllegalSynTree
• Formula.Types.genCnf
• Tasks.LegalCNF.GenerateLegal.genCnf

Und es wäre auffällig, wenn nur bei den legalen KNFs (wo sich leicht die Mengen durchzählen lassen, um das Maß "Anzahl der Literale" zu bestimmen) die Einschränkung erfolgt, bei den illegalen KNFs aber nicht analog. Und dort einfach auch die Literale (an Blättern des Baums) zu zählen, ist zumindest nicht offensichtlich ein "analoges Maß", einfach weil die Struktur der Formeln ja recht anders sein kann.

Jedoch "Länge des Strings" ist ein Maß, dass auf alle Fälle anwendbar ist, und auch wirklich einen Vergleich liefert, der zumindest oberflächlich der Idee "alle angebotenen Kandidaten sind einigermaßen gleich komplex" entspricht.

[jvoigtlaender]

Das mit der

Fehlermeldung "Menge an Formeln ist zu groß. Eine Formeln könnte mehrfach generiert werden.", die keinerlei Informationen enthält, wie dieses Problem (welches ist das überhaupt?) behoben werden könnte

und

Eventuell steuern die Hinweise zur Konfiguration einen auch in eine sub-optimale Richtung.

erfordert vielleicht einfach geeignete Präzisierungen in den Fehlermeldungen?