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?
$\begingroup$
$\endgroup$
3
-
2$\begingroup$ $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. $\endgroup$– JuhoCommented May 28, 2012 at 9:52
-
3$\begingroup$ Please include short descriptions and/or references explaining what "forward checking" and "arc consistency" are so the question is readable for non-experts. Thanks! $\endgroup$– RaphaelCommented May 28, 2012 at 9:54
-
$\begingroup$ 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)$. $\endgroup$– OptCommented May 28, 2012 at 16:07
Add a comment
|
2 Answers
$\begingroup$
$\endgroup$
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.
$\begingroup$
$\endgroup$
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.
