Skip to content

Conversation

@JNAOB
Copy link
Collaborator

@JNAOB JNAOB commented Mar 28, 2025

CLOSE #219

Neues Feld negLiteralRatio in NormalFormConfig steuert den prozentualen Anteil der negativen Literale in der Formel.

Neue Funktionen:

  • genCnfWithRatio
  • genDnfWithRatio

Bereits integriert in genCnf' und genDnf'.

Der angegebene Anteil wird an den nächstmöglichen Anteil angenähert, damit immer eine Formel generiert werden kann, die die Bedingung erfüllt. Beispielsweise eine Formel mit 9 Literalen und einem gewünschten Anteil von 30 % wird auf 1/3 (≈ 33  %) geprüft.

Ist der angegebene Anteil außerhalb des Intervalls [0, 1], wird eine zufällige Formel generiert.

@jvoigtlaender
Copy link
Member

jvoigtlaender commented Mar 28, 2025

Vielleicht sollte statt eines exakten Verhältnisses mit einem Range gearbeitet werden. Analog zu

, percentTrueEntries :: Maybe (Int,Int)

Dann würde sich die Notwendigkeit des "Snappens" erübrigen.

Es müsste dann vielleicht sichergestellt werden (durch Überprüfung im Config-Checker), dass besagter Range nicht zu klein gewählt wird (so dass schlimmstenfalls gar kein Wert innerhalb des Ranges möglich ist; bin mir gerade nicht sicher, ob bei den percentTrueEntries auf diesen Aspekt geachtet wird).

Gegebenenfalls wäre Verwendung (nach geeigneter Generalisierung) von für Verwendung mit percentTrueEntries bereits existierenden Hilfsfunktionen wie withRatio möglich.

@jvoigtlaender
Copy link
Member

Aside: #275

@JNAOB
Copy link
Collaborator Author

JNAOB commented Mar 31, 2025

Das Verhältnis wird jetzt über ein Intervall gesteuert.

genericWithRatio ist eine Weiterentwicklung von withRatio, wegen zyklischer Imports aber in Formula.Types und nicht in Util.

Siehe hier

Statt (Int, Int) wird RatioMode benutzt, um zu bestimmen, welches Verhältnis geprüft werden soll.

data RatioMode = ByPositiveLiterals (Int, Int) | ByTruthValues (Int, Int) deriving (Show)

@JNAOB
Copy link
Collaborator Author

JNAOB commented Apr 1, 2025

Es müsste dann vielleicht sichergestellt werden (durch Überprüfung im Config-Checker), dass besagter Range nicht zu klein gewählt wird (so dass schlimmstenfalls gar kein Wert innerhalb des Ranges möglich ist; bin mir gerade nicht sicher, ob bei den percentTrueEntries auf diesen Aspekt geachtet wird).

Ich denke, die Range kann nicht zu klein sein. Durch die Verwendung von percentage wird auf eine Ganzzahl abgerundet, die erreichbar ist. Hier habe ich percentage aus withRatio übernommen, demnach sollte das auch schon für percentTrueEntries gelten.

percentage :: Int -> Int
percentage num = n *num `div` 100

Damit ist die untere Grenze immer kleiner gleich der oberen Grenze, solange die Werte in der Range aufsteigend sind. Im schlimmsten Fall ist demnach die obere Grenze und die untere Grenze gleich, was dem vorherigen Fall mit dem konkreten Verhältnis entspricht. Es muss also nur darauf geachtet werden, dass die Range zwischen 0 und 100 ist und die erste Zahl kleiner gleich die zweite Zahl ist.

Nur die Bennenung mit percentage ist vielleicht etwas irreführend, da hier ja keine wirkliche Prozentzahl ausgerechnet wird, sondern nur die Anzahl an Klammern/Wahrheitswerten, um die Prozentzahl zu erreichen.

@jvoigtlaender
Copy link
Member

Okay, also die Sorge

Also etwa: es gibt 16 Zeilen in der Wahrheitstafel; es wird verlangt, dass zwischen 2 und 3 Prozent der Einträge True sind; aber unter den Zahlen 0 bis 16 gibt es keine, die genau zwischen 2 und 3 Prozent von 16 liegt.

aus #275 trifft nicht in genau der Form zu, sondern die 2 und 3 Prozent von 16 würden beide auf 0 abgerundet und dann nach einer Formel gesucht, in der genau 0 Einträge True sind.

Ergo könnte das "schlimmstenfalls gar kein Wert innerhalb des Ranges [existent]" nicht eintreten, aber ein "besagter Range zu klein" bzw. "schlimmstenfalls gar kein Wert innerhalb des Ranges möglich" durchaus, im Sinne, dass es vielleicht (wegen anderer Constraints) gar nicht möglich ist, eine Formel zu erwürfeln, die immer zu False auswertet. Wenn dem so ist, müsste "2 bis 3 Prozent bei 16 Einträgen" eben doch verboten werden, damit die Suche nach einer alle Constraints erfüllenden Formel nicht scheitert.

@jvoigtlaender
Copy link
Member

Eine mögliche "Heuristik" wäre (hier und in #275), die Größe der "Grundgesamtheit" (im Beispiel die Zahl 16) mit heranzuziehen bei der Beurteilung (im Config-Checker), ob ein gewisses Intervall zugelassen werden soll; und dann zu fordern, dass die Auswahl zwischen mindestens zwei verschiedene Werten besteht. (Etwa: bei 16 darf man (10,20) als Prozentintervall wählen, da die beiden Zahlen 2 und 3 zwischen 10% von 16 und 20% von 16 liegen. Und in der Tat finde ich, dass dann withRatio in dem Fall auch wirklich nur 2 und 3 akzeptieren sollte, nicht auch "1 weil 10% von 16 abgerundet 1 ergibt".)


import Data.List(intercalate, delete, nub, transpose, (\\))
import Data.List(intercalate, delete, nub, transpose, (\\)) -- minimumBy
-- import Data.Ord(comparing)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Solche Zeilen/Diff-Anteile könnten noch weg. Auch weiter unten.


class Formula a where
literals :: a -> [Literal]
duplicateLiterals :: a -> [Literal]
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Irgendwie habe ich das Gefühl, dass die API hier nicht gut ist, wenn wir sowohl literals als auch duplicateLiterals im Angebot haben.

Das eine ist ja immer eine "Obermenge" (bzw. eben Multimenge) des anderen.

Wie wäre es mit einem Refactoring:

  • Es gibt nur noch eine von den beiden Funktionen; sie heißt literals aber hat die Semantik des duplicateLiterals.
  • An allen vorherigen Stellen, an denen literals verwendet wurde, wird ein Aufruf von nub (oder nubOrd oder nubSort, was gerade passt) hinzugefügt. Bzw. auf ihn kann auch verzichtet werden, wenn klar ist, dass an der Stelle keine Duplikate vorliegen können (etwa wegen der konkreten Art von Formula, auf der dort literals aufgerufen wurde) oder das Vorliegen von Duplikaten kein Problem wäre (zum Beispiel falls die Liste nur auf Leerheit getestet wird oder so).

-- The used atomic formulas are drawn from the list of chars.
-- The ratio must be between 0 and 1; otherwise, it will be ignored.
genCnfWithPercentRange :: PercentRangeMode -> (Int,Int) -> (Int,Int) -> [Char] -> Bool -> Gen Cnf
genCnfWithPercentRange percentPosLiterals (minNum,maxNum) (minLen,maxLen) atoms enforceUsingAllLiterals = do
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Der Variablenname percentPosLiterals hier ist merkwürdig, da der PercentRangeMode ja auch anders ausgeprägt sein könnte.

Tritt bei mindestens einer anderen Funktion unten nochmal auf.

-- | Generates a random dnf satisfying the given bounds
-- for the amount and the length of the contained conjunctions.
-- for the amount and the length of the contained conjunctions,
-- as well as the ratio of negative literals.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Isn't it positive literals that are constrained now?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Auch anderswo falsch beschrieben.


-- | Generates a random dnf satisfying the given bounds
-- for the amount and the length of the contained conjunctions.
-- The used atomic formulas are drawn from the list of chars.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Wurden hier die Dokumentationen von genDnf und genDnfWithPercentRange verwechselt?

let
allLiterals = duplicateLiterals form
posLiterals = filter isPositive allLiterals
in (length posLiterals, length allLiterals, bounds)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ich fürchte, dass ich nicht ganz verstehe, wie das hier funktioniert bzw. ob es korrekt ist.

Zum Beispiel wundert mich, dass die Variable posLiteralsNumber in dem einen Fall an length trueEntries gebunden wird. Das scheint mir unlogisch.

@JNAOB JNAOB marked this pull request as draft November 7, 2025 12:29
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Verhältnis positiver und negativer Literale bei Formelgenerierung steuern lassen

3 participants