Open-WBO
Open-WBO: a modular MaxSAT solver. This paper presents open-wbo, a new MaxSAT solver. open-wbo has two main features. First, it is an open-source solver that can be easily modified and extended. Most MaxSAT solvers are not available in open-source, making it hard to extend and improve current MaxSAT algorithms. Second, open-wbo may use any MiniSAT-like solver as the underlying SAT solver. As many other MaxSAT solvers, open-wbo relies on successive calls to a SAT solver. Even though new techniques are proposed for SAT solvers every year, for many MaxSAT solvers it is hard to change the underlying SAT solver. With open-wbo, advances in SAT technology will result in a free improvement in the performance of the solver. In addition, the paper uses open-wbo to evaluate the impact of using different SAT solvers in the performance of MaxSAT algorithms.
Keywords for this software
References in zbMATH (referenced in 28 articles )
Showing results 1 to 20 of 28.
Sorted by year (- Bonet, Maria Luisa; Buss, Sam; Ignatiev, Alexey; Morgado, Antonio; Marques-Silva, Joao: Propositional proof systems based on maximum satisfiability (2021)
- Devriendt, Jo; Gleixner, Ambros; Nordström, Jakob: Learn to relax: integrating (0-1) integer linear programming with pseudo-Boolean conflict-driven search (2021)
- Kyrillidis, Anastasios; Shrivastava, Anshumali; Vardi, Moshe Y.; Zhang, Zhiwei: Solving hybrid Boolean constraints in continuous space via multilinear Fourier expansions (2021)
- Lei, Zhendong; Cai, Shaowei; Luo, Chuan; Hoos, Holger: Efficient local search for pseudo Boolean optimization (2021)
- Manthey, Norbert: The \textscMergeSatsolver (2021)
- Py, Matthieu; Cherif, Mohamed Sami; Habet, Djamal: A proof builder for Max-SAT (2021)
- Berg, Jeremias; Bacchus, Fahiem; Poole, Alex: Abstract cores in implicit hitting set MaxSat solving (2020)
- Cai, Shaowei; Lei, Zhendong: Old techniques in new ways: clause weighting, unit propagation and hybridization for maximum satisfiability (2020)
- Cherif, Mohamed Sami; Habet, Djamal; Abramé, André: Understanding the power of Max-SAT resolution through up-resilience (2020)
- Dimitrova, Rayna; Ghasemi, Mahsa; Topcu, Ufuk: Reactive synthesis with maximum realizability of linear temporal logic specifications (2020)
- Le Berre, Daniel; Marquis, Pierre; Wallon, Romain: On weakening strategies for PB solvers (2020)
- Pei, Yan Ru; Manukian, Haik; Di Ventra, Massimiliano: Generating weighted MAX-2-SAT instances with frustrated loops: an RBM case study (2020)
- Demirović, Emir; Musliu, Nysret; Winter, Felix: Modeling and solving staff scheduling with partial weighted maxSAT (2019)
- Beyersdorff, Olaf; Chew, Leroy; Mahajan, Meena; Shukla, Anil: Understanding cutting planes for QBFs (2018)
- Jahren, Eivind; Asín, Achá Roberto: Resizing cardinality constraints for MaxSAT (2018)
- Lang, Jérôme; Mengin, Jérôme; Xia, Lirong: Voting on multi-issue domains with conditionally lexicographic preferences (2018)
- Berg, Jeremias; Järvisalo, Matti: Cost-optimal constrained correlation clustering via weighted partial maximum satisfiability (2017)
- Demirović, Emir; Musliu, Nysret: maxSAT-based large neighborhood search for high school timetabling (2017)
- Hyttinen, Antti; Plis, Sergey; Järvisalo, Matti; Eberhardt, Frederick; Danks, David: A constraint optimization approach to causal discovery from subsampled time series data (2017)
- Ignatiev, Alexey; Morgado, Antonio; Marques-Silva, Joao: On tackling the limits of resolution in SAT solving (2017)