×

zbMATH — the first resource for mathematics

Regular-SAT: A many-valued approach to solving combinatorial problems. (English) Zbl 1121.68104
Summary: Regular-SAT is a constraint programming language between CSP and SAT that – by combining many of the good properties of each paradigm – offers a good compromise between performance and expressive power. Its similarity to SAT allows us to define a uniform encoding formalism, to extend existing SAT algorithms to Regular-SAT without incurring excessive overhead in terms of computational cost, and to identify phase transition phenomena in randomly generated instances. On the other hand, Regular-SAT inherits from CSP more compact and natural encodings that maintain more the structure of the original problem. Our experimental results – using a range of benchmark problems – provide evidence that Regular-SAT offers practical computational advantages for solving combinatorial problems.

MSC:
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Achlioptas, D.; Gomes, C.P.; Kautz, H.; Selman, B., Generating satisfiable problem instances, (), 256-261
[2] Bayardo, R.J.; Schrag, R.C., Using CSP look-back techniques to solve real-world SAT instances, (), 203-208
[3] Beckert, B.; Hähnle, R.; Manyà, F., The SAT problem of signed CNF formulas, (), 61-82
[4] R. Béjar, Systematic and local search algorithms for regular-sat, Ph.D. Thesis, Universitat Autònoma de Barcelona, 2000.
[5] Béjar, R.; Manyà, F., A comparison of systematic and local search algorithms for regular CNF formulas, (), 22-31 · Zbl 0935.68094
[6] Béjar, R.; Manyà, F., Solving combinatorial problems with regular local search algorithms, (), 33-43 · Zbl 0944.68166
[7] Béjar, R.; Manyà, F., Phase transitions in the regular random 3-SAT problem, (), 292-300
[8] Béjar, R.; Manyà, F., Solving the round Robin problem using propositional logic, (), 262-266
[9] Cheeseman, P.; Kanefsky, B.; Taylor, W.M., Where the really hard problems are, () · Zbl 0747.68064
[10] J. C. Culberson, F. Luo, Exploring the k-colorable landscape with iterated greedy, in: Cliques, Coloring and Satisfiability, of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 36, 1996, pp. 245-284. · Zbl 0864.90117
[11] Davis, M.; Logemann, G.; Loveland, D., A machine program for theorem-proving, Commun. of the ACM, 5, 394-397, (1962) · Zbl 0217.54002
[12] Frisch, A.M.; Peugniez, T.J., Solving non-Boolean satisfiability problems with stochastic local search, (), 282-288
[13] Gent, I.P.; MacIntyre, E.; Prosser, P.; Walsh, T., The constrainedness of search, ()
[14] C. Gomes, H. Kautz, Y. Ruan, Qwh—a structured benchmark domain for local search, Technical Report, Intelligent Information Systems Institute (IISI), Cornell University, 2001.
[15] Gomes, C.P.; Selman, B., Problem structure in the presence of perturbations, (), 221-226
[16] Gomes, C.; Selman, B.; Crato, N., Heavy-tailed distributions in combinatorial search, (), 121-135
[17] Haken, A., The intractability of resolution, Theoret. comput. sci., 39, 297-308, (1985) · Zbl 0586.03010
[18] Hähnle, R., Short conjunctive normal forms in finitely-valued logics, J. logic comput., 4, 6, 905-927, (1994) · Zbl 0818.03003
[19] R. Hähnle, Automated Deduction in Multiple-Valued Logics, International Series of Monographs in Computer Science, vol. 10, Oxford University Press, Oxford, 1994.
[20] Hähnle, R., Exploiting data dependencies in many-valued logics, J. appl. non-classical logics, 6, 49-69, (1996) · Zbl 0836.03013
[21] Hoos, H.H.; Stützle, T., Local search algorithms for SAT: an empirical evaluation, J. automat. reason., 24, 4, 421-481, (2000) · Zbl 0961.68039
[22] Kautz, H.A.; Selman, B., Pushing the envelope: planning, propositional logic, and stochastic search, ()
[23] Li, C.M.; Anbulagan, Look-ahead versus look-back for satisfiability problems, (), 341-355
[24] Marques-Silva, J.P.; Guerra, L., Algorithms for satisfiability in combinational circuits based on backtrack search and recursive learning, ()
[25] Mitchell, D.; Selman, B.; Levesque, H., Hard and easy distributions of SAT problems, ()
[26] R. Monasson, R. Zecchina, S. Kirkpatrick, B. Selman, L. Troyansky, Determining computacional complexity from characteristic ‘phase transitions’, Nature 400 (8). · Zbl 1369.68244
[27] M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, S. Malik, Chaff: engineering an efficient sat solver, in: 39th Design Automation Conference, 2001.
[28] Régin, J.-C., A filtering algorithm for constraints of difference in csps, (), 362-367
[29] Selman, B.; Kautz, H.A.; Cohen, B., Noise strategies for improving local search, (), 337-343
[30] Stergiou, K.; Walsh, T., The difference all-difference makes, ()
[31] M. Velev, R. Bryant, Effective use of boolean satisfiability procedures in the formal verification of superscalar and vliw microprocessors, in: 38th Design Automation Conference (DAC’01), 2001. · Zbl 1069.68119
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.