Switch to: References

Add citations

You must login to add citations.
  1. A resolution calculus for MinSAT.Chu-Min Li, Fan Xiao & Felip Manyà - 2021 - Logic Journal of the IGPL 29 (1):28-44.
    The logical calculus for SAT are not valid for MaxSAT and MinSAT because they preserve satisfiability but not the number of unsatisfied clauses. To overcome this drawback, a MaxSAT resolution rule preserving the number of unsatisfied clauses was defined in the literature. This rule is complete for MaxSAT when it is applied following a certain strategy. In this paper we first prove that the MaxSAT resolution rule also provides a complete calculus for MinSAT if it is applied following the strategy (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  • Understanding the power of Max-SAT resolution through UP-resilience.Mohamed Sami Cherif, Djamal Habet & André Abramé - 2020 - Artificial Intelligence 289:103397.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  • Propositional proof systems based on maximum satisfiability.Maria Luisa Bonet, Sam Buss, Alexey Ignatiev, Antonio Morgado & Joao Marques-Silva - 2021 - Artificial Intelligence 300 (C):103552.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  • Simplified forms of computerized reasoning with distance semantics.Ofer Arieli & Anna Zamansky - 2011 - Journal of Applied Logic 9 (1):1-22.
  • Clause tableaux for maximum and minimum satisfiability.Josep Argelich, Chu Min Li, Felip Manyà & Joan Ramon Soler - 2021 - Logic Journal of the IGPL 29 (1):7-27.
    The inference systems proposed for solving SAT are unsound for solving MaxSAT and MinSAT, because they preserve satisfiability but not the minimum and maximum number of clauses that can be falsified, respectively. To address this problem, we first define a clause tableau calculus for MaxSAT and prove its soundness and completeness. We then define a clause tableau calculus for MinSAT and also prove its soundness and completeness. Finally, we define a complete clause tableau calculus for solving both MaxSAT and MinSAT, (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  • WPM3: An (in)complete algorithm for weighted partial MaxSAT.Carlos Ansótegui & Joel Gabàs - 2017 - Artificial Intelligence 250 (C):37-57.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  • SAT-based MaxSAT algorithms.Carlos Ansótegui, Maria Luisa Bonet & Jordi Levy - 2013 - Artificial Intelligence 196 (C):77-105.