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? 



What kind of SAT am I dealing with here?
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.


