I am searching for 3sat problems having unique solution. Till now, I only found one site https://www.cs.ubc.ca/~hoos/SATLIB/benchm.html
There are good examples of 3sat instance on that site but the problem is they have more than 1 solution if it's satisfiable. I want such big instances of 3sat of having 20 40 variables and at least 100 clauses ( More will be good ) but having unique solution. Where can I get such list of questions Or is there any algorithm which can generate 3sat question having unique solution ?
To construct a 3SAT problem with unique solution, you could use an arithmetic circuit like an adder or a multiplier. The resulting output lines are then compared against the known result using a digital comparator.
The design flow could be as follows:
The simplest variant of such a circuit would be a digital comparator without pre-attached arithmetic circuit.
To get a unique solution, the arithmetic expression must have a unique solution. Counterexamples include integer division and integer sqare root.