CODEWITHSUNDEEP
constraint-programmingsatisfiabilitysat
genclik27
genclik27

Reputation: 323

Converting unsatisfiable set of constraints into satisfiable smaller sets of constraints

I have a project in my mind and I am curious whether something similar is done previously. Assume that there is a set of different type of constraints and these constraints are not satisfiable together.

C = {c1, c2, c3, ..., cn}

(c1 and c2 and c3 ... cn) : Not satisfiable

My aim is to divide this set into k sets (possibly k is very small) in a way that every set of constraint becomes satisfiable individually.

The basic solution is using a greedy approach. A constraint will be selected as the first constraint and labelled as first group. Then, the second one will be chosen and is checked whether it is solvable with the first constraint. If they are solvable, then the second constraint will be also in the first group, otherwise, it will be labelled as the second group. This process will continue in this manner until no constraint is left in the set. Another way of doing this may be dividing the constraint into 2 sets and check whether these sets are solvable individually. If not, continue dividing recursively. These 2 approaches both suffer in size, they divide constraint sets into very small sets.

I am looking for an efficient way of dividing a constraint set into k sets where k is close to optimal value (smallest k value). There are 2 challenges in here, 1) scalability issue and 2) structure of constraints is not known beforehand.

Upvotes: 1

Views: 89

Answers (1)

tobyodavies
tobyodavies

Reputation: 28099

An algorithm that woould do what you want can be expressed in terms of minimal unsatisfiable subsets which are well studied. This is the latest SAT competition track for them as far as I can tell: http://www.cril.univ-artois.fr/SAT11/results/results.php?idev=48

Using this, the following pseudo-code should do what you want

def sat_partition(CNF):
    partitions = {}
    while CNF is not empty:
        MUS = compute_mus(CNF)
        Remove one arbitrary element of MUS
        partitions += {MUS}
        CNF -= MUS
    return partitions

Upvotes: 1

Related Questions