What kind of SAT am I dealing with here?

Question

Problem set up: I have a long list of variables, $v_i$ (say about 200 total). I am given a bunch of Boolean statements as follows: $$\omega_1\land \omega_2\land \omega_3\land \omega_4\land \omega_5 \land \ldots \land \omega_n$$

Each $\omega_k$ is a disjuction of mutually exclusive statements (for example:) $$\omega_1 := \left( (v_1\land v_2 \land\lnot v_3)\lor (v_1\land \lnot v_2 \land v_3) \lor (\lnot v_1\land v_2 \land v_3) \right)$$

In other words it looks like the omegas are in the opposite of conjuctive normal form. In practice they will have more variables in each set of parentheses but will remain mutually exclusive.

My question: Is there a standard SAT paradigm to consider this in? I don't know if converting these to CNF is worthwhile--I'm told it could just make the problem exteremely messy-looking. On the other hand if I want to have a hope of solving (or proving no solution) then with problems this big it would seem that a bonifide SAT solver is my best bet.

Has anyone seen anything like this style of SAT before and does it have a name or formalism?

Answer 1

In practice, the best thing to do might be to convert to CNF and hand it to a standard SAT solver. It may "look messy" to humans, but not to the SAT solver. You might find a solver that accepts more general formats (though perhaps it will convert the problem internally to CNF). I know SMT solvers will accept assertions such as

(or (and v1 v2 (not v3)) (and v1 (not v2) v3) ((not v1) v2 v3))

and incorporate good SAT solvers.

Answer 2

Each $\omega_i$ is a Disjunctive normal form formula DNF.

So you have conjunction of DNF formulas.

DNF is easy to satisfy and hard to falsify.

Agree with Robert that possibly the best approach is to convert to CNF and try good SAT solver, unless you can exploit structure to greatly simplify the problem.

Answer 3

Problems of this type can easily be converted to CNF by introducing some auxiliary variables.

Your $\omega_1$ is a disjunction of three conjunctions, so introduce auxiliary variables $y_1, y_2, y_3$, one for each conjunction. We want to make $y_i$ equivalent to the $i$th conjunction. This is easy to do; for example, to make $y_1$ equivalent to $v_1\wedge v_2\wedge \neg v_3$, introduce the disjunction $$\neg v_1\vee \neg v_2 \vee v_3 \vee y_1$$ to force $y_1$ to be true when $v_1$ and $v_2$ and $\neg v_3$ are all true, and introduce the disjunctions $$v_1\vee \neg y_1$$ $$v_2\vee \neg y_1$$ $$\neg v_3 \vee \neg y_1$$ to force $v_1$ and $v_2$ and $\neg v_3$ to be true when $y_1$ is true. Then $\omega_1$ just becomes $y_1\vee y_2 \vee y_3$.

If you're not experienced with CNF or SAT solvers then this might look messy, but weight-two clauses are very efficiently handled by SAT solvers, and introducing auxiliary variables is no big deal either. This is actually a pretty efficient conversion in my opinion.