MiniMaxSat
MiniMaxSat: A New Weighted Max-SAT Solver. n this paper we introduce MiniMaxSat, a new Max-SAT solver that incorporates the best SAT and Max-SAT techniques. It can handle hard clauses (clauses of mandatory satisfaction as in SAT), soft clauses (clauses whose falsification is penalized by a cost as in Max-SAT) as well as pseudo-boolean objective functions and constraints. Its main features are: learning and backjumping on hard clauses; resolution-based and subtraction-based lower bounding; and lazy propagation with the two-watched literals scheme. Our empirical evaluation on a wide set of optimization benchmarks indicates that its performance is usually close to the best specialized alternative and, in some cases, even better.
Keywords for this software
References in zbMATH (referenced in 36 articles , 1 standard article )
Showing results 1 to 20 of 36.
Sorted by year (- Berend, Daniel; Twitto, Yochai: Probabilistic characterization of random Max (r)-Sat (2021)
- Cherif, Mohamed Sami; Habet, Djamal; Abramé, André: Understanding the power of Max-SAT resolution through up-resilience (2020)
- Marques-Silva, Joao; Malik, Sharad: Propositional SAT solving (2018)
- Ansótegui, Carlos; Gabàs, Joel: WPM3: an (in)complete algorithm for weighted partial MaxSAT (2017)
- Ansótegui, Carlos; Gabàs, Joel; Levy, Jordi: Exploiting subproblem optimization in SAT-based maxsat algorithms (2016)
- Ansótegui, Carlos; Gabàs, Joel; Malitsky, Yuri; Sellmann, Meinolf: MaxSAT by improved instance-specific algorithm configuration (2016)
- Cai, Shaowei; Luo, Chuan; Lin, Jinkun; Su, Kaile: New local search methods for partial MaxSAT (2016)
- Jamil, Noreen; Müller, Johannes; Naeem, M. Asif; Lutteroth, Christof; Weber, Gerald: Extending linear relaxation for non-square matrices and soft constraints (2016)
- Eberhard, Sebastian; Hetzl, Stefan: Inductive theorem proving based on tree grammars (2015)
- Achá, Roberto Asín; Nieuwenhuis, Robert: Curriculum-based course timetabling with SAT and MaxSAT (2014)
- Allouche, David; André, Isabelle; Barbe, Sophie; Davies, Jessica; de Givry, Simon; Katsirelos, George; O’Sullivan, Barry; Prestwich, Steve; Schiex, Thomas; Traoré, Seydou: Computational protein design as an optimization problem (2014)
- Davies, Jessica; Bacchus, Fahiem: Exploiting the power of MIP solvers in MAXSAT (2013)
- Heras, F.; Baneres, D.: Incomplete inference for graph problems (2013)
- Menai, Mohamed El Bachir; Al-Yahya, Tasniem Nasser: A taxonomy of exact methods for partial Max-SAT (2013)
- Morgado, Antonio; Heras, Federico; Liffiton, Mark; Planes, Jordi; Marques-Silva, Joao: Iterative and core-guided maxsat solving: a survey and assessment (2013)
- Maratea, Marco: Planning as satisfiability with IPC simple preferences and action costs (2012)
- Maratea, Marco; Pulina, Luca: Solving disjunctive temporal problems with preferences using maximum satisfiability (2012)
- Morgado, Antonio; Heras, Federico; Marques-Silva, Joao: Improvements to core-guided binary search for MaxSAT (2012)
- Abío, Ignasi; Deters, Morgan; Nieuwenhuis, Robert; Stuckey, Peter J.: Reducing chaos in SAT-like search: finding solutions close to a given one (2011)
- Arieli, Ofer; Zamansky, Anna: A framework for reasoning under uncertainty based on non-deterministic distance semantics (2011)