commit 6a2f2076075354cd8990e2653867cf0879c7d7d2
parent 81b4ef3643e9eb9e507ffc17c63bdc61a9451a33
Author: Antoine Amarilli <a3nm@a3nm.net>
Date: Tue, 14 Oct 2025 07:44:44 +0200
Merge remote-tracking branch 'origin/master'
Diffstat:
5 files changed, 35 insertions(+), 2 deletions(-)
diff --git a/automaton_acceptance b/automaton_acceptance
@@ -0,0 +1,13 @@
+# Automaton acceptance
+
+Given [automaton] A and [word] w, [decide] if A accepts w
+
+- [NFA_acceptance]: [state_set_simulation]
+
+[lower_bounds] from [ov_conjecture], see [backurs2016which]
+
+Up: [automata_problems], [membership_problem]
+
+See also: [regular_language_membership], [amarilli2025linear]
+
+Aliases: automaton membership, automata membership
diff --git a/boolean_formula b/boolean_formula
@@ -8,7 +8,9 @@ An [expression] which represents a [boolean_function], built from [literals] usi
- [clause]
- [term]
- [literal]
-- [Boolean_formulas_positive]
+- [boolean_formula_positive]
+
+[Boolean_formula_lower_bound]
Up: [representation] of [boolean_function]
diff --git a/boolean_formula_lower_bound b/boolean_formula_lower_bound
@@ -0,0 +1,17 @@
+# Boolean formula lower bound
+
+What are [lower_bounds] on the size of [Boolean_formulas] compared to [Boolean_circuits]?
+
+[fischer1982omega]: the [modulo_3] [Boolean_function] has a size lower bound of Omega(n log n) over the [full_Boolean_basis]
+
+[wegener1987complexity] Chapter 8 Theorem 5.2: the [Boolean_threshold_function] "at least two variables are true" on the basis [AND], [OR] and [NOT] needs size Omega(n log log n)
+
+Better bounds are known for [positive_Boolean_formulas]: [wegener1987complexity] Chapter 8 Theorem 1.2 says that the threshold function needs size Omega(n log n) with [AND] and [OR]
+
+[wegener1987complexity] Chapter 8 Theorem 8.2: the [parity_function] on the basis [AND], [OR] and [NOT] needs size Omega(n^2)
+
+Best separation is in Omega(n^{3-o(1)}), cf [hastad1998shrinkage] and https://cstheory.stackexchange.com/questions/25555/may-boolean-circuits-be-exponentially-more-concise-than-boolean-formulae/25601
+
+Related: https://cstheory.stackexchange.com/a/55791
+
+Up: [lower_bound], [boolean_formula]
diff --git a/negation b/negation
@@ -9,4 +9,4 @@
Up: [logic]
-Aliases: negated, negations
+Aliases: negated, negations, NOT
diff --git a/parity b/parity
@@ -5,6 +5,7 @@
- [parity_fine_grained]
- [sat_parity]
- [parity_constraints]
+- [parity_function]
- [even]
- [odd]