2
$\begingroup$

Given a conjunctive normal form (CNF) is it possible to remove one solution from its set of solutions (irrespective of whether the CNF has a solution or not in the first place)? By that I am asking if there is a new formula that will reduce the number of solutions of the original by one i.e. if the original one has 0 solutions then the newly constructed one will have 0 as well but if the original one has x solutions (x > 0) then the new one will have x-1.
If not (this might be in NP) is there an easy way to find a bound on the number of solutions removed?

Forcing a variable to take a specific value has the inconvenience of perhaps resulting in no solution at all (it might be the case that there is only one solution to begin with but it might also be the case where the N solutions depended on the variable taking another specific value).

For instance: e.g. Given (x1 V x2)^(!x1 V x2) - a CNF with possible solutions: x1 = T, x2 = T and x1=F, x2=T, I would like to construct a CNF with solution x1 = T, x2 = T only (or x1=F, x2=T only). (Note: ! = not and V = or)

  • 0
    You're right I wasn't as precise as I should have been. I fixed this hopefully.2011-11-19

1 Answers 1

2

For 1-CNF you can always remove one SAT solution if it exists because such formulas can only have 0 or 1 solution. If the formula has one solution, add a clause that negates one of the literals in the formula and the formula will then have no solution.

For 2-CNF formulas, you can use one of the known linear-time algorithms to find a solution and then add a single clause to the formula that removes just that solution. For example, if the formula has five variables and one of the solutions is 01001, add the clause (x1 or !x2 or x3 or x4 or !x5).

For everything else (k-CNF where k > 2) there is no known general polynomial-time algorithm for SAT, so the naive plan of finding a solution and then adding a clause to remove it isn't efficient enough. If you're willing to wait potentially an exponentially long time for your SAT solver to find a solution, you can then easily construct a clause that if added to the formula removes that solution.