{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T14:18:40Z","timestamp":1775053120787,"version":"3.50.1"},"reference-count":38,"publisher":"Springer Science and Business Media LLC","issue":"1-3","license":[{"start":{"date-parts":[[2006,1,19]],"date-time":"2006-01-19T00:00:00Z","timestamp":1137628800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2006,10,5]]},"DOI":"10.1007\/s10817-005-9011-0","type":"journal-article","created":{"date-parts":[[2006,1,18]],"date-time":"2006-01-18T12:33:03Z","timestamp":1137587583000},"page":"143-179","source":"Crossref","is-referenced-by-count":16,"title":["Solving Non-Boolean Satisfiability Problems with Stochastic Local Search: A Comparison of Encodings"],"prefix":"10.1007","volume":"35","author":[{"given":"Alan M.","family":"Frisch","sequence":"first","affiliation":[]},{"given":"Timothy J.","family":"Peugniez","sequence":"additional","affiliation":[]},{"given":"Anthony J.","family":"Doggett","sequence":"additional","affiliation":[]},{"given":"Peter W.","family":"Nightingale","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,1,19]]},"reference":[{"key":"9011_CR1","unstructured":"Achlioptas, D., Gomes, C. P., Kautz, H. A. and Selman, B. (2000) Generating satisfiable problem instances, in Proc. of the Seventeenth National Conf. on Artificial Intelligence, pp. 256\u2013261."},{"key":"9011_CR2","unstructured":"B\u00e9jar, R. (2000) Systematic and Regular Search Algorithms for Regular-SAT. Ph.D. thesis, Universitat Auton\u00f2ma de Barcelona."},{"key":"9011_CR3","doi-asserted-by":"crossref","unstructured":"B\u00e9jar, R. and Many\u00e0, F. (1999a) A comparison of systematic and local search algorithms for regular CNF formulas, in A. Hunter and S. Parsons (eds.), Proc. Fifth European Conference on Symbolic and Quantitative Approaches to Reasoning with Uncertainty, ECSQARU\u201999, London, UK, Vol. 1638 of Lecture Notes in Artificial Intelligence, pp. 22\u201331.","DOI":"10.1007\/3-540-48747-6_3"},{"key":"9011_CR4","unstructured":"B\u00e9jar, R. and Many\u00e0, F. (1999b) Solving combinatorial problems with regular local search algorithm, in H. Ganzinger and D. McAllester (eds.), Proc. 6th Int. Conference on Logic for Programming and Automated Reasoning, LPAR, Tbilisi, Georgia, Vol. 1705 of Lecture Notes in Artificial Intelligence, pp. 33\u201343."},{"key":"9011_CR5","unstructured":"B\u00e9jar, R. and Many\u00e0, F. (2000) Solving the round robin problem using propositional logic, in Proc. of the Seventeenth National Conf. on Artificial Intelligence, pp. 261\u2013266."},{"key":"9011_CR6","doi-asserted-by":"crossref","unstructured":"B\u00e9jar, R., Cabicol, A., Fern\u00e0ndez, C., Many\u00e1, F. and Gomes, C. P. (2001) Capturing structure with satisfiability, in T. Walsh (ed.), Principles and Practice of Constraint Programming \u2013 CP 2001, pp. 135\u2013149.","DOI":"10.1007\/3-540-45578-7_10"},{"key":"9011_CR7","unstructured":"Brafman, R. I. and Hoos, H. H. (1999) To encode or not to encode \u2013 I: linear planning, in Proc. of the Sixteenth Int. Joint Conf. on Artificial Intelligence, pp. 988\u2013993."},{"key":"9011_CR8","doi-asserted-by":"crossref","unstructured":"Colbourn, C. J. (1983) Embedding partial steiner triple systems is NP-complete, J. Comb. Theory 35.","DOI":"10.1016\/0097-3165(83)90031-6"},{"key":"9011_CR9","doi-asserted-by":"crossref","unstructured":"Davis, M., Logemann, G. and Loveland, D. (1962) A machine program for theorem proving, Commun. ACM 5(7).","DOI":"10.1145\/368273.368557"},{"key":"9011_CR10","unstructured":"Ernst, M. D., Millstein, T. D. and Weld, D. S. (1997) Automatic SAT-compilation of planning problems, in Proc. of the Fifteenth Int. Joint Conf. on Artificial Intelligence, pp. 1169\u20131176."},{"key":"9011_CR11","unstructured":"Frisch, A. M. and Peugniez, T. J. (1998) Solving non-Boolean satisfiability problems with local search, in Fifth Workshop on Automated Reasoning: Bridging the Gap between Theory and Practice, St. Andrews, Scotland."},{"key":"9011_CR12","unstructured":"Frisch, A. M. and Peugniez, T. J. (2001) Solving non-Boolean satisfiability problems with stochastic local search, in Proc. of the Seventeenth Int. Joint Conf. on Artificial Intelligence, Seattle, Washington, pp. 282\u2013288."},{"key":"9011_CR13","unstructured":"Gent, I. P. (2002) Arc consistency in SAT, in Proc. of the Fifteenth European Conf. on Artificial Intelligence, pp. 121\u2013125."},{"key":"9011_CR14","unstructured":"Gent, I. P. and Walsh, T. (eds.), CSPLib: A Problem Library for Constraints. http:\/\/www.csplib.org ."},{"key":"9011_CR15","unstructured":"Gomes, C. P. and Selman, B. (1997) Problem structure in the presence of perturbations, in Proc. of the Fourteenth National Conf. on Artificial Intelligence, pp. 221\u2013226."},{"key":"9011_CR16","unstructured":"Gomes, C. P., Kautz, H. A. and Ruan, Y. (2001) lsencode: A Generator of Quasigroup with Holes and Quasigroup Completion Problems."},{"key":"9011_CR17","unstructured":"Hoos, H. H. (1998) Stochastic Local Search\u2013Methods, Models, Applications. Ph.D. thesis, Technical University of Darmstadt."},{"key":"9011_CR18","unstructured":"Hoos, H. H. (1999) SAT-encodings, search space structure, and local search performance, in Proc. of the Sixteenth Int. Joint Conf. on Artificial Intelligence, pp. 296\u2013302."},{"key":"9011_CR19","unstructured":"Jonsson, A. K. and Ginsberg, M. L. (1993) Experimenting with new systematic and nonsystematic search techniques, in Working Notes of the 1993 AAAI Spring Symposium on AI and NP-Hard Problems, Stanford University in Palo Alto, California."},{"key":"9011_CR20","unstructured":"Kautz, H. A. and Selman, B. (1992) Planning as satisfiability, in B. Neumann (ed.), Proc. of the Tenth European Conf. on Artificial Intelligence, Vienna, Austria, pp. 359\u2013363."},{"key":"9011_CR21","unstructured":"Kautz, H. A. and Selman, B. (1996) Pushing the envelope: planning, propositional logic, and stochastic search, in Proc. of the Thirteenth National Conf. on Artificial Intelligence, Portland, Oregon, USA, pp. 1202\u20131207."},{"key":"9011_CR22","unstructured":"Kautz, H. A., McAllester, D. and Selman, B. (1996) Encoding plans in propositional logic, in L. C. Aiello, J. Doyle, and S. Shapiro (eds.), Principles of Knowledge Representation and Reasoning: Proc. of the Fifth Int. Conf. San Francisco, pp. 374\u2013385."},{"key":"9011_CR23","unstructured":"Kautz, H. A., McAllester, D. and Selman, B. (1997) Exploiting variable dependency in local search (Abstract), in Poster Session Abstracts of IJCAI-97, p. 57."},{"key":"9011_CR24","unstructured":"Kautz, H. A., Ruan, Y., Achiloptas, D., Gomes, C., Selman, B. and Stickel, M. (2001) Balance and filtering in structured satisfiable problems, in Proc. of the Seventeenth Int. Joint Conf. on Artificial Intelligence, Seattle, Washington, pp. 351\u2013358."},{"key":"9011_CR25","unstructured":"Li, C. M. and Anbulagan (1997) Heuristics based on unit propagation for satisfiability problems, in Proc. of the Fifteenth Int. Joint Conf. on Artificial Intelligence, pp. 366\u2013371."},{"key":"9011_CR26","unstructured":"Mitchell, D., Selman, B. and Levesque, H. J. (1992) Hard and easy distributions of SAT problems, in Proc. of the Tenth National Conf. on Artificial Intelligence, San Jose, CA, pp. 459\u2013465."},{"key":"9011_CR27","unstructured":"Peugniez, T. J. (1998) Solving Non-Boolean Satisfiability Problems with Local Search. BSc dissertation, Department of Computer Science, University of York."},{"key":"9011_CR28","unstructured":"Prestwich, S. (2004) Local search on SAT-encoded colouring problems, in Theory and Applications of Satisfiability Testing: 6th Int. Conf., pp. 105\u2013119."},{"key":"9011_CR29","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1613\/jair.49","volume":"1","author":"R. Sebastiani","year":"1994","unstructured":"Sebastiani, R. (1994) Applying GSAT to non-clausal formulas, J. Artif. Intell. Res. 1, 309\u2013314.","journal-title":"J. Artif. Intell. Res."},{"key":"9011_CR30","unstructured":"Selman, B., Levesque, H. J. and Mitchell, D. (1992) A new method for solving hard satisfiability problems in Proc. of the Tenth National Conf. on Artificial Intelligence, pp. 440\u2013446."},{"key":"9011_CR31","unstructured":"Selman, B., Kautz, H. A. and Cohen, B. (1994) Noise strategies for improving local search, in Proc. of the Twelfth National Conf. on Artificial Intelligence, Menlo Park, CA, USA, pp. 337\u2013343."},{"key":"9011_CR32","unstructured":"Shaw, P. (1998) Using constraint programming and local search methods to solve vehicle routing problems, in Principles and Practice of Constraint Programming \u2013 CP 1998, pp. 417\u2013431."},{"key":"9011_CR33","unstructured":"Shaw, P., Stergiou, K. and Walsh, T. (1998) Arc consistency and quasigroup completion, in Proceedings of ECAI98 Workshop on Non-binary Constraints."},{"key":"9011_CR34","unstructured":"Stamm-Wilbrandt, H. (1993) Programming in Propositional Logic, or Reductions: Back to the Roots (Satisfiability), Technical report, Institut f\u00fcr Informatik III, Universit\u00e4t Bonn."},{"key":"9011_CR35","unstructured":"Stock, P. G. (2000) Solving Non-Boolean Satisfiability with the Davis-Putnam Method, BSc dissertation, Dept. of Computer Science, Univ. of York."},{"key":"9011_CR36","unstructured":"Van Hentenryck, P. and Michel, L. (2003) Control abstractions for local search, in Principles and Practice of Constraint Programming \u2013 CP 2003, pp. 65\u201380."},{"key":"9011_CR37","unstructured":"Walser, J. P. (1997) Solving linear pseudo-boolean constraint problems with local search, in Proc. of the Fourteenth National Conf. on Artificial Intelligence, pp. 269\u2013274."},{"key":"9011_CR38","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-48369-1","volume-title":"Integer Optimization by Local Search: A Domain-Independent Approach","author":"J. P. Walser","year":"1999","unstructured":"Walser, J. P. (1999) Integer Optimization by Local Search: A Domain-Independent Approach, Springer, Berlin Heidelberg New York."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-005-9011-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-005-9011-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-005-9011-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T01:21:46Z","timestamp":1559265706000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-005-9011-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,1,19]]},"references-count":38,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2006,10,5]]}},"alternative-id":["9011"],"URL":"https:\/\/doi.org\/10.1007\/s10817-005-9011-0","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,1,19]]}}}