# 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