×

zbMATH — the first resource for mathematics

Balance and filtering in structured satisfiable problems. (Preliminary report). (English) Zbl 0985.90509
Kautz, Henry (ed.) et al., LICS 2001 workshop on theory and application of satisfiability testing (SAT 2001). Boston, MA, USA, June 14-15, 2001. Amsterdam: Elsevier, Electron. Notes Discrete Math. 9, no pag., electronic only (2001).
Summary: New methods to generate hard random problem instances have driven progress on algorithms for deduction and constraint satisfaction. Recently Achlioptas et al. (AAAI 2000) introduced a new generator based on Latin squares that creates only satisfiable problems, and so can be used to accurately test incomplete (one sided) solvers. We investigate how this and other generators are biased away from the uniform distribution of satisfiable problems and show how they can be improved by imposing a balance condition. More generally, we show that the generator is one member of a family of related models that generate distributions ranging from ones that are everywhere tractable to ones that exhibit a sharp hardness threshold. We also discuss the critical role of the problem encoding in the performance of both systematic and local search solvers.
The final version of this paper appears in Proc. Seventeenth National Conference on Artificial Intelligence (IJCAI-01), Morgan-Kaufmann (2001).
For the entire collection see [Zbl 0968.90001].

MSC:
90C15 Stochastic programming
90B40 Search theory
Software:
SATO
PDF BibTeX XML Cite