Abstract
The CRIL multi-strategy platform for SAT includes a whole family of local search techniques and some of the best Davis and Putnam strategies for checking propositional satisfiability. Most notably, it features an optimized tabu-based local search method and includes a powerful logically complete approach that combines the respective strengths of local and systematic search techniques. This platform is a comprehensive toolkit provided with most current SAT instances generators and with various user-friendly tools.
The development of the CRIL platform for SAT was supported in part by the Ganymède II project of the Contrat de plan état/Région Nord-Pas-de-Calais.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Davis, M., Putnam, H.: A Computing Procedure for Quantification Theory. Journal of the Association for Computing Machinery, 7, pp. 201–215.
Crawford, J.: Solving Satisfiability Problems Using a Combination of Systematic and Local Search. Working notes of the DIMACS Workshop on Maximum Clique, Graph Coloring, and Satisfiability (1993).
McAllexter, D., Selman, B., Kautz, H.A.: Evidence for Invariants in Local Search. Proceedings of the Fourteenth National Conference on Artificial Intelligence (AAAI'97) (1997) pp. 321–326.
Mazure, B., SaÏs, L., Grégoire, é.: Tabu Search for SAT, Proceedings of the Fourteenth National Conference on Artificial Intelligence (AAAI'97), (1997) pp. 281–285.
Mazure, B., SaÏs, L., Grégoire, é.: Detecting Logical Inconsistencies. Proceedings of Mathematics and Artificial Intelligence Symposium (1996) pp. 116–121, extended version in Annals of Mathematics and Artificial Intelligence (1998).
Selman, B., Levesque, H., Mitchell, D.: A New Method for Solving Hard Satisfiability Problems. Proceedings of the Tenth National Conference on Artificial Intelligence (AAAI'92) (1992) pp. 440–446.
Selman, B., Kautz, H.A., Cohen, B.: Local Search Strategies for Satisfiability Testing. Proceedings of the DIMACS Workshop on Maximum Clique, Graph Coloring, and Satisfiability (1993).
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mazure, B., SaÏs, L., Grégoire, é. (1998). System description: CRIL platform for SAT. In: Kirchner, C., Kirchner, H. (eds) Automated Deduction — CADE-15. CADE 1998. Lecture Notes in Computer Science, vol 1421. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0054253
Download citation
DOI: https://doi.org/10.1007/BFb0054253
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64675-4
Online ISBN: 978-3-540-69110-5
eBook Packages: Springer Book Archive