<p>A multilinear polynomial representation of <span class="math-container">$f$</span> over <span class="math-container">$GF(2)$</span> is:</p>
<p><span class="math-container">$$f(x_1,x_2,\dots,x_n) = \sum_{S \subseteq \{1,\dots,n\}} a_S \prod_{i\in S}x_i$$</span></p>
<p>where <span class="math-container">$a_S \in \{0,1\}$</span>. Let:</p>
<p><span class="math-container">$$f_0 = f(0,x_2,\dots,x_n), \quad f_1 = f(1,x_2,\dots,x_n)$$</span></p>
<p>The function we want is:</p>
<p><span class="math-container">$$g(x_2,\dots,x_n) = f_0 \lor f_1 = f_0 + f_1 + f_0 f_1$$</span></p>
<p>over <span class="math-container">$GF(2)$</span>. The core idea is to build a circuit for <span class="math-container">$g$</span> without duplicating the entire circuit for <span class="math-container">$f_0$</span> and <span class="math-container">$f_1$</span>. Since <span class="math-container">$f_0$</span> and <span class="math-container">$f_1$</span> share all submonomials that do not explicitly contain <span class="math-container">$x_1$</span>, we can unify those shared parts in the final circuit.</p>
<p>The embedding into <span class="math-container">$\mathrm{GF}(2)[x_1,\dots,x_n,y_1,\dots,y_m]$</span> provides a systematic way to tag partial products or subfunctions so multiple identical copies can be &quot;collapsed&quot; into one. At the gate level, each output is a Boolean function of some input subset. When two gate outputs implement the same subfunction, we unify them by wiring to a single gate.</p>
<p>While we don't strictly need new variables <span class="math-container">$y_j$</span> for gate unification, they help enforce constraints like:</p>
<p><span class="math-container">$$y_j + (u + v) = 0 \quad \Longleftrightarrow \quad y_j = u + v$$</span></p>
<p>for bits <span class="math-container">$u, v$</span>. If <span class="math-container">$u$</span> and <span class="math-container">$v$</span> are subfunction outputs, <span class="math-container">$y_j$</span> serves as a single wire merging them. This formalizes that matching submonomials <span class="math-container">$\prod_{i\in S}x_i$</span> share the same wire <span class="math-container">$y_j$</span>. The number of <span class="math-container">$y_j$</span> needed depends on distinct subfunctions to name - potentially <span class="math-container">$O(s)$</span> variables for <span class="math-container">$s$</span> gates to ensure each subfunction gets a unique wire.</p>
<p>Each gate in <span class="math-container">$f$</span>'s circuit implements a Boolean function of <span class="math-container">$\{x_1,\dots,x_n\}$</span>. When partially evaluated at <span class="math-container">$x_1=0$</span> or <span class="math-container">$x_1=1$</span>, that gate represents some variable subset in the multilinear polynomial view. With canonical labels (e.g., sorted variable indices plus combination type), identical subfunctions have matching labels.</p>
<p>While naive pairwise comparison needs <span class="math-container">$O(s^2)$</span> comparisons, hashing/sorting reduces identical label identification to <span class="math-container">$O(s \log s)$</span> lookups. The circuit implementation of comparisons or hashing adds overhead but remains <span class="math-container">$O(s \log s)$</span> with a balanced merge tree. After unifying identical subfunctions, the final OR needs just a constant number of additional gates beyond the unified subDAG.</p>
<p>Here is the detailed construction:</p>
<pre><code>def buildGCircuit(f):
    # 1. Construct the DAG for f with size s. Each node is a gate (AND/OR/XOR)
    #    and each leaf is an input x_i. (Over GF(2), we primarily have AND/XOR,
    #    but assume we can handle a library of basic gates.)
    
    # 2. Make a copy of this DAG but partially evaluate x_1=0 where relevant =&gt; f0DAG
    #    Similarly, copy the DAG for x_1=1 =&gt; f1DAG
    #    These DAGs have at most 2s nodes in total if done naively.

    # 3. Assign a canonical label to each node in both f0DAG and f1DAG.
    #    For example, if the node is an AND gate with children labeled L and R,
    #    then label(node) = &quot;AND(label(L), label(R))&quot;.
    #    For a leaf x_i with i != 1, label(leaf) = &quot;x_i@0&quot; or &quot;x_i@1&quot; depending
    #    on partial evaluation context (or &quot;x_i&quot; if unaffected).
    #    For x_1 itself, label(leaf) = &quot;0&quot; or &quot;1&quot; in the relevant DAG.

    # 4. Build a map from label -&gt; node. Traverse the DAG from leaves up to outputs:
    #    whenever we compute label(N), if label(N) is already in the map,
    #    unify node N with the previously existing node that has the same label.
    #    Otherwise, store (label(N) -&gt; N) in the map.

    # 5. Let f0Output and f1Output be the outputs of the partially evaluated DAGs
    #    (which might be merged with many other nodes by step 4).
    #    Build final gates to compute:
    #       gOutput = f0Output XOR f1Output XOR (f0Output AND f1Output)
    #    Return gOutput as the root of the new circuit (plus all merged subDAGs).

    return finalCircuit
</code></pre>
<p>Merging preserves functional correctness since replacing truly identical subfunctions with a single representative doesn't change outputs. The final circuit still correctly computes <span class="math-container">$f_0$</span> and <span class="math-container">$f_1$</span>, producing <span class="math-container">$g = f_0 + f_1 + f_0f_1$</span>.</p>
<p>Consider a favorable example where <span class="math-container">$f$</span> factors significantly with repeated <span class="math-container">$x_1$</span>-independent subfunctions:</p>
<p><span class="math-container">$$f(x_1,x_2,x_3) = x_2x_3 + x_1(x_2 + x_3) + x_2 + x_3$$</span></p>
<p>over <span class="math-container">$GF(2)$</span>. Here <span class="math-container">$f_0$</span> and <span class="math-container">$f_1$</span> share subfunctions like <span class="math-container">$x_2 + x_3$</span> or <span class="math-container">$x_2x_3$</span>. Unifying these shared components can yield a circuit close to size <span class="math-container">$s$</span>.</p>
<p>In pathological cases where <span class="math-container">$f_0$</span> and <span class="math-container">$f_1$</span> share few/no subfunctions (if every gate involves <span class="math-container">$x_1$</span> uniquely), unification gives minimal savings. The circuit nearly duplicates for each branch plus OR gates, approaching <span class="math-container">$2s$</span> overhead but typically slightly better from minor merges.</p>

CC BY-SA 4.0
2024-12-28T09:06:56.353Z
This does not seem to answer the question, as it does not give a better worst-case upper bound than the trivial $2s$, nor a proof that $(2-\epsilon)s$ is not possible.
Emil Jeřábek
CC BY-SA 4.0
2024-12-28T17:26:46.797Z
I am sorry @EmilJeřábek but this is again one of the users who resort to gen ai for writing such answers. This user has already been suspended at Maths, MO, CV, Physics,Computational Science. I have written a Meta post on this: [Reporting the recent infestation of new users resorting to gen AI targeting STEM communities](https://meta.stackexchange.com/questions/405216/reporting-the-recent-infestation-of-new-users-resorting-to-gen-ai-targeting-stem).
User1865345
CC BY-SA 4.0
2024-12-28T17:30:58.053Z
I am rather surprised of how the moderators are apparently not active here as they have last been seen months ago as per their profiles. However, the best course of action is flagging for mods' attention and downvoting such posts @EmilJeřábek
User1865345
CC BY-SA 4.0
2024-12-28T05:17:29.937Z
2024-12-28T05:17:29.937Z
Raynard Bond
<p>We know that many SAT solvers exploits a &quot;branching&quot; strategy, which is setting a variable to 0 and 1, respectively, and check if any branch is satisfiable. But I suspect there is some information redundancy in the two branches.</p>
<p>Consider a Boolean formula/circuit <span class="math-container">$f(x_1,x_2,\cdots,x_n)$</span> with size <span class="math-container">$s$</span> (size is defined as the number of binary and/or gates used), and let <span class="math-container">$f_0=f(0,x_2,\cdots,x_n)$</span>, <span class="math-container">$f_1=f(1,x_2,\cdots,x_n)$</span>, <span class="math-container">$g=f_0\lor f_1$</span>. Obviously <span class="math-container">$g$</span> is equi-satisfiable with <span class="math-container">$f$</span>. The trivial representation of <span class="math-container">$g$</span> requires size at most <span class="math-container">$2s+O(1)$</span> (by simply combining to branches with an or gate), which seems pretty weird since their isn't an information gain from <span class="math-container">$f$</span> to <span class="math-container">$g$</span>. The amount of information even declined, yet the representation size doubled.</p>
<p>So, I wonder if there's an upper bound to the minimum size of a formula/circuit that represents <span class="math-container">$g$</span> in terms of <span class="math-container">$f$</span>, and if there's a polynomial-time algorithm that transforms <span class="math-container">$f$</span> to <span class="math-container">$g$</span> that meets this upper bound. If there's a better upper bound than <span class="math-container">$2s+O(1)$</span> and there exists an efficient transformation algorithm, then a more efficient SAT solver can be built since branching would not necessarily lead to doubling in the search space anymore.</p>
<p>I've actually did some experiments for the Boolean circuit case, with <span class="math-container">$n=4,5$</span>. I randomly sampled a few thousand truth tables for <span class="math-container">$f$</span> and leveraged <a href="https://github.com/berkeley-abc/abc" rel="nofollow noreferrer">Berkeley ABC</a> to do exact synthesis on <span class="math-container">$f$</span> and <span class="math-container">$g$</span> to find the minimum size of Boolean circuits that represent their truth tables. It turned out that the empirical upper bound of the minimum size of a circuit for <span class="math-container">$g$</span> is exactly <span class="math-container">$s$</span>.</p>
<p>So, is this problem well-studied?</p>

CC BY-SA 4.0
2024-12-23T19:28:11.753Z
Note that the strong exponential time hypothesis says that $(1+1/k - \varepsilon)s + o(s)$ can't be done with an $O(n^k)$ time algorithm
Command Master
CC BY-SA 4.0
2024-12-24T01:30:29.313Z
@CommandMaster I think you mean $(2-\varepsilon)s+o(s)$ can't be done with a polynomial-time transformation algorithm? Yeah this is clear, but as we know SETH is just a hypothesis and many people are working on disproving it. I suspect my problem reveals some intrinsic properties of Boolean functions/circuits and it's reluctant to deal with it by a hypothesis in SAT solving.
Soha
CC BY-SA 4.0
2024-12-29T03:04:46.753Z
https://en.wikipedia.org/wiki/Conflict-driven_clause_learning
D.W.
CC BY-SA 4.0
2024-12-29T05:25:47.323Z
@D.W. CDCL only works on clauses but here $f$ can be a deep formula/circuit.
Soha
<reference-request><circuit-complexity><boolean-formulas>
Upper bound to the minimum size of branched Boolean formulas/circuits
Soha
# Upper bound to the minimum size of branched Boolean formulas/circuits

(Asked by: username_0 on 2024-12-23)

We know that many SAT solvers exploits a "branching" strategy, which is setting a variable to 0 and 1, respectively, and check if any branch is satisfiable. But I suspect there is some information redundancy in the two branches.

Consider a Boolean formula/circuit $f(x\_1,x\_2,\cdots,x\_n)$ with size $s$ (size is defined as the number of binary and/or gates used), and let $f\_0=f(0,x\_2,\cdots,x\_n)$, $f\_1=f(1,x\_2,\cdots,x\_n)$, $g=f\_0\lor f\_1$. Obviously $g$ is equi-satisfiable with $f$. The trivial representation of $g$ requires size at most $2s+O(1)$ (by simply combining to branches with an or gate), which seems pretty weird since their isn't an information gain from $f$ to $g$. The amount of information even declined, yet the representation size doubled.

So, I wonder if there's an upper bound to the minimum size of a formula/circuit that represents $g$ in terms of $f$, and if there's a polynomial-time algorithm that transforms $f$ to $g$ that meets this upper bound. If there's a better upper bound than $2s+O(1)$ and there exists an efficient transformation algorithm, then a more efficient SAT solver can be built since branching would not necessarily lead to doubling in the search space anymore.

I've actually did some experiments for the Boolean circuit case, with $n=4,5$. I randomly sampled a few thousand truth tables for $f$ and leveraged [Berkeley ABC](https://github.com/berkeley-abc/abc) to do exact synthesis on $f$ and $g$ to find the minimum size of Boolean circuits that represent their truth tables. It turned out that the empirical upper bound of the minimum size of a circuit for $g$ is exactly $s$.

So, is this problem well-studied?

**Tags:** reference-request, circuit-complexity, boolean-formulas

> **Comments:**
> **username_1**: Note that the strong exponential time hypothesis says that $(1+1/k - \varepsilon)s + o(s)$ can't be done with an $O(n^k)$ time algorithm  
> **username_0**: @CommandMaster I think you mean $(2-\varepsilon)s+o(s)$ can't be done with a polynomial-time transformation algorithm? Yeah this is clear, but as we know SETH is just a hypothesis and many people are working on disproving it. I suspect my problem reveals some intrinsic properties of Boolean functions/circuits and it's reluctant to deal with it by a hypothesis in SAT solving.  
> **username_2**: https://en.wikipedia.org/wiki/Conflict-driven_clause_learning  
> **username_0**: @username_2 CDCL only works on clauses but here $f$ can be a deep formula/circuit.  

---

## 1 answers

### Answer by username_3 on 2024-12-28. Score: -5

A multilinear polynomial representation of $f$ over $GF(2)$ is:
$$f(x_1,x_2,\dots,x_n) = \sum_{S \subseteq \{1,\dots,n\}} a_S \prod_{i\in S}x_i$$
where $a_S \in \{0,1\}$. Let:
$$f_0 = f(0,x_2,\dots,x_n), \quad f_1 = f(1,x_2,\dots,x_n)$$
The function we want is:
$$g(x_2,\dots,x_n) = f_0 \lor f_1 = f_0 + f_1 + f_0 f_1$$
over $GF(2)$. The core idea is to build a circuit for $g$ without duplicating the entire circuit for $f_0$ and $f_1$. Since $f_0$ and $f_1$ share all submonomials that do not explicitly contain $x_1$, we can unify those shared parts in the final circuit.
The embedding into $\mathrm{GF}(2)[x_1,\dots,x_n,y_1,\dots,y_m]$ provides a systematic way to tag partial products or subfunctions so multiple identical copies can be "collapsed" into one. At the gate level, each output is a Boolean function of some input subset. When two gate outputs implement the same subfunction, we unify them by wiring to a single gate.
While we don't strictly need new variables $y_j$ for gate unification, they help enforce constraints like:
$$y_j + (u + v) = 0 \quad \Longleftrightarrow \quad y_j = u + v$$
for bits $u, v$. If $u$ and $v$ are subfunction outputs, $y_j$ serves as a single wire merging them. This formalizes that matching submonomials $\prod_{i\in S}x_i$ share the same wire $y_j$. The number of $y_j$ needed depends on distinct subfunctions to name - potentially $O(s)$ variables for $s$ gates to ensure each subfunction gets a unique wire.
Each gate in $f$'s circuit implements a Boolean function of $\{x_1,\dots,x_n\}$. When partially evaluated at $x_1=0$ or $x_1=1$, that gate represents some variable subset in the multilinear polynomial view. With canonical labels (e.g., sorted variable indices plus combination type), identical subfunctions have matching labels.
While naive pairwise comparison needs $O(s^2)$ comparisons, hashing/sorting reduces identical label identification to $O(s \log s)$ lookups. The circuit implementation of comparisons or hashing adds overhead but remains $O(s \log s)$ with a balanced merge tree. After unifying identical subfunctions, the final OR needs just a constant number of additional gates beyond the unified subDAG.
Here is the detailed construction:
def buildGCircuit(f):
    # 1. Construct the DAG for f with size s. Each node is a gate (AND/OR/XOR)
    #    and each leaf is an input x_i. (Over GF(2), we primarily have AND/XOR,
    #    but assume we can handle a library of basic gates.)
    
    # 2. Make a copy of this DAG but partially evaluate x_1=0 where relevant => f0DAG
    #    Similarly, copy the DAG for x_1=1 => f1DAG
    #    These DAGs have at most 2s nodes in total if done naively.

    # 3. Assign a canonical label to each node in both f0DAG and f1DAG.
    #    For example, if the node is an AND gate with children labeled L and R,
    #    then label(node) = "AND(label(L), label(R))".
    #    For a leaf x_i with i != 1, label(leaf) = "x_i@0" or "x_i@1" depending
    #    on partial evaluation context (or "x_i" if unaffected).
    #    For x_1 itself, label(leaf) = "0" or "1" in the relevant DAG.

    # 4. Build a map from label -> node. Traverse the DAG from leaves up to outputs:
    #    whenever we compute label(N), if label(N) is already in the map,
    #    unify node N with the previously existing node that has the same label.
    #    Otherwise, store (label(N) -> N) in the map.

    # 5. Let f0Output and f1Output be the outputs of the partially evaluated DAGs
    #    (which might be merged with many other nodes by step 4).
    #    Build final gates to compute:
    #       gOutput = f0Output XOR f1Output XOR (f0Output AND f1Output)
    #    Return gOutput as the root of the new circuit (plus all merged subDAGs).

    return finalCircuit

Merging preserves functional correctness since replacing truly identical subfunctions with a single representative doesn't change outputs. The final circuit still correctly computes $f_0$ and $f_1$, producing $g = f_0 + f_1 + f_0f_1$.
Consider a favorable example where $f$ factors significantly with repeated $x_1$-independent subfunctions:
$$f(x_1,x_2,x_3) = x_2x_3 + x_1(x_2 + x_3) + x_2 + x_3$$
over $GF(2)$. Here $f_0$ and $f_1$ share subfunctions like $x_2 + x_3$ or $x_2x_3$. Unifying these shared components can yield a circuit close to size $s$.
In pathological cases where $f_0$ and $f_1$ share few/no subfunctions (if every gate involves $x_1$ uniquely), unification gives minimal savings. The circuit nearly duplicates for each branch plus OR gates, approaching $2s$ overhead but typically slightly better from minor merges.

> **Comments:**
> **username_4**: This does not seem to answer the question, as it does not give a better worst-case upper bound than the trivial $2s$, nor a proof that $(2-\epsilon)s$ is not possible.  
> **username_5**: I am sorry @EmilJeřábek but this is again one of the users who resort to gen ai for writing such answers. This user has already been suspended at Maths, MO, CV, Physics,Computational Science. I have written a Meta post on this: [Reporting the recent infestation of new users resorting to gen AI targeting STEM communities](https://meta.stackexchange.com/questions/405216/reporting-the-recent-infestation-of-new-users-resorting-to-gen-ai-targeting-stem).  
> **username_5**: I am rather surprised of how the moderators are apparently not active here as they have last been seen months ago as per their profiles. However, the best course of action is flagging for mods' attention and downvoting such posts @EmilJeřábek  

---

