Solving a formula, which is connected to various rationality criteria, currently is done using a multitude of strategies. However, the classes taupy.Debate, taupy.Argument and taupy.Position do not have attribute to account for the underlying logic. This needs to change now that the approach to run simulation experiments with three-valued formulas appear more and more promising.

Currently available tools in taupy:

• binary decision diagrams via dd, very good for #SAT of Boolean (two-valued) debates, but relatively slow for checking whether a given formula is SAT (because the decision tree has to be initialised first). Multi-valued diagrams (MDDs) are an abstraction of BDDs that could, in principle, work for three or n-valued Boolean formulas, but no implementation of MDDs in Python is known. BDDs are used in taupy.satisfiability() and taupy.satisfiability_count().
• the classic DPLL algorithm via sympy, very bad for #SAT, but very good for checking whether any given Boolean formula is SAT. This function is imported from sympy, stored at dpll_satisfiable() in the modules that need it.
• the optimised z3 heuristics for #SAT (taupy.z3_all_models()), general SAT checks (using the z3.Solver class) and MaxSAT (using the z3.Optimize class). z3 can be used to check partial two-valued positions, but one can also implement other logics in z3, and then z3 could be used for partial positions that suspend! (big step forward, at least theoretically)

It does not seem to be advisable to use z3 for all purposes. Instances of z3 objects can be quite tricky to handle, causing problems with multi-processing (which ideally would be preserved, since this currently seems necessary to enlarge the sentence pool toward 30 or beyond). More research needed here on how to best integrate z3 objects!

Todo list:

• Abstraction in Debate, Argument, Position and Simulation classes to account for different logics
• A new KleeneanSolver class to handle formulas and models from Kleenean logic (I think I have settled for Kleene in favour of Ł3, but it shouldn't be too difficult to implement Ł3 as well.)

The group-based polarisation measures currently run on networkx Graph objects. When moving to python-igraph and scikit-learn, group-based polarisation measures should be calculated using numpy matrices only. This will be much faster and will provide a common framework for algorithms from igraph and scikit.