1
$\begingroup$

I have an assignment where i have to encode certain problem to conjunctive normal form so i can solve it by using SAT solver. I have been able to encode my problem correctly but the solver is quite slow and most likely the cause for this is the length of some clauses which i have.

So my question is:

How can one break down long clauses into smaller ones and therefore speed up the SAT solver, lets say i have following clause:

$ (x_1 \vee x_2 \vee x_3 \vee ... \vee x_n) $ where n can potentially be large number.

Is there any way to split this into smaller clauses which would be logically equivalent?

$\endgroup$
  • 2
    $\begingroup$ Every CNF is equivalent to a 3CNF, in which every clause contains at most 3 literals. You can see the reduction in any NP-completeness proof of 3SAT. I'm not sure that will speed up to SAT solver, though. $\endgroup$ – Yuval Filmus Feb 2 '17 at 20:03
4
$\begingroup$

The reason why the SAT solver is slow is unlikely to be the size of the clauses, but rather the hardness of the problem itself.

In any case, any instance of CNF-SAT can notoriously be transformed into an equisatisfiable formula with at most three literals per clause by replacing each clause in the form:

$$ ( x_1 \vee x_2 \vee \dots \vee x_n) $$

with:

$$ (x_1 \vee x_2 \vee y_1) \wedge (\neg y_1 \vee x_3 \vee y_2) \wedge \dots \wedge (\neg y_{n-4} \vee x_{n-2} \vee y_{n-3}) \wedge (\neg y_{n-3} \vee x_{n-1} \vee x_n) $$

where $\{y_i\}_{i \in \mathbb{N}}$ are fresh variables.

| cite | improve this answer | |
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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