One thing I'm interested in knowing is:
In general if there was a Boolean equation that you knew only one possible assignment of its variables would make it true. Then can it always be simplified easily (in polynomial time) down to one term representing the only solution?
What I have in mind is the integer factorisation of a semiprime with additional constraints.
So we have:
P × Q = N where N is the given semiprime.
P does not equal 1
Q does not equal 1
And P < Q
These 4 constraints force the binary digits of P and Q to all have just 1 possible value each.
Now we create a circuit representing the constraints. Convert that circuit into conjunctive normal form using tseytin transformation.
And now just generate just the 1st term of the conversation from the conjunctive normal form into disjunctive normal form (DNF). This can be done from picking one literal from each clause and joining them up with ANDs.
This first term of the DNF can not be true if the whole equation is false. So it must contain a part of the solution from the variables in its term. Grab the values of the variables that would make that 1st DNF term true. Substitute those values back into the original CNF equation, let it simplify, rinse and repeat.
Could such a technique possibly work?