Constrain certain variables in CNF to unique satisfying assignments

Question

[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.

Answer 1

If you could add clauses to a CNF formula to cause it to be unsatisfiable iff certain sets of variables don't have non-unique assignments among the formula's satisfying assignments, you could use this same method to solve UNIQUE-SAT for any CNF formula. Since UNIQUE-SAT is co-NP-complete, you'll have proven NP = co-NP. So it is unlikely there is a solution to the problem that involves simply adding clauses.

Answer 2

Below are links to a SAT-2015 paper titled "#∃SAT: Projected Model Counting" by Rehan Abdul Aziz, Geoffrey Chu, Christian Muise, and Peter Stuckey. The paper includes descriptions of the problem in general as well as algorithms for solving such problems expressed in CNF.

Full paper: http://link.springer.com/chapter/10.1007/978-3-319-24318-4_10

Preprint: http://arxiv.org/pdf/1507.07648v1.pdf