More general formulas for `Pick`, `Fill` and `Decide`

[nimec01]

First steps towards an implementation for #98

[nimec01]

I just stumbled upon the pickCnf option in PickConfig. What is its meaning? It's not getting used, apparently.

[jvoigtlaender]

I've looked into the distant past. There once was this code:

genPickExercise :: PickConfig -> IO (String,Either ([(Int,Cnf)],Table) ([(Int,Table)],Cnf))
genPickExercise
    PickConfig {cnfConfig = CnfConfig {clauseConf = ClauseConfig {..}, ..}, ..}
  = do
    first <- generate (getCnf usedLiterals)
    let satForm = convert first
    rest <- generate (vectorOf (amountOfOptions-1) (getWithSameLiterals first satForm))
    let cnfs = first : rest
    rightCnf <- generate (elements cnfs)
    if pickCnf
      then do
        let
          table = getTable rightCnf
          zippedCnfs = zip [1..] cnfs
          desc = exerciseDescPick2 zippedCnfs table
        pure (desc,Left (zippedCnfs,table))
      else do
        let
          tables = zip [1..] (map getTable cnfs)
          desc = exerciseDescPick tables rightCnf
        pure (desc,Right (tables,rightCnf))
  where
    getCnf :: [Char] -> Gen Cnf
    getCnf lits = genCnf (minClauseAmount, maxClauseAmount) (minClauseLength, maxClauseLength)
                     lits

    getWithSameLiterals :: Cnf -> Sat.Formula Char -> Gen Cnf
    getWithSameLiterals cnf sat = do
        let cnfLits = getLiterals cnf
        newCnf <- getCnf (map getC cnfLits)
        if getLiterals newCnf == cnfLits && Sat.satisfiable (sat Sat.:++: convert newCnf)
          then pure newCnf
          else getWithSameLiterals cnf sat

exerciseDescPick :: [(Int,Table)] -> Cnf -> String
exerciseDescPick tables cnf =
    "Betrachten Sie die folgende Formel in konjunktiver Normalform: \n\n" ++
    show cnf ++
    "\n Welche der folgenden Wahrheitstafeln passt zu der Formel?\n\n" ++
    showIndexedList tables ++
    "\nGeben Sie die richtige Tafel durch ihre Nummer an."

exerciseDescPick2 :: [(Int,Cnf)] -> Table -> String
exerciseDescPick2 cnfs table =
    "Betrachten Sie die folgende Wahrheitstafel: \n\n" ++
    show table ++
    "\n Welche der folgenden Formeln in konjunktiver Normalform passt zu der Wahrheitstafel?\n\n" ++
    showIndexedList cnfs ++
    "\nGeben Sie die richtige Tafel durch ihre Nummer an."

So it looks like at some point that parameter was used to decide whether to let the student choose one of three formulas for one given truth table, or one of three truth tables for one given formula.

Wheras by now only one of these modes is still supported, I guess.

[nimec01]

PickConfig definitely needs more constraints (probably in regard to whether amountOfOptions is achievable with a given minAmountOfUniqueAtoms).

Here are some problematic examples:

PickConfig {
  syntaxTreeConfig = SynTreeConfig {
    minNodes = 8, 
    maxNodes = 9, 
    minDepth = 4, 
    maxDepth = 4, 
    availableAtoms = "FGIKLSUVWXYZ", 
    minAmountOfUniqueAtoms = 2, 
    allowArrowOperators = False, 
    maxConsecutiveNegations = 2, 
    minUniqueBinOperators = 1}, 
  amountOfOptions = 5, 
  pickCnf = False, 
  printSolution = False, 
  extraText = Nothing
}

-- fails to fill these shapes with "FKV" such that the formulas are not semantically equivalent
[
  Binary And (Binary And (Not (Leaf ())) (Binary Or (Leaf ()) (Leaf ()))) (Leaf ()),
  Binary And (Not (Leaf ())) (Binary And (Not (Leaf ())) (Not (Leaf ()))),
  Binary And (Binary And (Not (Leaf ())) (Not (Leaf ()))) (Not (Leaf ())),
  Binary And (Binary And (Leaf ()) (Binary And (Leaf ()) (Leaf ()))) (Binary Or (Leaf ()) (Leaf ())),
  Binary Or (Not (Leaf ())) (Binary Or (Binary Or (Leaf ()) (Leaf ())) (Not (Leaf ())))
]

-- same here with "DZ"
PickConfig {
  syntaxTreeConfig = SynTreeConfig {
    minNodes = 6, 
    maxNodes = 12, 
    minDepth = 3, 
    maxDepth = 4, 
    availableAtoms = "ABDEFGJKRSTVXZ", 
    minAmountOfUniqueAtoms = 2, 
    allowArrowOperators = True, 
    maxConsecutiveNegations = 2, 
    minUniqueBinOperators = 1}, 
  amountOfOptions = 5, 
  pickCnf = False, 
  printSolution = False, 
  extraText = Nothing
}

[
  Binary And (Not (Not (Leaf ()))) (Binary And (Binary Equi (Leaf ()) (Leaf ())) (Not (Leaf ()))),
  Binary Or (Leaf ()) (Binary Impl (Not (Leaf ())) (Binary Or (Leaf ()) (Leaf ()))),
  Not (Binary Or (Binary And (Leaf ()) (Leaf ())) (Binary Or (Leaf ()) (Leaf ()))),
  Binary And (Leaf ()) (Not (Binary And (Leaf ()) (Leaf ()))),
  Binary Impl (Not (Leaf ())) (Not (Not (Leaf ())))
]

[jvoigtlaender]

Concerning this aspect:

PickConfig definitely needs more constraints (probably in regard to whether amountOfOptions is achievable with a given minAmountOfUniqueAtoms).

I think I am foremost surprised that the amount of literals to be used is not part of the config anymore. That is, in your problematic example configurations, there appear

fails to fill these shapes with "FKV"

and

same here with "DZ"

but the fact that in one case an attempt is made to use exactly three literals, and in the other case exactly two literals, is not informed by the original config.

Even apart from any problems with generation/termination etc., this seems problematic, that the lecturer would have no control over this aspect. After all, it will have a large impact on the size of the task shown to students. A truth table over three literals is twice as big as one over two literals. So, we can't have one student get one, another student the other, from the same task configuration. (And secondarily, without a configuration parameter controlling the exact number of atoms, one cannot use that number in expressing constraints that try to guarantee successful instance generation.)

I guess in the previous version of this task type, this control is present via the usedLiterals option in https://github.com/fmidue/logic-tasks/blob/15bfef2a5fd7abdd0be69c94d006ba26634fd1fe/src/Config.hs#L180-L184 (I assume, but am not sure right now without looking through the code, that this usedLiterals is really an "exactly those must occur" parameter, unlike the availableAtoms and minAmountOfUniqueAtoms parameters in SynTreeConfig.)

[nimec01]

PickConfig now requires that length availableAtoms == minAmountOfUniqueAtoms. The change also allowed me to simplify genPickInst (the trees will always have the same atoms; I don't have to use this https://github.com/fmidue/logic-tasks/pull/124#discussion_r1562553791 approach).

We might also want to add percentTrueEntries to PickConfig to prevent formulas being valid or unfulfillable (that is possible right now and makes some instances very easy to solve).

[jvoigtlaender]

We might also want to add percentTrueEntries to PickConfig to prevent formulas being valid or unfulfillable (that is possible right now and makes some instances very easy to solve).

Yes, this addition seems reasonable. Maybe also for the Decide task?

And following a discussion from further above, remove pickCnf?

[jvoigtlaender]

PickConfig now requires that length availableAtoms == minAmountOfUniqueAtoms

Shouldn't this also be done for the Fill and Decide tasks?

These previously used genCnf (minClauseAmount, maxClauseAmount) (minClauseLength, maxClauseLength) usedLiterals, and I assume the usedLiterals argument made sure that exactly those literals are used. But that constraint is not currently captured in the reimplementations using genSynTree.

[nimec01]

PickConfig now requires that length availableAtoms == minAmountOfUniqueAtoms

Shouldn't this also be done for the Fill and Decide tasks?

These previously used genCnf (minClauseAmount, maxClauseAmount) (minClauseLength, maxClauseLength) usedLiterals, and I assume the usedLiterals argument made sure that exactly those literals are used. But that constraint is not currently captured in the reimplementations using genSynTree.

I added percentTrueEntries to all three tasks. Pick has some problems with that. My guess is that there are cases where percentTrueEntries is in conflict with the bounds of syntaxTreeConfig.

[nimec01]

Pick has some problems with that. My guess is that there are cases where percentTrueEntries is in conflict with the bounds of syntaxTreeConfig.

Nowadays, I don't think that it is related to syntaxTreeConfig. Otherwise, Fill and Decide would also be suffering from that. I think it's the interaction between amountOfOptions and percentTrueEntries. My guess is that it could be impossible to find amountOfOptions different formulas that satisfy the given percentTrueEntries.

If that's the case, we would probably need to:

• add more checks for PickConfig
• update the test cases so that more realistic configs are used

Here are some example configs that are problematic:

PickConfig {
  syntaxTreeConfig = SynTreeConfig {
    minNodes = 29, 
    maxNodes = 30, 
    minDepth = 5, 
    maxDepth = 5, 
    availableAtoms = "AEFHIJKORTUVXZ", 
    minAmountOfUniqueAtoms = 14, 
    allowArrowOperators = False, 
    maxConsecutiveNegations = 3, 
    minUniqueBinOperators = 2},
  amountOfOptions = 4, 
  percentTrueEntries = Just (72,78), 
  printSolution = False, 
  extraText = Nothing
 }

PickConfig {
  syntaxTreeConfig = SynTreeConfig {
    minNodes = 38, 
    maxNodes = 53, 
    minDepth = 6, 
    maxDepth = 9, 
    availableAtoms = "AEGKMNOUVWXZ", 
    minAmountOfUniqueAtoms = 12, 
    allowArrowOperators = True, 
    maxConsecutiveNegations = 3, 
    minUniqueBinOperators = 4}, 
  amountOfOptions = 3, 
  percentTrueEntries = Just (64,67), 
  printSolution = False, 
  extraText = Nothing
}

(There are also configs with wider percentTrueEntries ranges)

[jvoigtlaender]

(There are also configs with wider percentTrueEntries ranges)

How wide? Such extremely narrow ranges as above are really more a "because the config type allows it" rather than "we might have a pedagogical reason to want to be so specific".

In practice, I can hardly think of ever wanting anything else than one of the following ranges:

• (0, 100)
• (0, 30)
• (0, 50)
• (50, 100)
• (70, 100)
• (35, 65)

So if a config check that the difference between the two borders is at least 30 would solve the issue (in the sense of "no problems ever anymore in practice, even though we don't have a formal proof of that"), then I would say go with that.

[nimec01]

So if a config check that the difference between the two borders is at least 30 would solve the issue (in the sense of "no problems ever anymore in practice, even though we don't have a formal proof of that"), then I would say go with that.

This works. The tests are still a bit slow, though.

[jvoigtlaender]

This is finished now, implementation-wise of the "new kind of formula usage"?

It would remain to adapt the example tasks, then.

On reflection now, I have come to wonder whether it wouldn't be better to not outright replace the old generation of CNFs with generation of arbitrary syntax trees, but instead offer it only as an alternative.

One reason is to still be able to use all old task configurations essentially unchanged (and maybe only gradually switch over to more general configurations). That might also address this point to some extent (https://github.com/fmidue/logic-tasks/issues/98#issue-2111880442):

Das könnte natürlich noch weitere Änderungen nach sich ziehen, etwa weil bestimmte Eigenschaften für die sinnvolle Aufgabenerzeugung (gleiche Schwierigkeit o.ä.), die sich bei KNFs "von selbst ergeben", nun noch separat betrachtet werden müssten.

We would always have the old kind of tasks around (for which we somehow believe that they are fair in terms of difficulty etc.), but could also do some new versions, and observe what happens. There might also be indeed didactic reasons to definitely use a CNF in some tasks (developing some understanding of special ways of evaluating CNFs, MinTerms vs. MaxTerms, etc.).

Implementation-wise it would probably mostly mean to sprinkle various Either, Left, Right occurrences throughout the current code, and reinstate certain code lines that are currently deleted.

Once one is at that, though, one might also wonder whether one shouldn't go the full way and offer three options to the user here:

• generate CNFs
• generate DNFs
• generate arbitrary formulas

[jvoigtlaender]

The tests are still a bit slow, though.

The slowness might to some extent come from this: https://github.com/fmidue/logic-tasks/blob/a5c55ee998b70a00e1ca32e81e67c066ca540a29/src/LogicTasks/Semantics/Pick.hs#L37-L38 creating the full vector and only then checking for "uniqueness" of entries. That is, if amountOfOptions = 10 and the first two trees generated are semantically equivalent, nevertheless the other eight trees are also generated and only after that the whole vector generation starts over.

I guess it would make sense to write a more efficient helper vectorOfUniqueBy :: Int -> (a -> a -> Bool) -> Gen a -> Gen [a] and use that here.

[nimec01]

I guess it would make sense to write a more efficient helper vectorOfUniqueBy :: Int -> (a -> a -> Bool) -> Gen a -> Gen [a] and use that here.

I could not really perceive any decrease in the duration, but there is no harm in implementing it anyway.

[nimec01]

Once one is at that, though, one might also wonder whether one shouldn't go the full way and offer three options to the user here:

• generate CNFs
• generate DNFs
• generate arbitrary formulas

I will probably just go ahead and implement it this way.

[nimec01]

This is not quite finished yet. I will have another look at it the next days.