Computational complexity of dividing a set of constraints into a minimum number of satisfiable clusters

Question

I am looking for the computational complexity of the following problem.

Divide a given set of constraints into a minimum number of satisfiable clusters such that the constraints within the same cluster are satisfiable together.

Constraints can be in any type, such as Boolean logic or CSP and you can assume that there is an S() function that takes a set of constraints and decides the satisfiability of these constraints.

For instance assume that the following set of constraints in Boolean logic for the Boolean parameters p1, p2, p3, and p4 are given.

C = {“p1”, “p1 & p2”, “!p1 & p2”, “p3 & p4”, “!p4”}

This set can be divided into 2 satisfiable clusters as follows:

 // A solution for C1 can be p1=True, p2=True, p3=True, p4=True
C1 = {“p1”, “p1 & p2”, “p3 & p4”} 

// A solution for C2 can be p1=False, p2=True, p3=True, p4=False
C2 = {“!p1 & p2”, “!p4”}

Another example would be:

C = {"x>1", "x!=y", "y==1", "x+y<1", "x+1<2*y", "x==1"} // where both x and y are integers.

This constraint set can be divided into 3 satisfiable clusters as follows:

 // A solution for C1 can be x=5, y=1
C1 = {"x>1", "x!=y", "y==1"}

// A solution for C2 can be x=0, y=-1
C2 = {"x+y<1"}

// A solution for C3 can be x=1, y=2
C3 = {"x+1<2*y", "x==1"}

Here is my informal approach for the computation complexity of the problem:

First, I consider the decision version of the problem: Given a set of constraints, can this set be partitioned into k satisfiable clusters? Since we assume that an S() function is always provided for the given constraint type, a solution can be easily verified whether it becomes satisfiable or not using the given S() function. Then, it becomes NP. About the hardness of the problem, let's assume that we are concerned with SAT (Boolean satisfiability problem). In this scenario, considering that the SAT problem is NP-Complete, the problem itself becomes NP-hard since deciding whether a set of constraints can be partitioned into 1 satisfiable cluster is a harder problem than SAT. Therefore, the computational complexity of my problem depends on the constraint used in the problem. That is, satisfiability of any constraint problem that is NP-complete makes my problem is NP-hard.

What do you think about my approach? And if you think it is not correct or not complete, can you suggest another approach?

Answer 1

I think your problem is NP-hard for k = 1 since that is equivalent to SAT, but it is in P for k > 1.

For example, a SAT instance can be easily decomposed into two satisfiable subformulas. Go from SAT to 3SAT using the usual methods, unit propagate, then sort what remains into Horn and anti-Horn sets, each of which is trivially satisfiable (or can be made so by tossing one of any $x \land \lnot{x}$ pair into the other pile). The Horn and anti-Horn sets can be further divided into as many satisfiable subsets as desired.