Expand description
Boolean-logic simplification, normal forms, satisfiability. Boolean-logic simplification: flatten/absorb, CNF/DNF, satisfiability.
Boolean expressions are built from BoolTrue/BoolFalse, the
relational nodes Gt/Ge/Eq_/Ne (there are no Lt/Le nodes —
a < b is stored as Gt(b, a)), the connectives And/Or/Not,
and opaque atoms (anything else, e.g. a symbol used as a proposition).
§Relational atoms
Every relational atom is normalised to a pair (a, b) (numeric
literals on the right, otherwise sort-key order) plus a 3-bit mask
over the trichotomy
{a < b, a = b, a > b}. Negation is mask complement, conjunction of
two atoms on the same pair is mask intersection, disjunction is mask
union. This gives ¬(a < b) = a ≥ b, (x > 0) ∧ (x ≥ 0) = x > 0,
(x > 0) ∨ (x = 0) = x ≥ 0, (x > 0) ∧ (x < 0) = false and
(x > 0) ∨ (x ≤ 0) = true for free. The trichotomy assumes the
operands are real-valued, which is the domain of symplex’s relational
nodes and inequality solver.
Atoms whose two sides can be ordered (both numeric, exact difference,
or well-separated constants) are folded to true/false.
§Satisfiability
BoolEx::is_tautology,
BoolEx::is_contradiction and
BoolEx::satisfiable first try a
propositional search (each relational pair is a 3-valued variable, each
opaque atom a 2-valued one; ≤ 24 variables, bounded budget). A
propositional proof is always sound. When the propositional answer is
inconclusive and every atom is a relational in one and the same free
symbol, the question is decided exactly through the inequality solver
and set algebra (x > 1 → x > 0 is recognised as a tautology).
Otherwise the answer is None — never a guess.