Propositional logic

Logical conjunction of any number of predicates.

And(a, b, c) is flattened (nested And arguments are spliced in), True arguments are dropped, a False argument or a complementary pair x, Not(x) gives False, duplicates are removed and the arguments are put in a canonical order (atoms by name, then compound terms), so And(b, a) is the same expression as And(a, b). Python True/False are accepted alongside expressions. A single argument is returned unchanged.

>>> import alkahest as ak
>>> p = ak.ExprPool(); a, b, c = p.symbol("a"), p.symbol("b"), p.symbol("c")
>>> ak.And(c, ak.And(b, a)) == ak.And(a, b, c)
True

Logical disjunction of any number of predicates (dual of And(): flattened, False dropped, True or x, Not(x) gives True, deduplicated and canonically ordered).

Logical negation; Not(Not(x)) is x and Not(True) is False.

Exclusive or (odd parity) of any number of predicates.

The kernel has no Xor node, so the result is the parity chain written with And/Or/Not; consecutive stages share their sub-formula, so the expression grows linearly with the number of arguments. Xor(x, x) is False; Xor() of bools only is refused (no pool).

Material implication a → b, built as Or(Not(a), b).

Equivalence of any number of predicates: true when all have the same value, built as Or(And(a₁…aₙ), And(¬a₁…¬aₙ)).

If-then-else (c ∧ t) ∨ (¬c ∧ e) (the multiplexer).

Negation normal form: negations pushed onto atoms, only And/Or above them. Arithmetic relations are opaque atoms (Not(x < 0) is kept, not rewritten to x >= 0).

Raises LogicError (E-LOGIC-002) for quantified formulas or non-Boolean terms.

Conjunctive normal form (product of sums).

With simplify=False (default) the form is obtained by distribution, with tautological, duplicate and subsumed clauses dropped; it can be exponentially larger than the input and is refused past 100 000 clauses (LogicError, E-LOGIC-003). simplify=True returns the minimum CNF of simplify_logic() instead.

>>> import alkahest as ak
>>> p = ak.ExprPool(); a, b, c = p.symbol("a"), p.symbol("b"), p.symbol("c")
>>> print(ak.to_cnf(ak.Or(a, ak.And(b, c))))
(a ∨ b) ∧ (a ∨ c)

Disjunctive normal form (sum of products); the dual of to_cnf(), with the same simplify switch and size ceiling.

Minimise a propositional formula to a two-level form.

expr

formula over Boolean symbols (relations such as x > 0 are accepted as opaque atoms).

form

"dnf" (sum of products), "cnf" (product of sums) or "auto" (whichever has fewer literals, DNF on a tie).

dontcare

optional formula marking assignments whose value is free; the result agrees with expr wherever dontcare is false.

exact

None (default) — exact up to 12 variables, heuristic beyond; True — exact or raise LogicError (E-LOGIC-004, more than 16 variables or a covering search past its bound); False — heuristic.

Expr — the minimised formula. minimize_logic() returns the

same with exact/terms/literals metadata.

The exact method is Quine–McCluskey prime implicants followed by a minimum cover (Petrick's method, run as branch-and-bound): fewest terms, then fewest literals. The heuristic is an espresso-style expand / irredundant pass on the ROBDD of the function; its cover is always equivalent but not necessarily minimum. Every result is checked against the input before it is returned.

Raises LogicError (E-LOGIC-002 not propositional, E-LOGIC-003 size ceiling, E-LOGIC-004 exactness unavailable, E-LOGIC-005 bad form) and BudgetExceededError under an active budget.

>>> import alkahest as ak
>>> p = ak.ExprPool(); a, b = p.symbol("a"), p.symbol("b")
>>> print(ak.simplify_logic(ak.Or(ak.And(a, b), ak.And(a, ak.Not(b)))))
a

simplify_logic() returning a MinimizedLogic record (expr, form, exact, terms, literals) so a caller can see whether minimality was proven. Default form is "dnf".

Multi-output. Pass a list or tuple of formulas to minimise them jointly: the result is a MultiMinimizedLogic whose exprs are two-level forms built from product terms (clauses for form="cnf") shared between outputs, so terms counts each distinct term once — never more than the sum of the separately minimised outputs. dontcare applies to every output. Up to 12 variables (16 with exact=True) the shared cover is exact (multi-output Quine–McCluskey primes, then a minimum cover of the (output, minterm) pairs: fewest distinct terms, then fewest literals); beyond that the espresso-style pass runs per output and the pooled cubes are cut down to an irredundant shared set, flagged exact=False. Every output is verified against its input before the result is returned. At most 64 outputs (LogicError, E-LOGIC-003).

>>> import alkahest as ak
>>> p = ak.ExprPool(); a, b = p.symbol("a"), p.symbol("b")
>>> r = ak.minimize_logic([ak.Xor(a, b), ak.And(a, b), ak.Or(a, b)])
>>> r.terms, r.exact
(3, True)

Result of minimize_logic() on a list of formulas: one two-level formula per output, built from product terms (or clauses) shared between outputs.

exprs

form

exact

terms

literals

per_output_terms

shared_terms

Build the reduced ordered BDD of a formula over Boolean symbols.

expr

formula (And/Or/Not/Xor/… over symbols).

order

optional list of symbols (or names) fixing the variable order, root first; symbols of expr not listed are appended. None uses depth-first first-visit order over the canonically sorted formula, which interleaves the operand bits of bit-sliced arithmetic (the order adders and comparators need).

max_nodes

node ceiling (default 2 000 000). A BDD that would exceed it is refused with LogicError (E-LOGIC-003); an active alkahest.Budget is honoured too (BudgetExceededError).

auto_reorder

dynamic variable reordering (Rudell sifting) once the manager holds this many live nodes: False off, True or an int threshold on. None (default) means on at 50 000 nodes unless an explicit order was given. It never changes what a BDD means, only its order and size; see BDD.reorder() to sift on demand.

PythonCopy

>>> import alkahest as ak

PythonCopy

>>> p = ak.ExprPool(); a, b, c = p.symbol("a"), p.symbol("b"), p.symbol("c")

PythonCopy

>>> f = ak.bdd(ak.Or(ak.And(a, b), ak.And(b, c), ak.And(a, c)))

PythonCopy

>>> f.sat_count(), f.node_count()

(4, 4)

A reduced ordered binary decision diagram, returned by bdd().

Canonical for its variable order: two BDDs of the same manager are equivalent exactly when equivalent() says so, in time independent of the formulas. &, |, ^ and ~ combine BDDs (or a BDD and an Expr); operands built by separate bdd() calls are merged by variable name.

auto_reorder

order

implies(other)

iff(other)

ite(g, h)

restrict(assignment)

exists(variables)

forall(variables)

sat_count(variables=None)

reorder(max_growth=1.2, max_swaps=...)

set_auto_reorder(threshold)

node_count()

support()

satisfy_one()

is_true()

is_false()

equivalent(other)

to_expr()

Decide whether two propositional formulas are equivalent.

f, g: formulas (same pool).

method

"auto" (truth table up to 16 variables, then a BDD capped at 200 000 nodes, then SAT), "truth_table", "bdd" or "sat" (DPLL on the miter f ⊕ g).

counterexample

return (verdict, assignment_or_None) instead of a bare bool; the assignment maps symbol names to bools and is checked to separate f and g.

Relations (x > 0) are accepted as opaque atoms: True is then still a proof, but a propositional difference is refused with LogicError (E-LOGIC-002) rather than reported as False, because x > 0 and Not(x <= 0) are propositionally independent yet equal over ℝ. A search that exhausts its bound raises LogicError (E-LOGIC-003) — never a guessed verdict.

>>> import alkahest as ak
>>> p = ak.ExprPool(); a, b = p.symbol("a"), p.symbol("b")
>>> ak.equivalent(ak.Not(ak.And(a, b)), ak.Or(ak.Not(a), ak.Not(b)))
True

Truth table of a formula over Boolean symbols.

expr

formula.

variables

the symbols to tabulate, in column order; must include every symbol of expr. None uses the formula's symbols sorted by name.

list[tuple[tuple[bool, ...], bool]] — one (assignment, value)

row per assignment, from all-False to all-True with the last

variable varying fastest. At most 22 variables (E-LOGIC-003).

Decide satisfiability of a predicate Expr.

Returns False if unsatisfiable, True if satisfiable with no witness variables, a dict of symbol → value string if a witness is found, or None if the fragment is unsupported. None never means "unsatisfiable" — only False is a proof of that.

Two fragments are decided, and they are disjoint:

• Purely propositional — every leaf is a bare symbol (read as a Boolean variable, whatever Domain it was declared with) or pool.pred_true() / pool.pred_false(), combined with pred_and / pred_or / pred_not (equivalently And() / Or() / Not()). This fragment is decided completely by DPLL: it returns None only if the search exceeds its budget of 2 000 000 branching decisions, never because it gave up thinking. Wide formulas (more than 64 symbols) and formulas with shared sub-formulas (Xor parity chains, carry chains) are encoded on their DAG, so their size is what they share, not what they unfold to. → and ↔ are in it once written out: a → b is Or(Not(a), b) and a ↔ b is And(Or(Not(a), b), Or(Not(b), a)); the kernel has no separate implication node (Implies(), Equivalent(), Xor() and ITE() build these forms).
• One real symbol against rational constants — x < 3, x >= 1/2 and Boolean combinations of them, decided by interval intersection. This one is incomplete: None is common, and expected.

Everything else is None, including — deliberately — any formula that mixes a Boolean symbol with an arithmetic relation (A ∧ x > 0), any formula over two or more real symbols, and anything quantified. Deciding those needs a Boolean-plus-theory combination this function does not implement; the cheap alternative, abstracting each relation to a fresh proposition, is sound for "unsatisfiable" only and would call x > 0 ∧ x < 0 satisfiable. Send them to decide() (real quantifier elimination by CAD) or to smt instead.

A witness dict is homogeneous, so a caller can tell which path answered from any one value: propositional witnesses map every symbol to "true" or "false", interval witnesses map every symbol to a rational literal such as "1/2". The two never appear in the same dict.

>>> import alkahest as ak
>>> p = ak.ExprPool()
>>> A, B = p.symbol("A"), p.symbol("B")
>>> ak.satisfiable(p.pred_and([p.pred_or([A, B]), p.pred_not(A), p.pred_not(B)]))
False
>>> sorted(ak.satisfiable(p.pred_and([p.pred_or([A, B]), p.pred_not(A)])).items())
[('A', 'false'), ('B', 'true')]

Result of minimize_logic(): the two-level formula and how it was obtained.

expr

form

exact

terms

literals