{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T09:34:32Z","timestamp":1777455272279,"version":"3.51.4"},"reference-count":48,"publisher":"Springer Science and Business Media LLC","issue":"7","license":[{"start":{"date-parts":[[2021,6,16]],"date-time":"2021-06-16T00:00:00Z","timestamp":1623801600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,6,16]],"date-time":"2021-06-16T00:00:00Z","timestamp":1623801600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100000923","name":"Australian Research Council","doi-asserted-by":"crossref","award":["DP150101618"],"award-info":[{"award-number":["DP150101618"]}],"id":[{"id":"10.13039\/501100000923","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Artif Intell Rev"],"published-print":{"date-parts":[[2021,10]]},"DOI":"10.1007\/s10462-021-10024-0","type":"journal-article","created":{"date-parts":[[2021,6,16]],"date-time":"2021-06-16T13:03:22Z","timestamp":1623848602000},"page":"5347-5411","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Evaluating logic gate constraints in local search for structured satisfiability problems"],"prefix":"10.1007","volume":"54","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5655-0683","authenticated-orcid":false,"given":"M. A. H.","family":"Newton","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M. M. A.","family":"Polash","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"D. N.","family":"Pham","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J.","family":"Thornton","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"K.","family":"Su","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A.","family":"Sattar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,6,16]]},"reference":[{"key":"10024_CR1","doi-asserted-by":"crossref","unstructured":"Balint A, Fr\u00f6hlich A (2010) Improving stochastic local search for sat with a new probability distribution. In: International conference on theory and applications of satisfiability testing. Springer, pp 10\u201315","DOI":"10.1007\/978-3-642-14186-7_3"},{"key":"10024_CR2","doi-asserted-by":"crossref","unstructured":"Balyo T, Fr\u00f6hlich A, Heule MJ, Biere A (2014) Everything you always wanted to know about blocked sets (but were afraid to ask). In: International conference on theory and applications of satisfiability testing. Springer, pp 317\u2013332","DOI":"10.1007\/978-3-319-09284-3_24"},{"key":"10024_CR3","volume-title":"Proceedings of SAT competition 2020: solver and benchmark descriptions","year":"2020","unstructured":"Balyo T, Froleyks N, Heule MJ, Iser M, J\u00e4rvisalo M, Suda M (eds) (2020) Proceedings of SAT competition 2020: solver and benchmark descriptions. University of Helsinki, Department of Computer Science, Helsinki"},{"issue":"2","key":"10024_CR4","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1287\/ijoc.6.2.126","volume":"6","author":"R Battiti","year":"1994","unstructured":"Battiti R, Tecchiolli G (1994) The reactive tabu search. ORSA J Comput 6(2):126\u2013140","journal-title":"ORSA J Comput"},{"key":"10024_CR5","first-page":"258","volume":"9","author":"A Belov","year":"2009","unstructured":"Belov A, Stachniak Z (2009) Improving variable selection process in stochastic local search for propositional satisfiability. SAT 9:258\u2013264","journal-title":"SAT"},{"key":"10024_CR6","first-page":"293","volume":"6175","author":"A Belov","year":"2010","unstructured":"Belov A, Stachniak Z (2010) Improved local search for circuit satisfiability. SAT 6175:293\u2013299","journal-title":"SAT"},{"key":"10024_CR7","unstructured":"Belov A, J\u00e4rvisalo M, Stachniak Z (2011) Depth-driven circuit-level stochastic local search for SAT. In: IJCAI, pp 504\u2013509"},{"key":"10024_CR8","unstructured":"Biere A (2016) Splatz, lingeling, plingeling, treengeling, yalsat entering the sat competition 2016. In: Proceedings of of SAT competition, pp 44\u201345"},{"key":"10024_CR9","unstructured":"Biere A, Fazekas K, Fleury M, Heisinger M (2020) CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020. In: Balyo T, Froleyks N, Heule M, Iser M, J\u00e4rvisalo M, Suda M (eds) Proceedings of SAT competition 2020\u2014solver and benchmark descriptions. University of Helsinki, Department of Computer Science Report Series B, vol B-2020-1, pp 51\u201353"},{"key":"10024_CR10","doi-asserted-by":"crossref","unstructured":"Cai S, Luo C, Su K (2015) CCAnr: a configuration checking based local search solver for non-random satisfiability. In: Heule M, Weaver S (Eds) Proceedings of SAT, LNCS, vol 9340, pp 1\u20138","DOI":"10.1007\/978-3-319-24318-4_1"},{"key":"10024_CR11","doi-asserted-by":"crossref","unstructured":"Cook SA (1971) The complexity of theorem-proving procedures. In: Proceedings of the third annual ACM symposium on theory of computing. ACM, pp 151\u2013158","DOI":"10.1145\/800157.805047"},{"issue":"7","key":"10024_CR12","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M Davis","year":"1962","unstructured":"Davis M, Logemann G, Loveland D (1962) A machine program for theorem-proving. Commun ACM 5(7):394\u2013397. https:\/\/doi.org\/10.1145\/368273.368557","journal-title":"Commun ACM"},{"key":"10024_CR13","doi-asserted-by":"crossref","unstructured":"Fu Z, Malik S (2007) Extracting logic circuit structure from conjunctive normal form descriptions. In: 20th international conference on VLSI design, 2007. Held jointly with 6th international conference on embedded systems. IEEE, pp 37\u201342","DOI":"10.1109\/VLSID.2007.81"},{"key":"10024_CR14","first-page":"1","volume":"51","author":"H Fu","year":"2020","unstructured":"Fu H, Wu G, Liu J, Xu Y (2020) More efficient stochastic local search for satisfiability. Appl Intell 51:1\u201320","journal-title":"Appl Intell"},{"key":"10024_CR15","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1016\/j.ins.2021.03.009","volume":"566","author":"H Fu","year":"2021","unstructured":"Fu H, Xu Y, Wu G, Liu J, Chen S, He X (2021) Emphasis on the flipping variable: towards effective local search for hard random satisfiability. Inf Sci 566:118\u2013139","journal-title":"Inf Sci"},{"key":"10024_CR16","volume-title":"Proceedings of sat competition 2018: solver and benchmark descriptions","year":"2018","unstructured":"Heule MJ, J\u00e4rvisalo MJ, Suda M et al (eds) (2018) Proceedings of sat competition 2018: solver and benchmark descriptions. University of Helsinki, Department of Computer Science, Helsinki"},{"key":"10024_CR17","unstructured":"Hoos HH (2002) An adaptive noise mechanism for walksat. In: AAAI\/IAAI, pp 655\u2013660"},{"issue":"4","key":"10024_CR18","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1023\/A:1006350622830","volume":"24","author":"HH Hoos","year":"2000","unstructured":"Hoos HH, St\u00fctzle T (2000) Local search algorithms for SAT: an empirical evaluation. J Autom Reason 24(4):421\u2013481","journal-title":"J Autom Reason"},{"key":"10024_CR19","unstructured":"Hoos HH, Tompkins DA (2007) Adaptive novelty+. SAT competition"},{"key":"10024_CR20","unstructured":"Hoos HH et al (2002) An adaptive noise mechanism for WalkSAT. In: AAAI\/IAAI, pp 655\u2013660"},{"key":"10024_CR21","doi-asserted-by":"crossref","unstructured":"Iser M, Manthey N, Sinz C (2015) Recognition of nested gates in CNF formulas. In: International conference on theory and applications of satisfiability testing. Springer, pp 255\u2013271","DOI":"10.1007\/978-3-319-24318-4_19"},{"issue":"1\u20133","key":"10024_CR22","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1016\/j.jalgor.2008.02.005","volume":"63","author":"M J\u00e4rvisalo","year":"2008","unstructured":"J\u00e4rvisalo M, Niemel\u00e4 I (2008) The effect of structural branching on the efficiency of clause learning sat solving: an experimental study. J Algorithms 63(1\u20133):90\u2013113","journal-title":"J Algorithms"},{"issue":"3","key":"10024_CR23","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/s10601-008-9062-z","volume":"14","author":"M J\u00e4rvisalo","year":"2009","unstructured":"J\u00e4rvisalo M, Junttila T (2009) Limitations of restricted branching in clause learning. Constraints 14(3):325\u2013356","journal-title":"Constraints"},{"key":"10024_CR24","doi-asserted-by":"crossref","unstructured":"J\u00e4rvisalo M, Junttila TA, Niemel\u00e4 I (2008a) Justification-based local search with adaptive noise strategies. In: LPAR. Springer, pp 31\u201346","DOI":"10.1007\/978-3-540-89439-1_3"},{"key":"10024_CR25","unstructured":"J\u00e4rvisalo M, Junttila TA, Niemel\u00e4 I (2008b) Justification-based non-clausal local search for SAT. In: ECAI, pp 535\u2013539"},{"issue":"4","key":"10024_CR26","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1007\/s10817-011-9239-9","volume":"49","author":"M J\u00e4rvisalo","year":"2012","unstructured":"J\u00e4rvisalo M, Biere A, Heule MJ (2012) Simulating circuit-level simplifications on CNF. J Autom Reason 49(4):583\u2013619","journal-title":"J Autom Reason"},{"issue":"1","key":"10024_CR27","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BF01531077","volume":"1","author":"RG Jeroslow","year":"1990","unstructured":"Jeroslow RG, Wang J (1990) Solving propositional satisfiability problems. Ann Math Artif Intell 1(1):167\u2013187. https:\/\/doi.org\/10.1007\/BF01531077","journal-title":"Ann Math Artif Intell"},{"issue":"12","key":"10024_CR28","doi-asserted-by":"publisher","first-page":"1377","DOI":"10.1109\/TCAD.2002.804386","volume":"21","author":"A Kuehlmann","year":"2002","unstructured":"Kuehlmann A, Paruthi V, Krohm F, Ganai MK (2002) Robust Boolean reasoning for equivalence checking and functional property verification. IEEE Trans Comput Aided Des Integr Circuits Syst 21(12):1377\u20131394","journal-title":"IEEE Trans Comput Aided Des Integr Circuits Syst"},{"key":"10024_CR29","doi-asserted-by":"crossref","unstructured":"Luo C, Hoos H, Cai S (2020) Pbo-ccsat: boosting local search for satisfiability using programming by optimisation. In: International conference on parallel problem solving from nature. Springer, pp 373\u2013389","DOI":"10.1007\/978-3-030-58112-1_26"},{"key":"10024_CR30","first-page":"436","volume":"7317","author":"N Manthey","year":"2012","unstructured":"Manthey N (2012) Coprocessor 2.0-a flexible CNF simplifier-(tool presentation). SAT 7317:436\u2013441","journal-title":"SAT"},{"key":"10024_CR31","unstructured":"Manthey N, Stephan A, Werner E (2016) Riss 6 solver and derivatives. In: Proceedings of SAT competition, pp 56\u201357"},{"key":"10024_CR32","unstructured":"Mazure B, Sais L, Gr\u00e9goire \u00c9 (1997) Tabu search for SAT. In: AAAI\/IAAI, pp 281\u2013285"},{"key":"10024_CR33","unstructured":"McAllester D, Selman B, Kautz H (1997) Evidence for invariants in local search. In: AAAI\/IAAI. Rhode Island, USA, pp 321\u2013326"},{"key":"10024_CR34","doi-asserted-by":"crossref","unstructured":"Newton M, Pham D, Sattar A, Maher M (2011) Kangaroo: An efficient constraint-based local search system using lazy propagation. In: CP LNCS, vol 6876. Springer, Heidelberg, pp 645\u2013659","DOI":"10.1007\/978-3-642-23786-7_49"},{"key":"10024_CR35","doi-asserted-by":"crossref","unstructured":"Ostrowski R, Gr\u00e9goire \u00c9, Mazure B, Sais L (2002) Recovering and exploiting structural knowledge from CNF formulas. In: International conference on principles and practice of constraint programming. Springer, pp 185\u2013199","DOI":"10.1007\/3-540-46135-3_13"},{"key":"10024_CR36","doi-asserted-by":"publisher","first-page":"360","DOI":"10.1016\/S1571-0653(04)00333-6","volume":"9","author":"DJ Patterson","year":"2001","unstructured":"Patterson DJ, Kautz H (2001) Auto-WalkSAT: a self-tuning implementation of WalkSAT. Electron Notes Discrete Math 9:360\u2013368","journal-title":"Electron Notes Discrete Math"},{"issue":"4","key":"10024_CR37","doi-asserted-by":"publisher","first-page":"e0231702","DOI":"10.1371\/journal.pone.0231702","volume":"15","author":"C Peng","year":"2020","unstructured":"Peng C, Xu Z, Mei M (2020) Applying aspiration in local search for satisfiability. PloS one 15(4):e0231702","journal-title":"PloS one"},{"key":"10024_CR38","first-page":"2359","volume":"7","author":"DN Pham","year":"2007","unstructured":"Pham DN, Thornton J, Sattar A (2007) Building structure into local search for SAT. IJCAI 7:2359\u20132364","journal-title":"IJCAI"},{"issue":"3","key":"10024_CR39","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"DA Plaisted","year":"1986","unstructured":"Plaisted DA, Greenbaum S (1986) A structure-preserving clause form translation. J Symb Comput 2(3):293\u2013304","journal-title":"J Symb Comput"},{"issue":"6","key":"10024_CR40","doi-asserted-by":"publisher","first-page":"501","DOI":"10.1007\/s10732-017-9353-x","volume":"23","author":"MA Polash","year":"2017","unstructured":"Polash MA, Newton MH, Sattar A (2017) Constraint-based search for optimal Golomb rulers. J Heuristics 23(6):501\u2013532","journal-title":"J Heuristics"},{"key":"10024_CR41","unstructured":"Prestwich S (2002) Supersymmetric modeling for local search. In: Second international workshop on symmetry in constraint satisfaction problems, Citeseer"},{"key":"10024_CR42","doi-asserted-by":"crossref","unstructured":"Prestwich S, Roli A (2005) Symmetry breaking and local search spaces. In: International conference on integration of artificial intelligence (AI) and operations research (OR) techniques in constraint programming. Springer, pp 273\u2013287","DOI":"10.1007\/11493853_21"},{"key":"10024_CR43","first-page":"48109","volume":"1001","author":"JA Roy","year":"2004","unstructured":"Roy JA, Markov IL, Bertacco V (2004) Restoring circuit structure from SAT instances. Ann Arbor 1001:48109\u20132122","journal-title":"Ann Arbor"},{"key":"10024_CR44","doi-asserted-by":"crossref","unstructured":"Ryvchin V, Nadel A (2018) Maple lcm dist chronobt: featuring chronological backtracking. In: Proceedings of SAT competition 2018","DOI":"10.1007\/978-3-319-94144-8_7"},{"key":"10024_CR45","first-page":"3","volume":"4","author":"V Ryvchin","year":"2008","unstructured":"Ryvchin V, Strichman O (2008) Local restarts in sat. Constraint Program Lett (CPL) 4:3\u201313","journal-title":"Constraint Program Lett (CPL)"},{"key":"10024_CR46","unstructured":"Seltner H (2014) Extracting hardware circuits from CNF formulas. Master\u2019s thesis, Institute for Formal Models and Verification"},{"key":"10024_CR47","unstructured":"Soos M, Devriendt J, Gocht S, Shaw A, Meel KS (2020) Cryptominisat with ccanr at the sat competition 2020. In: SAT COMPETITION 2020, p 27"},{"key":"10024_CR48","doi-asserted-by":"crossref","unstructured":"Tseitin GS (1983) On the complexity of derivation in propositional calculus. In: Automation of reasoning. Springer, pp 466\u2013483","DOI":"10.1007\/978-3-642-81955-1_28"}],"container-title":["Artificial Intelligence Review"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10462-021-10024-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10462-021-10024-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10462-021-10024-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,9,5]],"date-time":"2021-09-05T07:20:02Z","timestamp":1630826402000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10462-021-10024-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,6,16]]},"references-count":48,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2021,10]]}},"alternative-id":["10024"],"URL":"https:\/\/doi.org\/10.1007\/s10462-021-10024-0","relation":{},"ISSN":["0269-2821","1573-7462"],"issn-type":[{"value":"0269-2821","type":"print"},{"value":"1573-7462","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,6,16]]},"assertion":[{"value":"16 June 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}