Wiki

Factorization over a finite field by linear algebra: the map v to v^p - v is linear on F_p[x]/(f), and the dimension of its kernel is exactly the number of irreducible factors. That count is worth having on its own, as a check on the gcd-based algorithms that shares none of their code.

A representation chosen so that mathematically equal objects are structurally identical. Once expressions have one, deciding equality is a comparison rather than a search, and a zero test is a look at the representation rather than an attempt to prove an identity. It is the property every layer of a CAS is built to preserve.

The randomized algorithm that splits a product of irreducibles of equal degree over a finite field. For odd p, a random element raised to (p^d - 1)/2 is 1 in some of the factor fields and -1 in others, so a GCD separates the two groups, and each attempt succeeds with probability about one half.

Conflict-driven clause learning: DPLL plus the observation that a conflict is a proof that some set of decisions is impossible. The solver analyses the implication graph, derives a new clause ruling that set out, adds it to the database, and backjumps possibly many levels at once rather than undoing one decision at a time.

The lock-free double-ended queue that work stealing is normally built on. The owner pushes and pops at the bottom with no atomic operation at all in the common case; thieves take from the top with a compare-and-swap; the two only contend when the deque is nearly empty, which is exactly the case the algorithm handles carefully.

The decision procedure for equality over uninterpreted functions: union-find plus the rule that equal arguments give equal applications. Merging two classes can therefore force their parents to merge, so the closure is computed by re-examining parents until nothing changes.

The extension that gives constraints their own kind, so the thing left of the arrow becomes a first-class type that can be named, parameterised, and computed by a type family. It is how a container class expresses whatever its elements require without fixing it in the class head.

Continuation-passing style: instead of returning, a function takes an extra continuation argument and calls it with the result. Every call becomes a tail call, which is what lets a CPS-transformed program run in constant stack space wherever tail calls are eliminated, and it makes control flow a value that can be stored and resumed.

A type that may mention values, so that a vector's length can appear in its type and a function can promise to return a vector one element longer than its argument. Type checking then involves evaluating terms, which is why languages with dependent types usually double as proof assistants.

An explicit choice of how a derived instance is produced: stock (compiler-generated), newtype (reuse the underlying type's instance by coercion), anyclass (take the class's own defaults), or via (borrow the instance of a representationally equal type). Naming the strategy removes the ambiguity that arises when more than one is applicable.

The fragment of linear arithmetic whose atoms all have the form x - y <= k. A set of such constraints is a weighted graph, and it is satisfiable exactly when the graph has no negative cycle, so Bellman-Ford both decides it and, on failure, hands back the cycle as the explanation.

The plain-text interchange format for CNF instances: a header giving the variable and clause counts, then one clause per line as space-separated nonzero integers terminated by a zero, with a negative integer meaning a negated variable. Every SAT solver reads it, which is what makes solvers comparable at all.

Davis-Putnam-Logemann-Loveland: the backtracking search underneath every classical SAT solver. Propagate units, and if that produces no conflict pick an unassigned variable, assign it, and recurse; on conflict undo the most recent decision and try the other value. Correct, complete, and exponential on the instances designed to hurt it.

The standard architecture for an SMT solver: a CDCL core treats each theory atom as a boolean variable and searches as usual, while a theory solver checks each candidate assignment for theory consistency and hands back an explanation when it fails. The explanation becomes a learned clause, so the boolean search is what drives progress.

The procedure that turns a conflict into a learned clause. Walk the implication graph backwards from the conflicting clause, resolving away literals assigned at the current decision level until exactly one remains: that unique implication point gives the clause that is both strong and cheap to derive, and its second-highest level says how far to backjump.

Generalized Algebraic Data Type: an ADT whose constructors may each refine the type parameter of the value they build, instead of every constructor sharing one polymorphic return type. This lets a single well-typed eval return an int for an Add node and a bool for an Eq node, checked at compile time rather than by an unchecked cast.

A generating set for a polynomial ideal whose leading terms generate the leading-term ideal, which makes the remainder of multivariate division unique and zero exactly on the ideal. Buchberger's algorithm builds one by reducing S-polynomials until none leaves a nonzero remainder.

Turning a factorization modulo p into one modulo p^k, one power at a time. The step is exact linear algebra rather than a search: the error divided by p^k fixes what the correction must be, and the Bezout relation between the two mod-p factors solves for it directly.

A type that abstracts over a type constructor rather than over a type, so that Functor f can be instantiated at Maybe or at lists without naming their element types. It is what makes a single Monad class usable across every container instead of one class per shape.

Multiplying two n-limb integers with three half-size multiplications instead of four, by reusing (a0+a1)(b0+b1) to obtain the middle term. That turns the schoolbook n^2 into about n^1.585, and it only pays above a threshold where the extra additions cost less than the multiplication saved.

A maximal subexpression that is not polynomial, treated as an opaque variable so that polynomial machinery still applies around it. It is what lets expand handle sin(x)*(x+1)^2: sin(x) becomes a variable, the expansion proceeds, and the variable is substituted back afterwards.

Long division on multi-limb integers. The loop is straightforward; the quotient digit is not. Normalizing so the divisor's top limb is at least half the base bounds the estimate's error at two, which a short correction loop removes, with a rare add-back when the multiply-and-subtract goes negative.

A bound on the coefficients of any factor of an integer polynomial, in terms of the degree and norm of the polynomial itself. It is what tells a Hensel lift when to stop: once the modulus exceeds twice the bound, a symmetric representative is the integer factor rather than merely congruent to it.

Computing a polynomial GCD over Z by computing it modulo several machine-word primes and reconstructing by the Chinese remainder theorem, stopping once the modulus provably exceeds twice the largest coefficient the answer could have. The answer is small even when the road to it is not, which is why this is orders of magnitude faster than any remainder sequence.

A total order on monomials compatible with multiplication, which is what makes a leading term well defined. Lexicographic order sorts by the first variable that differs, graded orders compare total degree first, and the choice changes the cost of a Groebner basis computation by orders of magnitude.

A typeclass instance declared in a module that owns neither the class nor the type. Because instance resolution is global but imports are not, two orphans for the same pair can coexist in one program and the behaviour then depends on what happened to be linked, which is why the compiler warns about them.

Two instances overlap when some type matches both. Resolution does not backtrack, so the compiler must commit and instead reports an error. The OVERLAPPING pragmas make the more specific instance win, which is unsound when the overlap is not visible where the constraint is solved.

Rewriting a rational function as a polynomial plus one term per irreducible factor power of the denominator. Splitting across coprime denominators is the Bezout identity and nothing more; doing it over irreducible rather than square-free factors is what requires a factoriser.

A type parameter that appears in a type's signature but in none of its fields, used purely to keep two otherwise identical representations from being mixed up. Unlike a GADT it adds no information at pattern-match time: it constrains what the caller may do, not what the compiler can learn.

The family of CNF instances asserting that n+1 pigeons fit in n holes with no two sharing. They are unsatisfiable, and every resolution proof of that is exponentially long, so they are the standard way to show that a solver's cleverness is heuristic rather than a change in worst-case behaviour.

Polynomial division made to stay inside a ring that is not a field, by multiplying the dividend by a power of the divisor's leading coefficient first. Nothing ever becomes a fraction, and the price is that coefficients square at every step, which is the problem the subresultant correction exists to solve.

A literal whose negation appears in no clause can be set true outright: doing so can only satisfy clauses, never falsify one, so the assignment needs no decision and is never undone. It is in the original DPLL paper and in almost no modern solver, because maintaining the occurrence counts costs more than the rule saves.

A base type paired with a logical predicate that its values must satisfy, such as the integers greater than zero. Checking is discharged by an SMT solver at compile time, so the guarantees are stronger than a plain type without requiring dependent-type-style proof terms from the programmer.

The Boolean satisfiability problem: given a propositional formula, decide whether some assignment of true and false to its variables makes it true. It is the canonical NP-complete problem, and also one that modern solvers routinely settle for instances with millions of variables.

Satisfiability modulo theories: SAT where the atoms are not opaque booleans but statements in some theory, such as linear arithmetic or equality over uninterpreted functions. The formula must be satisfiable both propositionally and in the theory, which is what makes SMT the engine under most program verifiers.

Splitting a polynomial into pairwise coprime square-free factors with their multiplicities. In characteristic zero, Yun's algorithm gets a whole multiplicity level per GCD because a polynomial and its derivative share exactly the repeated factors; in characteristic p it needs an extra branch, since the derivative of x^p is zero.

The polynomial remainder sequence that keeps coefficient growth linear rather than doubly exponential. Each remainder is divisible by a factor predictable from the previous two degrees and leading coefficients, and dividing it out at every step holds the intermediates near the true subresultants.

The product over every sign choice of x minus a sum of distinct square roots. These are irreducible over Z and split into factors of degree at most two modulo every prime, which makes them the worst case for factorization: recombination has to test every subset of the mod-p factors before concluding there is nothing to find.

The decision procedure plugged into a DPLL(T) core for one specific theory. Its interface is small: accept assertions, report consistent or inconsistent, and on inconsistency return a subset of the assertions that already conflict, because a smaller explanation becomes a stronger learned clause.

The inference rule that does most of the work in a SAT solver: if every literal of a clause is false except one unassigned literal, that literal must be true. Applying it to fixpoint after each decision is where solvers spend the bulk of their time, which is why the data structure that finds unit clauses is the thing worth optimizing.

Variable State Independent Decaying Sum: the branching heuristic in every modern SAT solver. Each variable carries an activity score, conflict analysis bumps the ones it touches, and all scores decay, so the search concentrates on whatever part of the formula is currently producing conflicts.

Two literals per clause are watched, with the invariant that neither is false unless the clause is already unit or falsified. A clause is only inspected when one of its watches becomes false, so propagation costs what it actually propagates rather than a rescan of the database, and backtracking costs nothing at all.

A pointer the collector is allowed to ignore when deciding reachability, so a cache can hold a value without keeping it alive. An ephemeron strengthens this to a key/value pair where the value is retained only while the key is independently reachable, which is what makes a memo table not leak.