3
$\begingroup$

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?

$\endgroup$
0

3 Answers 3

6
$\begingroup$

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.

$\endgroup$
4
  • $\begingroup$ Converting to CNF can make formulas like this unpleasantly large, even for SAT solvers. The problem is that a disjunction of $n$ conjunctions of $k$ literals each would, in the worst case, turn into a conjunction of $k^n$ clauses. So we'd better hope that the OP's formulas are far from the worst case. $\endgroup$ Oct 2, 2014 at 12:43
  • $\begingroup$ @AndreasBlass I am pretty sure the OP's formula has polynomial sized CNF if additional variables are introduced (which is common practice). Make OR gate $C:= A \lor B$ introducing new variables for the gate. If you disallow new variables, maybe you are right. $\endgroup$
    – joro
    Oct 2, 2014 at 13:52
  • $\begingroup$ I'll try this approach. Thanks. If it does get impossibly big for my SAT sovler. I'll comment here. $\endgroup$
    – amcalde
    Oct 2, 2014 at 13:57
  • $\begingroup$ See my answer for an efficient conversion to CNF using auxiliary variables. $\endgroup$ Oct 3, 2014 at 1:41
3
$\begingroup$

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.

$\endgroup$
3
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.