{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T11:45:27Z","timestamp":1740138327745,"version":"3.37.3"},"reference-count":16,"publisher":"World Scientific Pub Co Pte Ltd","issue":"04","funder":[{"DOI":"10.13039\/501100003549","name":"Orsz\u00c3\u00a1gos Tudom\u00c3\u00a1nyos Kutat\u00c3\u00a1si Alapprogramok","doi-asserted-by":"publisher","award":["140102613"],"award-info":[{"award-number":["140102613"]}],"id":[{"id":"10.13039\/501100003549","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int. J. Artif. Intell. Tools"],"published-print":{"date-parts":[[2017,8]]},"abstract":"<jats:p>When deciding the satisfiability of a Boolean formula, one promising approach is to split the formula into two smaller independent sub-formulas. While many studies report encouraging early results with such methods, the approach is rarely used in state-of-the-art solvers. In this paper, we present a technique that uses formula partitioning to guide the solution of the SAT problem through providing initialization values for the VSIDS heuristic. Our results on a large number of benchmark instances show that the method can notably improve the performance of modern solvers, especially if the time available for solving is short. We also present some findings in the area of hypergraph partitioning, which is used as a tool for our technique.<\/jats:p>","DOI":"10.1142\/s0218213017500117","type":"journal-article","created":{"date-parts":[[2017,2,15]],"date-time":"2017-02-15T01:29:00Z","timestamp":1487122140000},"page":"1750011","source":"Crossref","is-referenced-by-count":2,"title":["Guiding SAT Solving by Formula Partitioning"],"prefix":"10.1142","volume":"26","author":[{"given":"Zolt\u00e1n \u00c1d\u00e1m","family":"Mann","sequence":"first","affiliation":[{"name":"University of Duisburg-Essen, Germany"}]},{"given":"P\u00e1l Andr\u00e1s","family":"Papp","sequence":"additional","affiliation":[{"name":"Swiss Federal Institute of Technology in Zurich, Switzerland"}]}],"member":"219","published-online":{"date-parts":[[2017,8,27]]},"reference":[{"key":"p_1","first-page":"72","volume":"27","author":"Mann Z. A.","year":"2014","journal-title":"EasyChair Proceedings in Computing"},{"key":"p_5","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2004.11.004"},{"key":"p_10","first-page":"41","volume":"27","author":"Mann Z. A.","year":"2014","journal-title":"EasyChair Proceedings in Computing"},{"key":"p_11","doi-asserted-by":"crossref","first-page":"201","DOI":"10.3233\/SAT190022","volume":"2","author":"Biere A.","year":"2006","journal-title":"Boolean Modeling and Computation"},{"key":"p_15","doi-asserted-by":"publisher","DOI":"10.1007\/BF02127976"},{"key":"p_16","doi-asserted-by":"publisher","DOI":"10.1007\/s10601-012-9121-3"},{"key":"p_18","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevE.70.066111"},{"issue":"1","key":"p_23","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1613\/jair.3442","volume":"43","author":"Huang R.","year":"2012","journal-title":"Journal of Artificial Intelligence Research"},{"key":"p_30","doi-asserted-by":"publisher","DOI":"10.1007\/BF01531077"},{"key":"p_38","doi-asserted-by":"publisher","DOI":"10.1109\/92.748202"},{"key":"p_39","doi-asserted-by":"publisher","DOI":"10.2478\/v10006-007-0022-3"},{"key":"p_41","doi-asserted-by":"publisher","DOI":"10.1002\/j.1538-7305.1970.tb01770.x"},{"key":"p_43","doi-asserted-by":"publisher","DOI":"10.1109\/43.573831"},{"key":"p_45","doi-asserted-by":"publisher","DOI":"10.1155\/2000\/19436"},{"key":"p_46","doi-asserted-by":"crossref","first-page":"565","DOI":"10.1613\/jair.2490","author":"Xu L.","year":"2008","journal-title":"Journal of Artificial Intelligence Research ("},{"key":"p_47","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(00)00081-3"}],"container-title":["International Journal on Artificial Intelligence Tools"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S0218213017500117","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,2]],"date-time":"2020-10-02T11:46:14Z","timestamp":1601639174000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/abs\/10.1142\/S0218213017500117"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,8]]},"references-count":16,"journal-issue":{"issue":"04","published-online":{"date-parts":[[2017,8,27]]},"published-print":{"date-parts":[[2017,8]]}},"alternative-id":["10.1142\/S0218213017500117"],"URL":"https:\/\/doi.org\/10.1142\/s0218213017500117","relation":{},"ISSN":["0218-2130","1793-6349"],"issn-type":[{"type":"print","value":"0218-2130"},{"type":"electronic","value":"1793-6349"}],"subject":[],"published":{"date-parts":[[2017,8]]}}}