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.


References in zbMATH (referenced in 25 articles , 1 standard article )

Showing results 1 to 20 of 25.
Sorted by year (citations)

1 2 next

  1. Ansótegui, Carlos; Gabàs, Joel; Malitsky, Yuri; Sellmann, Meinolf: MaxSAT by improved instance-specific algorithm configuration (2016)
  2. Jamil, Noreen; Müller, Johannes; Naeem, M.Asif; Lutteroth, Christof; Weber, Gerald: Extending linear relaxation for non-square matrices and soft constraints (2016)
  3. Eberhard, Sebastian; Hetzl, Stefan: Inductive theorem proving based on tree grammars (2015)
  4. Achá, Roberto Asín; Nieuwenhuis, Robert: Curriculum-based course timetabling with SAT and MaxSAT (2014)
  5. 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)
  6. Davies, Jessica; Bacchus, Fahiem: Exploiting the power of MIP solvers in maxsat (2013)
  7. Heras, F.; Baneres, D.: Incomplete inference for graph problems (2013)
  8. Menai, Mohamed El Bachir; Al-Yahya, Tasniem Nasser: A taxonomy of exact methods for partial Max-SAT (2013)
  9. Morgado, Antonio; Heras, Federico; Liffiton, Mark; Planes, Jordi; Marques-Silva, Joao: Iterative and core-guided maxsat solving: a survey and assessment (2013)
  10. Maratea, Marco: Planning as satisfiability with IPC simple preferences and action costs (2012)
  11. Maratea, Marco; Pulina, Luca: Solving disjunctive temporal problems with preferences using maximum satisfiability (2012)
  12. Morgado, Antonio; Heras, Federico; Marques-Silva, Joao: Improvements to core-guided binary search for MaxSAT (2012)
  13. Abío, Ignasi; Deters, Morgan; Nieuwenhuis, Robert; Stuckey, Peter J.: Reducing chaos in SAT-like search: finding solutions close to a given one (2011)
  14. Arieli, Ofer; Zamansky, Anna: A framework for reasoning under uncertainty based on non-deterministic distance semantics (2011)
  15. Ibaraki, Toshihide; Imamichi, Takashi; Koga, Yuichi; Nagamochi, Hiroshi; Nonobe, Koji; Yagiura, Mutsunori: Efficient branch-and-bound algorithms for weighted MAX-2-SAT (2011)
  16. Marques-Silva, Joao; Argelich, Josep; Graça, Ana; Lynce, In^es: Boolean lexicographic optimization: algorithms & applications (2011)
  17. Mengshoel, Ole J.; Roth, Dan; Wilkins, David C.: Portfolios in stochastic local search: efficiently computing most probable explanations in Bayesian networks (2011)
  18. Nair, Naveen; Govindan, Anandraj; Jayaraman, Chander; Kiran, T.V.S.; Ramakrishnan, Ganesh: Pruning search space for weighted first order Horn clause satisfiability (2011)
  19. Östergård, Patric R.J.; Vaskelainen, Vesa P.: Russian doll search for the Steiner triple covering problem (2011)
  20. Cooper, M.C.; de Givry, S.; Sanchez, M.; Schiex, T.; Zytnicki, M.; Werner, T.: Soft arc consistency revisited (2010)

1 2 next