[Reposted because the original question was deleted by the poster.]
I'm looking for a way to add additional clauses (and maybe additional variables) to an already existing SAT instance so that solutions with non-unique assignments for certain variables are invalidated.
Currently I enumerate all the original solutions, and filter out the bad solutions having duplicate partial assignments on specific variables. But this becomes impractical when there are many solutions to the original instance, compared to a very small number of good solutions.
If the SAT solver had information within the CNF that duplicate partial assignments on certain variables invalidate any solution that contains those partial assignments, it would speed up the search significantly.
Here's an example with 16 variables: 90 original solutions, 42 filtered solutions. https://gist.github.com/re-curse/7b1c970768400ef5d0fe
This example instance generates 90 solutions, but 48 solutions are bad because they duplicate assignments for variables 1-8 or variables 8-16. I need to add clauses to the CNF to filter out those bad 48 solutions while the solver searches instead of retroactively filtering after enumerating all original solutions.
An example of two bad solutions for this instance are (00110110 00110110) and (00110110 00111001) because variables 1-8 have an assignment [ie. 00110110] that shows up more than once in the 90 original solutions.