On the complexity of unique Circuit SAT

We consider the Circuit SAT problem for a circuit with at most one satisfying assignment. We present an algorithm running in time $O(2^{.374589m})$, where $m$ is the number of internal gates of the circuit. In order to make the exposition self-contained, we also describe the algorithm for the general case of Circuit SAT with running time $O(2^{.389667m})$ obtained by Savinov in [10].