{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,4,6]],"date-time":"2023-04-06T21:30:13Z","timestamp":1680816613979},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2007,6,23]],"date-time":"2007-06-23T00:00:00Z","timestamp":1182556800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Constraints"],"published-print":{"date-parts":[[2007,7,13]]},"DOI":"10.1007\/s10601-007-9022-z","type":"journal-article","created":{"date-parts":[[2007,6,22]],"date-time":"2007-06-22T19:58:29Z","timestamp":1182542309000},"page":"345-369","source":"Crossref","is-referenced-by-count":3,"title":["Satisfiability Testing of Boolean Combinations of Pseudo-Boolean Constraints using Local-search Techniques"],"prefix":"10.1007","volume":"12","author":[{"given":"Lengning","family":"Liu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Miros\u0142aw","family":"Truszczy\u0144ski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2007,6,23]]},"reference":[{"key":"9022_CR1","unstructured":"Aloul, F. A., Ramani, A., Markov, I., & Sakallah, K. (2002). PBS: A backtrack-search pseudo-Boolean solver and optimizer. In Proceedings of the 5th International Symposium on Theory and Applications of Satisfiability (pp. 346\u2013353)."},{"key":"9022_CR2","unstructured":"Barth, P. (1995). A Davis-Putnam based elimination algorithm for linear pseudo-Boolean optimization. Technical Report, Max-Planck-Institut f\u00fcr Informatik. MPI-I-95-2-003."},{"key":"9022_CR3","series-title":"LNCS","first-page":"71","volume-title":"Proceedings of the 11th Annual Symposium on Theoretical Aspects of Computer Science (STACS-1994)","author":"B. Benhamou","year":"1994","unstructured":"Benhamou, B., Sais, L., & Siegel, P. (1994). Two proof procedures for a cardinality based language in propositional calculus. In Proceedings of the 11th Annual Symposium on Theoretical Aspects of Computer Science (STACS-1994). LNCS, volume 775 (pp. 71\u201382). Berlin Heidelberg New York: Springer."},{"key":"9022_CR4","first-page":"635","volume-title":"The 18th National Conference on Artificial Intelligence (AAAI-2002)","author":"H. E. Dixon","year":"2002","unstructured":"Dixon, H. E., & Ginsberg, M. L. (2002). Inference methods for a pseudo-Boolean satisfiability solver. In The 18th National Conference on Artificial Intelligence (AAAI-2002) (pp. 635\u2013640). Menlo Park, CA: AAAI Press."},{"key":"9022_CR5","unstructured":"East, D., & Truszczy, M. (2001). Propositional satisfiability in answer-set programming. In Proceedings of Joint German\/Austrian Conference on Artificial Intelligence (KI-2001). LNAI, volume 2174 (pp. 138\u2013153). Berlin Heidelberg New York: Springer."},{"key":"9022_CR6","volume-title":"Computers and Intractability. A Guide to the Theory of NP-completeness","author":"M. R. Garey","year":"1979","unstructured":"Garey, M. R., & Johnson, D. S. (1979). Computers and Intractability. A Guide to the Theory of NP-completeness. San Francisco, CA: Freeman."},{"key":"9022_CR7","doi-asserted-by":"crossref","unstructured":"Goldberg, E., & Novikov, Y. (2002). Berkmin: a fast and robust sat-solver. In DATE-2002 (pp. 142\u2013149).","DOI":"10.1109\/DATE.2002.998262"},{"key":"9022_CR8","unstructured":"Hoos, H. (1999). On the run-time behaviour of stochastic local search algorithms for sat. In Proceedings of The Sixteenth National Conference on Artificial Intelligence (AAAI-99), Orlando, Florida (pp. 661\u2013666)."},{"key":"9022_CR9","unstructured":"Hoos, H. H., & Stutzle, T. (1998). A characterization the run-time behaviour of stochastic local search. http:\/\/www.cs.ubc.ca\/~hoos\/Publ\/aida-98-01.ps ."},{"key":"9022_CR10","volume-title":"Stochastic Local Search Foundations and Applications","author":"H. H. Hoos","year":"2004","unstructured":"Hoos H. H., & St\u00fctzle, T. (2004). Stochastic Local Search Foundations and Applications. San Francisco, CA: Morgan Kaufmann."},{"key":"9022_CR11","first-page":"291","volume-title":"Proccedings of the 17th National Conference on Artificial Intelligence (AAAI-2000)","author":"C. M. Li","year":"2000","unstructured":"Li, C. M. (2000). Integrating equivalency reasoning into Davis-Putnam procedure. In Proccedings of the 17th National Conference on Artificial Intelligence (AAAI-2000) (pp. 291\u2013296). Menlo Park, CA: AAAI Press."},{"key":"9022_CR12","first-page":"342","volume-title":"Proceedings of the 3rd International Conference on Principles and Practice of Constraint Programming. LNCS, volume 1330","author":"C. M. Li","year":"1997","unstructured":"Li, C. M., & Anbulagan, M. (1997). Look-ahead versus look-back for satisfiability problems. In Proceedings of the 3rd International Conference on Principles and Practice of Constraint Programming. LNCS, volume 1330 (pp. 342\u2013356). Berlin Heidelberg New York: Springer."},{"key":"9022_CR13","unstructured":"Liu, L. (2006). Computational tools for solving hard search problems. Ph.D. Thesis, University of Kentucky. ftp:\/\/ftp.cs.uky.edu\/cs\/manuscripts\/LiuDissertation.pdf ."},{"key":"9022_CR14","first-page":"495","volume-title":"Proceedings of the 9th International Conference on Principles and Practice of Constraint Programming (CP-2003). LNCS, volume 2833","author":"L. Liu","year":"2003","unstructured":"Liu, L., & Truszczy\u0144ski, M. (2003). Local-search techniques in propositional logic extended with cardinality atoms. In Rossi, F., ed., Proceedings of the 9th International Conference on Principles and Practice of Constraint Programming (CP-2003). LNCS, volume 2833 (pp. 495\u2013509). Berlin Heidelberg New York: Springer."},{"key":"9022_CR15","first-page":"98","volume-title":"Local search techniques for Boolean combinations of pseudo-Boolean constraints","author":"L. Liu","year":"2006","unstructured":"Liu, L., & Truszczy\u0144ski, M. (2006) Local search techniques for Boolean combinations of pseudo-Boolean constraints. In Proceedings of The Twentieth National Conference on Artificial Intelligence (AAAI-06) (pp. 98\u2013103). Menlo Park, CA: AAAI Press."},{"key":"9022_CR16","unstructured":"Manquinho, V., & Roussel, O. (2005). Pseudo Boolean evaluation 2005. http:\/\/www.cril.univ-artois.fr\/PB05\/ ."},{"key":"9022_CR17","unstructured":"Manquinho, V., & Roussel, O. (2006). Pseudo Boolean evaluation 2006. http:\/\/www.cril.univ-artois.fr\/PB06\/ ."},{"key":"9022_CR18","doi-asserted-by":"crossref","first-page":"103","DOI":"10.3233\/SAT190018","volume":"2","author":"V. M. Manquinho","year":"2006","unstructured":"Manquinho, V. M., & Roussel, O. (2006). The first evaluation of pseudo-Boolean solvers (pb\u201905). Journal on Satisfiability, Boolean Modeling and Computation 2, 103\u2013143.","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"9022_CR19","doi-asserted-by":"crossref","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"J. P. Marques-Silva","year":"1999","unstructured":"Marques-Silva, J. P., & Sakallah, K. A. (1999). GRASP: A new search algorithm for satisfiability. IEEE Trans. Comput. 48, 506\u2013521.","journal-title":"IEEE Trans. Comput."},{"key":"9022_CR20","first-page":"530","volume-title":"Proceedings of the 38th ACM IEEE Design Automation Conference","author":"M. Moskewicz","year":"2001","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., & Malik, S. (2001). Chaff: engineering an efficient SAT solver. In Proceedings of the 38th ACM IEEE Design Automation Conference (pp. 530\u2013535). New York: ACM Press."},{"key":"9022_CR21","unstructured":"Prestwich, S. D. (2002). Randomised backtracking for linear pseudo-Boolean constraint problems. In Proceedings of the 4th International Workshop on Integration of AI and OR techniques in Constraint Programming for Combinatorial Optimisation Problems, (CPAIOR-2002) (pp. 7\u201320). http:\/\/www.emn.fr\/x-info\/cpaior\/Proceedings\/CPAIOR.pdf ."},{"key":"9022_CR22","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 (Research Note). J. Artif. Intell. Res. 1, 309\u2013314.","journal-title":"J. Artif. Intell. Res."},{"key":"9022_CR23","first-page":"337","volume-title":"Proceedings of the 12th National Conference on Artificial Intelligence (AAAI-1994), Seattle, USA","author":"B. Selman","year":"1994","unstructured":"Selman, B., Kautz, H. A., & Cohen, B. (1994). Noise strategies for improving local search. In Proceedings of the 12th National Conference on Artificial Intelligence (AAAI-1994), Seattle, USA (pp. 337\u2013343). Menlo Park, CA: AAAI Press."},{"key":"9022_CR24","unstructured":"Walser, J. (1997). SLS PB solver wsatoip. http:\/\/www.ps.uni-sb.de\/~walser\/wsatpb\/wsatpb.html ."},{"key":"9022_CR25","first-page":"269","volume-title":"Proceedings of the 11th National Conference on Artificial Intelligence (AAAI-97)","author":"J. P. Walser","year":"1997","unstructured":"Walser, J. P. (1997). Solving linear pseudo-Boolean constraints with local search. In Proceedings of the 11th National Conference on Artificial Intelligence (AAAI-97) (pp. 269\u2013274). Menlo Park, CA: AAAI Press."},{"key":"9022_CR26","doi-asserted-by":"crossref","unstructured":"Zhang, H. (1997). SATO: an efficient propositional prover. In Proceedings of the International Conference on Automated Deduction (CADE-97). LNAI, volume 1104 (pp. 308\u2013312).","DOI":"10.1007\/3-540-63104-6_28"}],"container-title":["Constraints"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10601-007-9022-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10601-007-9022-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10601-007-9022-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,23]],"date-time":"2020-04-23T08:38:27Z","timestamp":1587631107000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10601-007-9022-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,6,23]]},"references-count":26,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2007,7,13]]}},"alternative-id":["9022"],"URL":"https:\/\/doi.org\/10.1007\/s10601-007-9022-z","relation":{},"ISSN":["1383-7133","1572-9354"],"issn-type":[{"value":"1383-7133","type":"print"},{"value":"1572-9354","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,6,23]]}}}