{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,12]],"date-time":"2025-12-12T13:16:25Z","timestamp":1765545385163},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540372066"},{"type":"electronic","value":"9783540372073"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11814948_37","type":"book-chapter","created":{"date-parts":[[2006,7,18]],"date-time":"2006-07-18T10:12:38Z","timestamp":1153217558000},"page":"410-423","source":"Crossref","is-referenced-by-count":7,"title":["Counting Models in Integer Domains"],"prefix":"10.1007","author":[{"given":"Ant\u00f3nio","family":"Morgado","sequence":"first","affiliation":[]},{"given":"Paulo","family":"Matos","sequence":"additional","affiliation":[]},{"given":"Vasco","family":"Manquinho","sequence":"additional","affiliation":[]},{"given":"Jo\u00e3o","family":"Marques-Silva","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"37_CR1","doi-asserted-by":"crossref","unstructured":"Aloul, F., Ramani, A., Markov, I., Sakallah, K.: Generic ILP versus specialized 0-1 ILP: An update. In: International Conference on Computer-Aided Design, November 2002, pp. 450\u2013457 (2002)","DOI":"10.1145\/774572.774638"},{"key":"37_CR2","doi-asserted-by":"crossref","unstructured":"Bacchus, F., Dalmao, S., Pitassi, T.: Algorithms and complexity results for #SAT and bayesian inference. In: Symposium on Foundations of Computer Science, pp. 340\u2013351 (2003)","DOI":"10.1109\/SFCS.2003.1238208"},{"key":"37_CR3","unstructured":"Bailleux, O., Boufkhad, Y.: Full CNF encoding: The counting constraints case. In: Seventh International Conference on Theory and Applications of Satisfiability Testing (2004)"},{"key":"37_CR4","doi-asserted-by":"crossref","unstructured":"Bailleux, O., Boufkhad, Y., Roussel, O.: A translation of pseudo Boolean constraints to SAT. Journal on Satisfiability, Boolean Modeling and Computation\u00a02 (March 2006)","DOI":"10.3233\/SAT190021"},{"key":"37_CR5","unstructured":"Barvinok, A., Pommersheim, J.: An algorithmic theory of lattice points in polyhedra. In: New Perspectives in Algebraic Combinatorics, vol.\u00a038, pp. 91\u2013147. MSRI Publications, Cambridge University Press (1999)"},{"key":"37_CR6","unstructured":"Bayardo, R.J., Pehoushek, J.D.: Counting models using connected components. In: National Conference on Artificial Intelligence (2000)"},{"issue":"1","key":"37_CR7","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/j.tcs.2003.10.002","volume":"313","author":"B. Boigelot","year":"2004","unstructured":"Boigelot, B., Latour, L.: Counting the solutions of presburger equations without enumerating them. Theoretical Computer Science\u00a0313(1), 17\u201329 (2004)","journal-title":"Theoretical Computer Science"},{"key":"37_CR8","doi-asserted-by":"crossref","unstructured":"Chai, D., Kuehlmann, A.: A Fast Pseudo-Boolean Constraint Solver. In: Proceedings of the Design Automation Conference, pp. 830\u2013835 (2003)","DOI":"10.1145\/775832.776041"},{"key":"37_CR9","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Translating pseudo-Boolean constraints into SAT. Journal on Satisfiability, Boolean Modeling and Computation\u00a02 (March 2006)","DOI":"10.3233\/SAT190014"},{"key":"37_CR10","unstructured":"Johnson, D.S., Trick, M.A.: Second DIMACS Implementation Challenge. DIMACS Series in Discrete Mathematics and Theoretical Computer Science (1994)"},{"issue":"4","key":"37_CR11","doi-asserted-by":"publisher","first-page":"1273","DOI":"10.1016\/j.jsc.2003.04.003","volume":"38","author":"J.A.D. Loera","year":"2004","unstructured":"Loera, J.A.D., Hemmecke, R., Tauzer, J., Yoshida, R.: Effective lattice point counting in rational convex polytopes. J. Symb. Comput.\u00a038(4), 1273\u20131302 (2004)","journal-title":"J. Symb. Comput."},{"key":"37_CR12","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Applying SAT methods in unbounded symbolic model checking. In: International Conference on Computer-Aided Verification (2002)","DOI":"10.1007\/3-540-45657-0_19"},{"key":"37_CR13","doi-asserted-by":"crossref","unstructured":"Morgado, A., Matos, P., Manquinho, V., Marques-Silva, J.: Counting models in integer domains. Technical Report 05\/2006, INESC-ID (March 2006)","DOI":"10.1007\/11814948_37"},{"key":"37_CR14","doi-asserted-by":"crossref","DOI":"10.1002\/9781118627372","volume-title":"Integer and Combinatorial Optimization","author":"G.L. Nemhauser","year":"1988","unstructured":"Nemhauser, G.L., Wolsey, L.A.: Integer and Combinatorial Optimization. John Wiley & Sons, Chichester (1988)"},{"key":"37_CR15","doi-asserted-by":"crossref","unstructured":"Pizzuti, C.: Computing Prime Implicants by Integer Programming. In: Proceedings of the International Conference on Tools with Artificial Intelligence, November 1996, pp. 332\u2013336 (1996)","DOI":"10.1109\/TAI.1996.560473"},{"key":"37_CR16","doi-asserted-by":"crossref","unstructured":"Pugh, W.: Counting solutions to presburger formulas: How and why. In: Conference on Programming Language Design and Implementation, June 1994, pp. 121\u2013134 (1994)","DOI":"10.1145\/178243.178254"},{"key":"37_CR17","unstructured":"Ravi, K., Somenzi, F.: Minimal satisfying assignments for conjunctive normal formulae. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems (2004)"},{"key":"37_CR18","unstructured":"Sang, T., Bacchus, F., Beame, P., Kautz, H.A., Pitassi, T.: Combining component caching and clause learning for effective model counting. In: International Conference on Theory and Applications of Satisfiability Testing (May 2004)"},{"issue":"2","key":"37_CR19","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/S0020-0190(98)00144-6","volume":"68","author":"J.P. Warners","year":"1998","unstructured":"Warners, J.P.: A linear-time transformation of linear inequalities into conjunctive normal form. Information Processing Letters\u00a068(2), 63\u201369 (1998)","journal-title":"Information Processing Letters"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing - SAT 2006"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11814948_37.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,5]],"date-time":"2024-02-05T11:15:30Z","timestamp":1707131730000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11814948_37"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540372066","9783540372073"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/11814948_37","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}