Circuit Satisfiability¶

The existence of an external Boolean input valuation that drives a finite acyclic gate circuit's designated output to true.

Version: v1 · 2026-10-17 · History
Domain-specific #: 14085
Domain group: Applied Sciences & Engineering
Origin domain: Computer Science & Software Engineering
Subdomains: Circuit Complexity, Combinational Equivalence Checking → Computer Science & Software Engineering
Aliases: CircuitSAT, Circuit satisfiability problem

Core Idea¶

Circuit satisfiability asks whether some external input valuation makes a finite acyclic Boolean gate circuit's designated output true. The circuit remains fixed while its inputs vary; internal wire values follow from the gates rather than becoming independent choices. In compact notation, for a circuit \(C\) with \(n\) external input bits,

\[ \operatorname{CircuitSAT}(C)=1 \quad\Longleftrightarrow\quad \exists x\in\{0,1\}^{n}: C(x)=1. \]

This is a decision problem over circuit descriptions. It is distinct from the circuit object, the evaluation of one supplied input, and an algorithm for finding a successful input. Rao states the existential definition and uses a verifier circuit to establish NP-completeness; that complexity result describes the general problem, not an additional ingredient required in each instance.^[1]

The circuit input permits shared subcircuits. A formula-shaped circuit also qualifies: sharing is allowed, not mandatory. The acyclic gate graph supplies evaluation semantics without introducing a state-transition or temporal-reachability question.^[2]

Structural Signature¶

Sig role-phrases: finite acyclic Boolean gate circuit; external Boolean input valuation; gate-consistent evaluation; designated output bit; existential output-one decision.

Finite acyclic Boolean gate circuit. The presented instance supplies gates and directed dependencies. Fan-out can reuse a result. Without this carrier, an existential question may remain, but it is no longer the circuit-typed problem.^[2]
External Boolean input valuation. These are the replaceable witness bits. Fixing one valuation and asking only for its result changes the task to evaluation.^[1]
Gate-consistent evaluation. Each internal value must agree with its gate's function. Free internal choices could create an apparent true output that no actual external input produces.^[1]
Designated output bit. A particular Boolean result defines success. A multi-output construction can combine differences into one result, but no particular combining gate is universally required.^[3]
Existential output-one decision. One successful external valuation suffices for yes; none means no. Requiring a count of successful valuations changes the requested answer.^[1]

A solver, a reduction, a certificate format and a useful application are not further constitutive roles. They explain how the question is posed or answered, while the five roles determine which question it is.

What It Is Not¶

Not a Boolean circuit alone. A circuit can represent a function without anyone asking whether its output can be true. Circuit satisfiability adds that existence question.
Not fixed-input evaluation. Observing \(C(a)=0\) rules out the particular input \(a\); it does not establish that every input fails. The quantifier is the difference.
Not formula SAT by a change of label. Formula-shaped circuits are included, but a separately presented formula is a different input representation. Rao's conversion adds constrained gate variables to a CNF formula and preserves satisfiability; it does not make the representations or variable sets identical.^[1]
Not counting satisfying assignments. A count contains information that the yes/no existence bit does not retain. “How many?” and “At least one?” are different tasks.
Not a particular search method. A solver can fail to settle an instance without changing the underlying mathematical yes/no answer.
Not unrestricted sequential reachability. The hardware case below concerns combinational circuits. Its one-shot valuation map does not establish a corresponding claim about arbitrary evolving circuit state.^[3]

Scope of Application¶

Two source-backed habitats give the same decision relation different jobs.

Verifier constructions in complexity theory. For a fixed problem instance \(x\), a circuit can compute whether a candidate witness \(w\) is accepted. The existence question concerns its acceptance output.^[1]
Combinational hardware equivalence. A difference circuit, or miter, compares two designs under the same primary inputs. Asking whether its difference output can be true searches for an inequivalence witness.^[3]

The first is a complete parameterized teaching construction; the second is documented original research with an explicit circuit example. Neither is evidence of a witnessed production deployment. Their applicability follows from the circuit and decision maps, not from a shared application name.

Clarity¶

The distinction between an input witness and an internal wire prevents a specific reasoning error. A proposed successful external valuation must generate the required internal values through the gates. It is insufficient to assign the output true while leaving its dependencies unconstrained. In a gate-variable encoding, the extra variables therefore carry obligations rather than extra freedom to choose any convenient result.^[1]

The question also fixes the direction of a hardware conclusion. A satisfiable difference miter means the designs differ on some input. An unsatisfiable one means no such input exists in the combinational model. A yes answer to CircuitSAT is thus not automatically a favorable verification result.^[3]

Manages Complexity¶

The five roles separate the represented design from the question asked about it. Gate types, wiring, fan-out and size can vary while the outer test stays the same: hold the circuit fixed, vary external inputs, evaluate consistently, inspect the selected output, and decide existence.

This compression does not discard the gate graph. Two representations can agree on existence while imposing different evaluation, encoding and checking obligations. Keeping both the common question and its circuit carrier visible avoids treating a translation as if it had left every detail unchanged.

Abstract Reasoning¶

Three inferences follow from the definition. A verified external valuation with output one establishes a positive instance. A failed valuation establishes only that this candidate does not witness one. To infer a negative instance requires evidence excluding all external valuations, rather than an accumulation of unsuccessful examples.

A gate-consistent CNF translation gives a second route to the same existence bit: unsatisfiability of that output-true encoding excludes an accepting circuit input.^[1] This inference depends on the encoding conditions. If a gate equation or the required output condition is omitted, the encoding no longer warrants the same conclusion.

For a miter, the existential witness has an additional interpretation: it identifies common inputs on which the designs disagree. That interpretation comes from the miter construction; it is not a meaning attached to every satisfying circuit input.^[3]

Knowledge Transfer¶

The verifier and miter cases teach the same modeling discipline: construct a Boolean output whose truth means exactly the event being sought, then ask whether any external valuation realizes it. In the verifier, true means acceptance of a witness. In the miter, true means disagreement of designs. Confusing those meanings reverses the practical conclusion while leaving the formal existence test unchanged.

Transfer within computing requires preserving the complete map, particularly the external-input domain and output interpretation. Outside literal Boolean gate models, “finding a satisfying configuration” can be an analogy or a broader feasibility question. It does not by itself establish circuit satisfiability.

Examples¶

Canonical¶

A verifier circuit for a fixed instance. Rao's NP-completeness construction starts from a verifier \(V\). With \(x\) fixed, it builds \(C_x(w)\) computing \(V(x,w)\). Acceptance of \(x\) is equivalent to the existence of a witness \(w\) making that circuit output one. This is a parameterized formal construction, not a measured deployment.^[1]

Mapped back: the finite acyclic Boolean gate circuit is \(C_x\); the external Boolean input valuation supplies \(w\); gate-consistent evaluation computes the verifier on fixed \(x\) and varying \(w\); the designated output bit is acceptance; the existential output-one decision asks whether any witness is accepted. The particular language, verifier and witness length can vary without replacing those roles.

Applied/practice¶

A combinational equivalence miter. Chatterjee and colleagues connect corresponding inputs of two designs, compare corresponding outputs by XOR, and combine differences into a single result. Their Figure 1 has one output per design, so its miter needs no final OR gate. A constantly zero miter establishes equivalence; an input making it one distinguishes the designs. The paper encodes the miter as gate clauses plus an output-true unit clause for SAT-based checking.^[3]

Mapped back: the finite acyclic Boolean gate circuit is the constructed miter; its external Boolean input valuation is shared by the designs; gate-consistent evaluation propagates that common input through both designs and the difference gates; the designated output bit reports a difference; the existential output-one decision asks whether such a difference can occur. The CNF and proof-producing checker implement an answering route, rather than adding necessary roles to CircuitSAT.

Structural Tensions¶

T1: Simple whole-miter proof vs. tractable combinational checking. In the documented CEC setting, a naive whole-miter SAT formulation permits a simple independently checkable resolution proof, but the resulting instance can be hard. Structural simplification can make checking practical while changing the circuit or splitting the obligations, so the direct monolithic proof is no longer immediately available. The cost of leaning toward simplification is the work of reconnecting its partial results to a certificate for the original miter. The source's solution reconstructs a single proof and preserves a simple verifier. This is a bounded verification-workflow tension, not an unavoidable conflict in every circuit-satisfiability instance.^[3]

Diagnostic: Which simplifications are needed for this miter, and what proof reconnects their results to the original difference-output question?

Structural–Framed Character¶

Circuit satisfiability is predominantly structural: once the circuit, Boolean semantics and designated output are fixed, the existence of a successful input is a mathematical fact.

Evaluative weight. Satisfiable does not mean good, efficient or safe. In a difference miter, it exposes inequivalence; in a verifier, it can express acceptance.
Human-practice dependence. People construct circuits and seek answers, but no successful solver run or institutional certification is required for the existence condition to hold.
Institutional origin. A course reduction and a hardware-verification program use the relation for different purposes. Neither institution determines its truth.
Vocabulary travel. “Satisfiable” also describes formulas and other formal constraints. Here its carrier remains a finite Boolean gate circuit.
Import versus recognition. An unrelated problem is not CircuitSAT merely because someone calls its requirements gates. Literal recognition requires the stated circuit semantics and quantifier.

The portable residue is an existential feasibility question. Whether that residue warrants a separate cross-domain abstraction is a broader question; it does not grant this circuit-typed entry independent reach beyond its carrier.

Its character: a formal structural decision problem whose reusable relation remains domain-specific because Boolean gates, external valuations and coherent circuit evaluation are constitutive.

Structural Core vs. Domain Accent¶

The skeletal relation holds a formal instance fixed and asks whether one permitted assignment meets its success condition. The domain-bound mechanism supplies an acyclic Boolean gate graph and derives its output from external bits. Removing that mechanism leaves a broader feasibility question, not the full named problem.

Verifier notation, XOR/OR miter layout, gate-variable CNF, resolution certificates and solver choices are accents of particular constructions or answering methods. They can change while the circuit-input existence question remains. The named entry does not clear the Prime bar on that basis: its two unlike uses remain literal Boolean computation, while purported noncomputing transfer requires a new representation and justification.

This entry is a kind of Function (Mapping).

Function (Mapping). CircuitSAT itself instantiates a deterministic function, rather than a particular solver: its domain is the set of well-formed finite acyclic Boolean circuit descriptions with designated outputs, its codomain is \(\{0,1\}\), and its rule assigns one exactly when an external input makes the output true. Each domain element has one definite answer, independent of evaluator, time or search history. The mapping is total on that declared domain, and the existential definition specifies its rule even when no successful witness or efficient computation is available. Both the verifier and miter constructions become inputs to this same decision mapping.^[1]
Satisfiability supplies the neighboring formula/model-existence identity. A satisfiability-preserving translation connects the questions, while the circuit representation remains a substantive distinction.
Boolean Circuit supplies the neighboring object identity. Circuit satisfiability asks an existence question about that object rather than naming the object alone.
Constraint Satisfaction shares assignment and feasibility language. The broader resemblance does not erase the designated circuit input and its evaluation semantics.

These comparisons identify common structure and differences; none makes a solver, a translation or the topic of hardware verification part of the formal definition.

Relationships to Other Abstractions¶

Current abstraction Circuit Satisfiability Domain-specific

Parents (1) — more general patterns this builds on

Circuit Satisfiability is a kind of Function (Mapping) Prime

Circuit satisfiability is the Boolean-valued mapping on well-formed acyclic gate-circuit descriptions that tests for any external input producing output one.

Hierarchy path (1) — routes to 1 parentless root

Circuit Satisfiability → Function (Mapping)

Neighborhood in Abstraction Space¶

Circuit Satisfiability sits in a sparse region of the domain-specific corpus (65^th percentile for distinctiveness): few abstractions share its structure, so a faithful description tends to retrieve it precisely.

Family — Computational Complexity & Hardness (18 abstractions)

Nearest neighbors

Comparator-circuit complexity class CC — 0.87
NOR logic — 0.86
Logical NOR — 0.84
Boolean circuit — 0.84
Deferred Measurement Principle — 0.83

Computed from structural-signature embeddings · 2026-10-17

Not to Be Confused With¶

Formula SAT. Tell: inspect the presented input. A formula can be realized as a circuit, but its formula representation and a general shared gate graph are not interchangeable descriptions without a construction.^[1]
Planar SAT. Tell: its extra restriction concerns the planarity of a formula's variable–clause incidence graph, not the existence question for an arbitrary gate circuit.
#SAT. Tell: the requested answer is a model count, rather than a yes/no existence bit.
Circuit evaluation. Tell: the external valuation is supplied rather than existentially varied.
Sequential reachability. Tell: the question concerns evolving state and a temporal target; the combinational miter example does not supply that map.^[3]

References¶

[1] Anup Rao. Lecture 8 (NP-complete programs). CSE 431, University of Washington, January 26, 2023. One-based PDF p. 1, Definition 1 and Theorem 3; p. 2, formula fan-out definition; p. 3, Theorem 5 gate-variable CNF construction. Full teaching text inspected; not an original Cook/Levin research paper. registry ↩a ↩b ↩c ↩d ↩e ↩f ↩g ↩h ↩i ↩j ↩k

[2] Jason Ku and Yun William Yu. Class 4 Scribe Notes, 6.890. Massachusetts Institute of Technology, September 16, 2014. One-based PDF p. 1, §2, Circuit SAT bullets. Ku and Yu are the notetakers; Erik Demaine is the instructor. Full university-hosted course notes inspected for the acyclic gate-DAG and reuse characterization; the printed 2014 date is used rather than the URL directory's spring19 label. registry ↩a ↩b

[3] Satrajit Chatterjee, Alan Mishchenko, Robert Brayton, and Andreas Kuehlmann. On Resolution Proofs for Combinational Equivalence. Proceedings of the 44^th Design Automation Conference (DAC), 2007, pp. 600–605. Printed pp. 600–601 / one-based PDF pp. 1–2, abstract, Figure 1 and §§2.1–2.4. Full original author-hosted text inspected; the figure is a documented example, not an observed production trace. registry ↩a ↩b ↩c ↩d ↩e ↩f ↩g ↩h