{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,1]],"date-time":"2026-02-01T18:53:56Z","timestamp":1769972036047,"version":"3.49.0"},"reference-count":17,"publisher":"SAGE Publications","issue":"1","license":[{"start":{"date-parts":[[2020,9,11]],"date-time":"2020-09-11T00:00:00Z","timestamp":1599782400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["SAT"],"abstract":"<jats:p>This paper is a system description of the anytime MaxSAT solver TT-Open-WBO-Inc, which won both of the weighted incomplete tracks of MaxSAT Evaluation 2019. We implemented the recently introduced polarity and variable selection heuristics, TORC and TSB, respectively, in the Open-WBO-Inc-BMO algorithm within the open-source anytime MaxSAT solver Open-WBO-Inc. As a result, the solver is substantially more efficient.<\/jats:p>","DOI":"10.3233\/sat-200126","type":"journal-article","created":{"date-parts":[[2020,9,11]],"date-time":"2020-09-11T13:51:28Z","timestamp":1599832288000},"page":"17-22","source":"Crossref","is-referenced-by-count":8,"title":["Polarity and Variable Selection Heuristics for SAT-Based Anytime MaxSAT"],"prefix":"10.1177","volume":"12","author":[{"given":"Alexander","family":"Nadel","sequence":"first","affiliation":[{"name":"Intel Corporation, P.O. Box 1659, Haifa 31015, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"179","published-online":{"date-parts":[[2020,9,11]]},"reference":[{"key":"10.3233\/SAT-200126_ref1","unstructured":"S.\u00a0Agbaria, D.\u00a0Carmi, O.\u00a0Cohen, D. Korchemny, M. Lifshits and A. Nadel, SAT-based semiformal verification of hardware, in: FMCAD 2010, 2010, pp.\u00a025\u201332."},{"key":"10.3233\/SAT-200126_ref2","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/j.artint.2017.05.003","article-title":"WPM3: An (in)complete algorithm for weighted partial MaxSAT","volume":"250","author":"Ans\u00f3tegui","year":"2017","journal-title":"Artif. Intell."},{"key":"10.3233\/SAT-200126_ref3","unstructured":"J.\u00a0Argelich, I.\u00a0Lynce and J.P.\u00a0Marques Silva, On solving Boolean multilevel optimization problems, in: IJCAI 2009, 2009, pp.\u00a0393\u2013398."},{"issue":"1","key":"10.3233\/SAT-200126_ref4","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1142\/S0218213018400018","article-title":"On the glucose SAT solver","volume":"27","author":"Audemard","year":"2018","journal-title":"International Journal on Artificial Intelligence Tools"},{"key":"10.3233\/SAT-200126_ref5","doi-asserted-by":"crossref","unstructured":"E.\u00a0Demirov\u00edc, G.\u00a0Chu and P.J.\u00a0Stuckey, Solution-based phase saving for CP: A\u00a0value-selection heuristic to simulate local search behavior in complete solvers, in: CP 2018, 2018, pp.\u00a099\u2013108.","DOI":"10.1007\/978-3-319-98334-9_7"},{"key":"10.3233\/SAT-200126_ref6","doi-asserted-by":"crossref","unstructured":"E.\u00a0Demirovic and P.J.\u00a0Stuckey, Techniques inspired by local search for incomplete maxsat and the linear algorithm: Varying resolution and solution-guided search, in: CP 2019, 2019, pp.\u00a0177\u2013194.","DOI":"10.1007\/978-3-030-30048-7_11"},{"issue":"4","key":"10.3233\/SAT-200126_ref7","doi-asserted-by":"publisher","first-page":"395","DOI":"10.3233\/AIC-130575","article-title":"Combining approaches for solving satisfiability problems with qualitative preferences","volume":"26","author":"Di Rosa","year":"2013","journal-title":"AI Comm."},{"key":"10.3233\/SAT-200126_ref8","doi-asserted-by":"crossref","unstructured":"S.\u00a0Joshi, P.\u00a0Kumar, R.\u00a0Martins and S.\u00a0Rao, Approximation strategies for incomplete MaxSAT, in: CP 2018, 2018, pp.\u00a0219\u2013228.","DOI":"10.1007\/978-3-319-98334-9_15"},{"issue":"1","key":"10.3233\/SAT-200126_ref9","first-page":"73","article-title":"Open-wbo-inc: Approximation strategies for incomplete weighted maxsat","volume":"11","author":"Joshi","year":"2019","journal-title":"JSAT"},{"issue":"2\u20133","key":"10.3233\/SAT-200126_ref10","first-page":"59","article-title":"The sat4j library, release\u00a02.2","volume":"7","author":"Le Berre","year":"2010","journal-title":"JSAT"},{"issue":"4","key":"10.3233\/SAT-200126_ref11","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1007\/s10601-013-9146-2","article-title":"Iterative and core-guided MaxSAT solving: A\u00a0survey and assessment","volume":"18","author":"Morgado","year":"2013","journal-title":"Constraints"},{"key":"10.3233\/SAT-200126_ref12","doi-asserted-by":"crossref","unstructured":"M.W.\u00a0Moskewicz, C.F.\u00a0Madigan, Y.\u00a0Zhao, L.\u00a0Zhang and S.M.\u00a0Chaff, Engineering an efficient SAT solver, in: DAC 2001, 2001, pp.\u00a0530\u2013535.","DOI":"10.1145\/378239.379017"},{"key":"10.3233\/SAT-200126_ref13","doi-asserted-by":"crossref","unstructured":"A.\u00a0Nadel, Generating diverse solutions in SAT, in: SAT 2011, 2011, pp.\u00a0287\u2013301.","DOI":"10.1007\/978-3-642-21581-0_23"},{"key":"10.3233\/SAT-200126_ref14","doi-asserted-by":"crossref","unstructured":"A.\u00a0Nadel, Anytime weighted MaxSAT with improved polarity selection and bit-vector optimization, in: FMCAD 2019, 2019, pp.\u00a0193\u2013202.","DOI":"10.23919\/FMCAD.2019.8894273"},{"key":"10.3233\/SAT-200126_ref15","doi-asserted-by":"crossref","unstructured":"A.\u00a0Nadel and V.\u00a0Ryvchin, Bit-vector optimization, in: TACAS 2016, 2016, pp.\u00a0851\u2013867.","DOI":"10.1007\/978-3-662-49674-9_53"},{"key":"10.3233\/SAT-200126_ref16","doi-asserted-by":"crossref","unstructured":"K.\u00a0Pipatsrisawat and A.\u00a0Darwiche, A\u00a0lightweight component caching scheme for satisfiability solvers, in: SAT 2007, 2007, pp.\u00a0294\u2013299.","DOI":"10.1007\/978-3-540-72788-0_28"},{"key":"10.3233\/SAT-200126_ref18","doi-asserted-by":"crossref","unstructured":"X.\u00a0Si, X.\u00a0Zhang, R.\u00a0Grigore and M.\u00a0Naik, Maximum satisfiability in software analysis: Applications and techniques, in: CAV 2017, Part\u00a0I, 2017, pp.\u00a068\u201394.","DOI":"10.1007\/978-3-319-63387-9_4"}],"container-title":["Journal on Satisfiability, Boolean Modeling and Computation"],"original-title":[],"link":[{"URL":"https:\/\/content.iospress.com\/download?id=10.3233\/SAT-200126","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T07:08:26Z","timestamp":1761548906000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/full\/10.3233\/SAT-200126"}},"subtitle":["System Description"],"short-title":[],"issued":{"date-parts":[[2020,9,11]]},"references-count":17,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2020,9,11]]}},"URL":"https:\/\/doi.org\/10.3233\/sat-200126","relation":{},"ISSN":["1574-0617"],"issn-type":[{"value":"1574-0617","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,9,11]]}}}