+ As per usage examples, clause literals are a list of strings.
+ Note: symbols extracted from literals are expected to be exactly two characters.
+ self.literal boolean values are initialized to None, so must be optional
+ model values should be Booleans, but aren't guaranteed to be non-None
in the code.
+ uses newer '... | None' annotation for Optional values
+ clauses are passed to the Formula initializer as both lists and sets, they
are stored as lists. Returned clauses will always be lists.
+ use explicit tuple annotation from __future__ rather than using (..., ...)
in return signatures
+ mapping returned by dpll_algorithm is optional per the documentation.