0
$\begingroup$

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

$\endgroup$
1
$\begingroup$

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.

$\endgroup$
1
$\begingroup$

The problem you are trying to solve seems to be called #∃SAT, or Projected Model Counting. Below are links to a recent paper that 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

$\endgroup$
  • $\begingroup$ Welcome to CS.SE! Can you edit the answer to add a full citation (title, authors, and where published)? This will help ensure the answer is useful even if the link dies, and might even help others find this answer via search. $\endgroup$ – D.W. Feb 19 '16 at 6:45

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.