Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Predicting and detecting symmetries in FOL finite model search
Audemard G., Benhamou B., Henocque L. Journal of Automated Reasoning36 (3):177-212,2006.Type:Article
Date Reviewed: Jun 4 2007

Audemard et al. study the impact of variable and value ordering heuristics on the heavy-tailedness of runtime distributions of backtrack search procedures. Specifically, they discuss the heavy-tailed behavior of the backtrack procedure at runtime. At the beginning of the paper, the authors mention the nonstandard probability distributions that are used as models in weather forecasting, stock market analysis, and combinatorial search methods. They recall that some constraint satisfaction problems (CSPs), like graph coloring and satisfiability, may have hard instances. The authors claim that the structure of the algorithms used to solve the CSPs plays an important role in avoiding the appearance of hard instances. Here, I have a different view on a hard instance. A hard instance is hard by its own nature, and an efficient algorithm with a given heuristic can be used to solve it.

The authors refer mainly to the work of Gomes et al. [1], who studied the transition between heavy-tailed and nonheavy-tailed behavior in runtime distributions. The authors have reproduced the experiments of Gomes et al., and made some observations while studying heavy-tailed behavior in the context of maintaining arc consistency (MAC). They observed that, when ordering the variables according to a given heuristic, like variables, minimum domains might avoid the heavy tails even for problems with 100 variables. The authors did some experiments using different well-known heuristics with the MAC algorithm, and applied them to the quasigroups with holes problem (QHP). Here, the authors also make some observations, like the fact that selecting the heuristics carefully might eliminate heavy-tailed behavior. They study the different combinations of variables and values (that is, ordering the variables according to their domains and degrees), and discuss their impact on the QHP using MAC.

The paper is long, and does not contain original results. The only observations made were in reproducing the experiments of Gomes et al. This is a technical paper, where the authors try to examine the effects of reordering the variables of CSPs. It is well known that reordering the variables of a CSP according to its domain (or minimum degree like the Brelaz algorithm for graph coloring) reduces the heavy-tailedness of the problem.

Almost all of the given definitions (binary constraint satisfaction problem, arc consistency, search algorithm, search tree, mistake point, refutations, and so on) are already known in the literature, and the authors have only changed some notations. The authors mention arc consistency, eight-queens, Latin square, the quasigroup completion problem, and the Monte Carlo problem. In my view, it would be much better to focus on one or two problems, rather than on a family of different CSPs where each one may have a specific structure. The authors mix many things, and try to comment and make observations about them. They talk about a significant improvement in an algorithm that they have already published; however, the improvement was not clear to me. A large number of references are given in the bibliography section to convince the reader. The major problem of this paper is its focus. As a reader, I couldn’t see things clearly.

Reviewer:  Jihad Jaam Review #: CR134352 (0805-0504)
1) Gomes, C.P.; Selman, B.; Crato, N.; Kautz, H. Heavy-tailed phenomena in satisfiability and constraint satisfaction problems. Automated Reasoning 24, 1-2(2000), 67–100.
Bookmark and Share
 
Deduction And Theorem Proving (I.2.3 )
 
 
Computations In Finite Fields (F.2.1 ... )
 
 
Constrained Optimization (G.1.6 ... )
 
 
Heuristic Methods (I.2.8 ... )
 
 
Sorting And Searching (F.2.2 ... )
 
 
Nonnumerical Algorithms And Problems (F.2.2 )
 
  more  
Would you recommend this review?
yes
no
Other reviews under "Deduction And Theorem Proving": Date
Noninteractive zero-knowledge
Blum M., De Santis A., Micali S., Persiano G. SIAM Journal on Computing 20(6): 1084-1118, 1991. Type: Article
Jan 1 1993
Cut elimination and automatic proof procedures
Zhang W. Theoretical Computer Science 91(2): 265-284, 1991. Type: Article
Apr 1 1993
A non-reified temporal logic
Bacchus F., Tenenberg J., Koomen J. Artificial Intelligence 52(1): 87-108, 1991. Type: Article
Oct 1 1992
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy