{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,9]],"date-time":"2026-05-09T06:06:49Z","timestamp":1778306809012,"version":"3.51.4"},"reference-count":52,"publisher":"Springer Science and Business Media LLC","issue":"1-4","license":[{"start":{"date-parts":[[2004,12,31]],"date-time":"2004-12-31T00:00:00Z","timestamp":1104451200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[2005,1]]},"DOI":"10.1007\/s10472-005-0417-5","type":"journal-article","created":{"date-parts":[[2005,3,2]],"date-time":"2005-03-02T19:19:42Z","timestamp":1109791182000},"page":"1-34","source":"Crossref","is-referenced-by-count":7,"title":["On SAT instance classes and a method for reliable performance experiments with SAT solvers"],"prefix":"10.1007","volume":"43","author":[{"given":"Franc","family":"Brglez","sequence":"first","affiliation":[]},{"given":"Xiao Yu","family":"Li","sequence":"additional","affiliation":[]},{"given":"Matthias F.","family":"Stallmann","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2004,12,31]]},"reference":[{"key":"417_CR1","volume-title":"Computer Algorithms","author":"S. Baase","year":"2000","unstructured":"S. Baase and A. Van Gelder, Computer Algorithms, 3rd edition (Addison-Wesley, Reading, MA, 2000).","edition":"3rd edition"},{"key":"417_CR2","unstructured":"G.E.P. Box, W.G. Hunter and J.S. Hunter, Statistics for Experimenters: An Introduction to Design, Data Analysis and Model Building (Wiley, 1978)."},{"key":"417_CR3","unstructured":"F. Brglez, Design of experiments to evaluate CAD algorithms: which improvements are due to improved heuristic and which are merely due to chance?, Technical Report 1998-TR@CBL-04-Brglez, CBL, CS Dept., NCSU, Raleigh, NC (April 1998). Also available at http:\/\/www.cbl.ncsu.edu\/publications\/#1998-TR@CBL-04-Brglez."},{"key":"417_CR4","unstructured":"F. Brglez and R. Drechsler, Design of experiments in CAD: Context and new data sets for ISCAS\u201999, in: Proc. of IEEE 1999 International Symposium on Circuits and Systems \u2014 ISCAS\u201999 (May 1999). A reprint is accessible from http:\/\/www.cbl.ncsu.edu\/publications\/#I999-ISCAS-Brglez."},{"key":"417_CR5","unstructured":"F. Brglez, X.Y. Li and M. Stallmann, The role of a skeptic agent in testing and benchmarking of SAT algorithms, in: Proc. of Fifth International Symposium on the Theory and Applications of Satisfiability Testing, http:\/\/www.cbl.ncsu.edu\/publications\/ (May 2002)."},{"key":"417_CR6","unstructured":"F. Brglez, M.F. Stallmann and X.Y. Li, SATbed \u2014 An environment for reliable performance experiments with SAT instance classes and algorithms, in: Proc. of SAT 2003, Sixth International Symposium on the Theory and Applications of Satisfiability Testing, Portofino, Italy, ed. S.M. Ligure (May 5\u20138, 2003). A revised version available at http:\/\/www.cbl.ncsu.edu\/publications\/."},{"key":"417_CR7","unstructured":"F. Brglez, M. Stallmann and X.Y. Li, SATbed home page: A tutorial, a user guide, a software archive, archives of SAT instance classes and experimental results, http:\/\/www.cbl.ncsu.edu\/OpenExperiments\/SAT\/ (2003)."},{"key":"417_CR8","unstructured":"C. Coarfa, D.D. Demopoulos, A.S.M. Aguirre, D. Subramanian and M.Y. Vardi, Random 3-SAT: The plot thickens, in: Principles and Practice of Constraint Programming (2000) pp. 143\u2013159."},{"key":"417_CR9","doi-asserted-by":"crossref","unstructured":"S. Cook and D. Mitchell, Finding hard instances of the satisfiability problem: A survey, http:\/\/dream.dai.ed.ac.uk\/group\/tw\/sat\/sat-survey3.ps (1997).","DOI":"10.1090\/dimacs\/035\/01"},{"key":"417_CR10","volume-title":"Statistics Manual","author":"E.L. Crow","year":"1960","unstructured":"E.L. Crow, F.A. Davis and M.W. Maxfield, Statistics Manual (Dover, New York, 1960)."},{"issue":"7","key":"417_CR11","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"M. Davis, G. Logemann and D. Loveland, A machine program for theorem-proving, Communications of the ACM 5(7) (1962) 394\u2013397.","journal-title":"Communications of the ACM"},{"issue":"3","key":"417_CR12","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"S. Davis","year":"1960","unstructured":"S. Davis and M. Putnam, A computing procedure for quantification theory, Journal of the Association for Computing Machinery 7(3) (1960) 201\u2013215.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"417_CR13","unstructured":"I.P. Gent and T. Walsh, The search for satisfaction, http:\/\/dream.dai.ed.ac.uk\/group\/tw\/sat\/sat-survey2.ps."},{"key":"417_CR14","volume-title":"Generation of tightly controlled equivalence classes for experimental design of heuristics for graph-based NP-hard problems","author":"D. Ghosh","year":"2000","unstructured":"D. Ghosh, Generation of tightly controlled equivalence classes for experimental design of heuristics for graph-based NP-hard problems, PhD thesis, Electrical and Computer Engineering, North Carolina State University, Raleigh, NC (May 2000). Also available at http:\/\/www.cbl.ncsu.edu\/publications\/#2000-Thesis-PhD-Ghosh."},{"key":"417_CR15","unstructured":"D. Ghosh and F. Brglez, Equivalence classes of circuit mutants for experimental design, in: Proc.of Intl. Symp. Circuits and Systems (ISCAS) (May\u2013June 1999). Also available at http:\/\/www.cbl.ncsu.edu\/publications\/#1999-ISCAS-Ghosh."},{"key":"417_CR16","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1109\/TIT.1959.1057543","volume":"5","author":"S.W. Golomb","year":"1959","unstructured":"S.W. Golomb, On the classification of boolean functions, IRE Transactions on Information Theory 5 (1959) 176\u2013186.","journal-title":"IRE Transactions on Information Theory"},{"key":"417_CR17","doi-asserted-by":"crossref","unstructured":"C.P. Gomes, B. Selman and N. Crato, Heavy-tailed distributions in combinatorial search, in: Principles and Practice of Constraint Programming (1997) pp. 121\u2013135.","DOI":"10.1007\/BFb0017434"},{"key":"417_CR18","doi-asserted-by":"crossref","unstructured":"J. Gu, P. Purdom, J. Franco and B. Wah, Algorithms for the satisfiability (SAT) problem: A survey, in: DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Vol. 35 (1997) pp. 19\u2013152, http:\/\/dream.dai.ed.ac.uk\/group\/tw\/sat\/sat-survey.ps.","DOI":"10.1090\/dimacs\/035\/02"},{"issue":"2\u20133","key":"417_CR19","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1016\/0004-3702(92)90028-V","volume":"56","author":"N.C. Gupta","year":"1992","unstructured":"N.C. Gupta and D.S, Nau, On the complexity of blocks-world planning, Artificial Intelligence 56(2\u20133) (1992) 223\u2013254.","journal-title":"Artificial Intelligence"},{"key":"417_CR20","doi-asserted-by":"crossref","unstructured":"J.E. Harlow and F. Brglez, Design of experiments for evaluation of BDD packages using controlled circuit mutations, in: Proc. of the International Conference on Formal Methods in Computer-Aided Design (FMCAD\u201998), Lecture Notes in Computer Science, Vol. 1522 (Springer, 1998) pp. 64\u201381. Also available from http:\/\/www.cbl.ncsu.edu\/publications\/#1998-FMCAD-Harlow.","DOI":"10.1007\/3-540-49519-3_6"},{"key":"417_CR21","unstructured":"J.E. Harlow and F. Brglez, Design of experiments and evaluation of BDD ordering heuristics, International Journal on Software Tools for Technology Transfer (STTT): Special Issue on BDDs (2001)."},{"key":"417_CR22","unstructured":"E. Hirsch and A. Kojevnikov, UnitWalk: A new SAT solver that uses local search guided by unit clause elimination, 2001, PDMI preprint 9\/2001, Steklov Institute of Mathematics at St. Petersburg (2001)."},{"key":"417_CR23","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/BF02430364","volume":"1","author":"J. Hooker","year":"1996","unstructured":"J. Hooker, Testing heuristics: We have it all wrong, Journal of Heuristics 1 (1996) 33\u201342.","journal-title":"Journal of Heuristics"},{"issue":"2","key":"417_CR24","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1287\/opre.42.2.201","volume":"42","author":"J.N. Hooker","year":"1994","unstructured":"J.N. Hooker, Needed: An empirical science of algorithms, Operations Research 42(2) (1994) 201\u2013212.","journal-title":"Operations Research"},{"key":"417_CR25","unstructured":"H.H. Hoos and T. St\u00fctzle, Evaluating Las Vegas algorithms \u2014 pitfalls and remedies, in: Proc. of UAI-98 (Morgan Kaufmann, San Mateo, CA, 1998) pp. 238\u2013245."},{"key":"417_CR26","doi-asserted-by":"crossref","unstructured":"H.H. Hoos and T. St\u00fctzle, Local search algorithms for SAT: An empirical evaluation, Journal of Automated Reasoning 24 (2000).","DOI":"10.1023\/A:1006350622830"},{"key":"417_CR27","unstructured":"H.H. Hoos and T. St\u00fctzle, SATLIB: An online resource for research on SAT, in: Proc. of SAT\u20192000 (IOS Press, 2000) pp. 283\u2013292, http:\/\/www.satlib.org."},{"key":"417_CR28","volume-title":"Electronic Component Reliability: Fundamentals, Modelling, Evaluation, and Assurance","author":"F. Jense","year":"1996","unstructured":"F. Jense, Electronic Component Reliability: Fundamentals, Modelling, Evaluation, and Assurance (Wiley, New York, 1996)."},{"key":"417_CR29","doi-asserted-by":"crossref","unstructured":"N. Kapur, D. Ghosh and F. Brglez, Towards a new benchmarking paradigm in EDA: analysis of equivalence class mutant circuit distributions, in: Proc. of ACM International Symposium on Physical Design (April 1997).","DOI":"10.1145\/267665.267704"},{"key":"417_CR30","unstructured":"H. Kautz, D. McAllester and B. Selman, Encoding plans in propositional logic, in: KR\u201996: Principles of Knowledge Representation and Reasoning (1996) pp. 374\u2013384. The SATPLAN benchmark set is available from http:\/\/sat.inesc.pt\/benchmarks\/cnf\/satplan\/."},{"key":"417_CR31","doi-asserted-by":"crossref","unstructured":"X.Y. Li, M.F. Stallmann and F. Brglez, QingTing: A local search SAT solver using an effective switching strategy and an efficient unit propagation, in: Proc. of 2003-SAT Issue on Satisfiability Testing, Lecture Notes in Computer Science, Vol. 2919 (2003) pp. 53\u201368. A significant revision of the paper published in Proc. of Sixth International Symposium on the Theory and Applications of Satisfiability Testing, Portofino, Italy, ed. S.M. Ligure (May 5\u20138, 2003). Available at http:\/\/www.cbl.ncsu.edu\/publications\/.","DOI":"10.1007\/978-3-540-24605-3_5"},{"key":"417_CR32","doi-asserted-by":"crossref","first-page":"387","DOI":"10.1080\/01621459.1969.10500983","volume":"64","author":"H. Lilliefors","year":"1969","unstructured":"H. Lilliefors, On the Kolmogorov-Smirnov test for the exponential distribution with mean unknown, Journal of the American Statistical Association 64 (1969) 387\u2013389.","journal-title":"Journal of the American Statistical Association"},{"key":"417_CR33","unstructured":"J.P. Marques-Silva, On selecting problem instances for evaluating satisfiability algorithms, in: Proc. of ECAI Workshop on Empirical Methods in Artificial Intelligence (ECAI-EMAI), 2000."},{"key":"417_CR34","unstructured":"D.A. McAllester, B. Selman and H.A. Kautz, Evidence for invariants in local search, in: Proc. of AAAI\/IAAI (1997) pp. 321\u2013326."},{"key":"417_CR35","unstructured":"D. Mitchell, A remark on benchmarks and analysis, in: Proc. of IJCAI-99 Workshop on Empirical AI (1999)."},{"key":"417_CR36","unstructured":"M. Mitzenmacher, A Brief History of Generative Models for Power Law and Lognormal Distributions (Allerton, 2001)."},{"key":"417_CR37","unstructured":"M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang and S. Malik, Chaff: Engineering an efficient SAT solver, in: IEEE\/ACM Design Automation Conference (DAC) (2001). Version 1.0 of Chaff is available from http:\/\/www.ee.princeton.edu\/chaff\/zchaff\/zchaff.2001.2.17.src.tar.gz."},{"key":"417_CR38","volume-title":"Probability, Models, and Applications","author":"I. Olkin","year":"1960","unstructured":"I. Olkin, L.J. Gleser and C. Derman, Probability, Models, and Applications (Macmillan, New York, 1960)."},{"key":"417_CR39","doi-asserted-by":"crossref","first-page":"1220","DOI":"10.1080\/01621459.2000.10474322","volume":"95","author":"J.A. Osborne","year":"2000","unstructured":"J.A. Osborne and T.A. Severini, Inference for exponential order statistic models based on an integrated likelihood function, Journal of the American Statistical Association 95 (2000) 1220\u20131228.","journal-title":"Journal of the American Statistical Association"},{"key":"417_CR40","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1080\/00949650211423","volume":"72","author":"J.A. Osborne","year":"2002","unstructured":"J.A. Osborne and T.A. Severini, The Lorenz curve for model assessment in exponential order statistic models, Journal of Statistical Computation and Simulation 72 (2002) 87\u201397.","journal-title":"Journal of Statistical Computation and Simulation"},{"key":"417_CR41","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1080\/00401706.1963.10490105","volume":"5","author":"F. Prochan","year":"1963","unstructured":"F. Prochan, Theoretical explanation of observed decreasing failure rate, Technometrics 5 (1963) 375.","journal-title":"Technometrics"},{"key":"417_CR42","unstructured":"Sat-Ex: The experimentation web site around the satisfiability, http:\/\/www.lri.fr\/ ~simon\/satex\/satex.php3."},{"key":"417_CR43","unstructured":"SATLIB \u2014 The Satisfiability Library, http:\/\/www.satlib.org (2003)."},{"key":"417_CR44","unstructured":"SAT Live! Up-to-date links for the SATisfiability problem, http:\/\/www.satlive.org."},{"issue":"1\u20132","key":"417_CR45","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1016\/0004-3702(95)00045-3","volume":"81","author":"B. Selman","year":"1996","unstructured":"B. Selman, D.G. Mitchell and H.J. Levesque, Generating hard satisfiability problems, Artificial Intelligence 81(1\u20132) (1996) 17\u201329.","journal-title":"Artificial Intelligence"},{"key":"417_CR46","doi-asserted-by":"crossref","unstructured":"M. Stallmann, F. Brglez and D. Ghosh, Heuristics and experimental design for bigraph crossing number minimization, in: Proc. of the First Workshop on Algorithm Engineering and Experimentation (ALENEX 99) (January 1999). Also available at http:\/\/www.cbl.ncsu.edu\/publications\/.","DOI":"10.1007\/3-540-48518-X_5"},{"key":"417_CR47","unstructured":"M. Stallmann, F. Brglez and D. Ghosh, Heuristics, experimental subjects and treatment evaluation in bigraph crossing minimization, Journal on Experimental Algorithmics (2001). Also available at http:\/\/www.cbl.ncsu.edu\/publications\/#2001-JEA-Stallmann."},{"key":"417_CR48","unstructured":"M.A. Trick, Second DIMACS challenge test problems, in: DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Vol. 26 (1993) pp. 653\u2013657. The SAT benchmark sets are available at ftp:\/\/dimacs.rutgers.edu\/pub\/challenge\/satisfiability."},{"key":"417_CR49","volume-title":"Introduction to Graph Theory","author":"D.B. West","year":"1996","unstructured":"D.B. West, Introduction to Graph Theory (Prentice-Hall, Englewood Cliffs, NJ, 1996)."},{"key":"417_CR50","unstructured":"J. Whittemore, J. Kim and K. Sakallah, SATIRE: a new incremental satisfiability engine, in: IEEE\/ACMDesign Automation Conference (DAC) (2001). Version 1.0.0 of SATIRE is available from http:\/\/andante.eecs.umich.edu\/satire\/Satire.tgz."},{"key":"417_CR51","doi-asserted-by":"crossref","unstructured":"H. Zhang, SATO: An efficient propositional proven, in: Conference on Automated Deduction (1997) pp. 272\u2013275. Version 3.2 of SATO is available from ftp:\/\/cs.uiowa.edu\/pub\/hzhang\/sato\/sato.tar.gz.","DOI":"10.1007\/3-540-63104-6_28"},{"key":"417_CR52","volume-title":"Implementing the Davis-Putnam Method","author":"H. Zhang","year":"2000","unstructured":"H. Zhang and M.E. Stickel, Implementing the Davis-Putnam Method (Kluwer Academic, Dordrecht, 2000)."}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-005-0417-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10472-005-0417-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-005-0417-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,6]],"date-time":"2020-04-06T02:27:07Z","timestamp":1586140027000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10472-005-0417-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,12,31]]},"references-count":52,"journal-issue":{"issue":"1-4","published-print":{"date-parts":[[2005,1]]}},"alternative-id":["417"],"URL":"https:\/\/doi.org\/10.1007\/s10472-005-0417-5","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,12,31]]}}}