# Reduction from SAT to 0,1 integer linear program with zero or one solutions

Probably this is well known. There is probabilistic reduction from SAT to Unique SAT (0 or 1 solutions).

According to answer and comments derandomizing the reduction would imply $PH \subseteq \oplus P$.

There is simple reduction from SAT to 0,1 integer linear program with zero or one solutions.

Given SAT formula $\phi$ on variables $x_1,\ldots x_n$, introduce binary variables $b_i \in \{0,1\}$.

Define map literals to linear polynomials $f(x_i)=b_i$ and $f(\lnot x_i)=1-b_i$.

For a clause $l_1 \lor \cdots \lor l_k$ add constraint $\sum_{i=1}^k f(l_i) \ge 1$.

So far the solutions of the constraints are in one to one correspondence with the solutions of $\phi$.

To make the solution unique, add the optimization

$$\text{maximize} \sum_{i=1}^n 2^{(i-1)}b_i$$

Two sets of distinct powers of two have equal sums iff the sets are equal, so the objective function have unique maximum if the constraints are satisfied. The ordering of $x_i$ doesn't matter. So the 0,1 ILP has zero or one solutions and it is not easier than NP-complete and coNP-complete.

In what complexity class is solving the 0,1 ILP?

As far as I know ILP are not a complexity class.

$\log_2(n)$ calls to NP oracle would solve it via binary search, though I don't see a direct reduction to SAT.

This appears close to UP though there is no certificate.