# Forward checking vs arc consistency on 3-SAT

If I were to let the variables be the propositions and, constraint be all clauses being satisfied, which technique would be more effective in solving 3-SAT? Forward checking or arc consistency? From what I gathered forward-checking is $O(n)$, while Arc consistency is about $O(8c)$ where c is the number of constraints (According to this page). So perhaps forward -checking is faster somehow? How should I determine which to use?

• $O(8c) = O(c)$, but where do you get the constant $8$? The time complexity of AC-3 is $O(cd^3)$, where $c$ is the number of constraints and $d$ the maximum size of a variable domain. FC runs in $O(n)$ time, where $n$ is the number of neighbouring variables. – Juho May 28 '12 at 9:52
• Please include short descriptions and/or references explaining what "forward checking" and "arc consistency" are so the question is readable for non-experts. Thanks! – Raphael May 28 '12 at 9:54
• Where are you getting the $O(n)$ for forward checking? Each forward check would also require unit propagation for every variable which in the worst case could be $O(c)$. – Opt May 28 '12 at 16:07

## 2 Answers

Both forward checking (FC) and arc consistency (AC) are methods of inference. Regardless of the problem you are solving, choosing a specific method of inference is always a tradeoff. Basically, the more you are willing to pay in terms of time, the more you gain in terms of strength of inference. So yes, it is faster to perform forward checking than arc consistency, but arc consistency is more effective at pruning the search space. If you are willing to pay even more, there are even stronger forms of consistency. The book by Russell & Norvig gives a nice, quick introduction.

Both FC and AC are relatively cheap and easy to implement, too. The suitable choice depends on the specific structure of your problem. I think at least in general, it is best that you experiment with both.

In practice, for almost all SAT problems except the most trivial, AC will be faster -- usually exponentially faster.

While AC is slightly slower per node, it can often perform reasoning steps which remove any exponential part of search.