1 Hi.

I’m Mars. I write a lot of code and I like to think I’m good at math.

I like minimalism. Can you tell?

I really like Atkinson Hyperlegible. Please consider using it!

My favorite color scheme is Gruvbox Material. It’s what this site is themed with… assuming you’re not messing with the CSS.

It highly annoys me when people write “alot” instead of “a lot,” “too” when they mean “to,” or “loose” when they mean “lose.”

2 Website to-do

3 Algebra Cube

4 Monoidal Category

A monoidal category is a category with the morphisms

The monoidal product is also known as the tensor product.

and isomorphisms

A mnemonic for the names of the unitors is left for lambda and right for rho.

This is just a fancy way of saying that the monoidal product is associative and passes through values on either operand when the other operand is the identity object.

4a Backlinks

5 Rhizomatic thinking

Rhizomatic thought is thinking that sporadically networks different ideas orthogonally to conceptual hierarchies (aka arborescent thought).

Rhizomatic Arborescent
entity-component-system (ECS) object-oriented programming
tagged filesystems directory hierarchies
Zettelkasten Johnny Decimal
relational databases document stores
There’s more to the concept but I’m doing other things at time of writing. Read the Wikipedia page for more info.

6 Monad

A monad is a monoid in the category of endofunctors.

7 Resolution

Given some variable :

Also note that due to the law of the excluded middle, resolution on two or more opposing variable assignments is a tautology:

The resolution rule itself is monotonic: every clause inferred through resolution is merely implied by the two clauses it’s constructed from. Therefore, assuming no means of eliminating subsumed clauses, the resolution rule as a means of inferring new clauses is valid if resolved clauses are directly added back to the set of known clauses.

7a Backlinks

8 Assignment power sets

Given some variables , , and , the set of possible refuting clauses for each partial assignment listed below is shown:

In other words, for any partial assignment, the set of clauses that can prove unsatisfiability of that partial assignment is the power set of that partial assignment’s negation. Therefore, any partial solution to a satisfiability problem can be disproven by finding a clause that contains only a subset of its negated literals.

Because the fixpoint resolution predicate can find all clauses that are logical consequences of other clauses, proving a partial assignment is satisfiable is equivalent to proving that the power set of the negated assignment is disjoint with .

We also have an inductive means of constructing complete power sets:

9 Fixpoint resolution

Defining a fixpoint ruleset for an instance using the resolution rule and first-order Horn clauses:

We can reframe this ruleset for non-empty clauses in terms of any literal :

and for the empty clause:

Note that for the latter rule:

  1. The empty clause rule is complete for SAT because it is equivalent to evaluating the Davis-Putnam satisfiability procedure.
  2. Because the empty clause rule is equivalent to DP, it is exponential in memory.
  3. Querying the satisfiability of the empty clause is unreachable by querying for a non-empty clause.

9a Backlinks

10 Endofunctor

An endofunctor is just a functor from a category to itself.

Given a category , an endofunctor can be defined as .

As in: “Endofunctor? I hardly know her!”

10a Backlinks

11 The satisfiability problem

The Boolean satisfiability problem is a fundamental problem in computer science, logic, and artificial intelligence. For a satisfiability instance, it asks whether there exists an assignment of truth values to the Boolean variables in the instance such that all propositional constraints in the instance are met.

11a Overview

I express satisfiability instances with the opaque identifier .

Every satisfiability instance has a set of variables , which represent the unique propositional variables in the instance.

We support the usual Boolean operators , , and for variables. An important rule is the law of double negation:

We can express the sets of positive and negative literals for :

Then combine them to obtain the total set of unique literals :

So far, we’ve expressed the domain of propositional satisfiability instances, but not their constraining clauses :

Each clause represents a disjunction of literals. The set of clauses represents the conjunctive normal form (CNF) of the constraints. Notably, all Boolean expressions can be expressed as CNF clauses using techniques such as the Tseitin transformation or repeat application of De Morgan’s laws.

Conjunctive normal form is also known as sum of products (SOP).

To solve the satisfiability problem for our instance , we attempt to find an assignment .

An assignment satisfies a clause if:

And the assignment satisfies if:

Summing up, the full satisfiability problem for is:

11b Clauses as “at least one”

Because all clauses in a satisfiability instance are disjunctions of literals, one way of conceptualizing a clause is as an “at least one” constraint.

11c Partial assignments

In the domain of SAT solving, we also often think about partial assignments:

11d Tautologies

For any clause , we say that is a tautology if:

Because tautologies are always satisfiable and yield no information about the satisfiability of an instance, we typically omit tautologies from problems.

11e Clause negation

A notational trick I use is to negate every literal in a clause using the operator.

12 Monoid

A monoid is an object within a monoidal category with the morphisms

such that

commutes given the identity morphism .

Alternative interpretations of monoids:

Examples of monoids:

Category Operation Identity
natural numbers addition 0
natural numbers multiplication 1
Boolean algebras
Boolean algebras
sets

12a Backlinks