Thread Reader
Robin Piedeleu

Robin Piedeleu

Nov 24
8 tweets

Our MFPS paper *A Complete Diagrammatic Calculus for Boolean Satisfiability*, with Fabio Zanasi and Tao Gu is on the arXiv:

In it, we give a presentation of the symmetric monoidal category of monotone relations over the Booleans, and argue that the resulting diagrammatic language is best understood as *the algebra of Boolean satisfiability* (SAT).
Why isn't Boolean algebra the algebra of SAT? Well, satisfiability is about *the existence* of solutions to systems of Boolean equations. The implicit existential quantifier in the definition of SAT takes it beyond the algebraic theory of Boolean algebras.
Otoh, the diagrammatic calculus we propose has existential quantification baked into it, since composition is interpreted via existential quantification (i.e., as composition in the category of relations).
SAT instances in conjunctive normal form have a natural representation: white nodes are clauses (disjunctions of literals) and black nodes take care of variable management (copying & discarding as usual). Note that the direction of the wires keep track of the polarity of literals
For ex, ∃x∃y(¬x∨y)∧(x∨y)∧(x∨¬y)∧(¬x∨¬y) is depicted as follows, w/ the 2 looped wires represent x and y, the rest encode the 4 clauses, from top to bottom: (¬x∨y) is the 1st wire, (x ∨ y) the 1st white dot, (x∨ ¬y) the middle wire, and (¬x∨¬y) the bottom white dot.
Resolution solvers (basic DPLL or CDCL for example) have a natural interpretation as certain rewrites on diagrams. The ex. above can be shown unsatisfiable as follows, with the last diagram represent the degenerate unsatisfiable clause 1≤0.
(For the initiated, the equational engine of resolution proofs is really the Frobenius law)
Robin Piedeleu

Robin Piedeleu

boxes-and-wires scientist
Follow on Twitter
Missing some tweets in this thread? Or failed to load images or videos? You can try to .