Differences

This shows you the differences between two versions of the page.

Link to this comparison view

msuncore [2016/06/23 12:32] (current)
ajrm created
Line 1: Line 1:
 +====== MSUnCore - Maximum Satisfiability with UNsatisfiable COREs ====== ​
  
 +
 +==== Description ====
 +
 +MSUnCore is a software system for solving (Weighted) (Partial) Maximum Satisfiability (MaxSAT), and implements a number of different algorithms. Most of the MaxSAT algorithms implemented in MSUnCore are based on iterative identification of unsatisfiable cores.
 +\\
 +
 +
 +==== Distribution ====
 +
 +MSUnCore is publicly available as an executable for the following platforms: ​
 +  * {{http://​logos.ucd.ie/​web/​lib/​exe/​fetch.php?​media=tools:​msuncore-20130422-linux64.tgz|Linux 64 Bits}}
 +  * {{http://​logos.ucd.ie/​web/​lib/​exe/​fetch.php?​media=tools:​msuncore-20130422-mountainlion.tgz|Mountain Lion}} ​
 +
 +==== Documentation ====
 +
 +{{http://​logos.ucd.ie/​web/​lib/​exe/​fetch.php?​media=docs:​readme-msuncore.txt|README}} file for MSUnCore.
 +
 +
 +Recent publications describing the algorithms implemented in MSUnCore include:
 +  *  A. Morgado, F. Heras, J. Marques-Silva:​ Improvements to Core-Guided Binary Search for MaxSAT. SAT 2012
 +  * Federico Heras, Antonio Morgado, Joao Marques-Silva:​ Core-guided Binary Search Algorithms for Maximum Satisfiability. AAAI 2011 
 +  * Joao Marques-Silva,​ Josep Argelich, Ana Graca, Inês Lynce: [[http://​dx.doi.org/​10.1007/​s10472-011-9233-2|Boolean Lexicographic Optimization:​ Algorithms and Applications]]. Annals of Mathematics and Artificial Intelligence,​ 2011
 +  * Vasco Manquinho, Joao Marques-Silva,​ Jordi Planes: [[http://​dx.doi.org/​10.1007/​978-3-642-02777-2_45|Algorithms for Weighted Boolean Optimization]]. SAT 2009: 495-508 ​
 +  * Vasco Manquinho, Joao Marques-Silva,​ Jordi Planes: [[http://​arxiv.org/​abs/​0904.0019|Algorithms for Weighted Boolean Optimization]] CoRR abs/​0903.0843:​ (2009) ​
 +  * Josep Argelich, Inês Lynce, Joao Marques-Silva:​ [[http://​ijcai.org/​papers09/​Papers/​IJCAI09-073.pdf|On Solving Boolean Multilevel Optimization Problems]]. IJCAI 2009: 393-398
 +  * Joao Marques-Silva,​ Vasco Manquinho: [[http://​dx.doi.org/​10.1007/​978-3-540-79719-7_21|Towards More Effective Unsatisfiability-Based Maximum Satisfiability Algorithms]]. SAT 2008: 225-230 ​
 +  * Joao Marques-Silva,​ Jordi Planes: [[http://​dx.doi.org/​10.1109/​DATE.2008.4484715|Algorithms for Maximum Satisfiability using Unsatisfiable Cores]]. DATE 2008: 408-413
 +  * Joao Marques-Silva,​ Jordi Planes: [[http://​arxiv.org/​abs/​0712.1097|On Using Unsatisfiability for Solving Maximum Satisfiability]]. CoRR abs/​0712.0097 (December 2007)
 +
 +
 +
 +Recent presentations related to MSUnCore:
 +  *Antonio Morgado, Federico Heras, Joao Marques-Silva:​ {{http://​logos.ucd.ie/​web/​lib/​exe/​fetch.php?​media=docs:​msuncore-pos11.pdf|The MSUnCore system for MaxSAT solving.}} Pragmatics of SAT (POS11) workshop.
 +
 +
 +
 +==== Benchmarks ====
 +
 +  * Weighted/​Unweighted (Partial) MaxSAT instances can be obtained from [[http://​www.maxsat.udl.cat/​ | MaxSAT Evaluations]]. ​
 +  * MSUncore accepts both the CNF and WCNF formats (for details on the formats see this [[http://​maxsat.ia.udl.cat/​requirements/​|page]]).
 +
 +
 +==== Contributors ====
 +
 +  * [[Joao.Marques-Silva | Joao Marques-Silva]](Principal Investigator)
 +  * [[Antonio.Morgado | António Morgado]]
 +  * [[http://​logos.ucd.ie/​web/​doku.php?​id=federico.heras|Federico Heras]]
 +  * [[http://​web.udl.es/​usuaris/​m4372594/​|Jordi Planes]]
 +  * [[http://​sat.inesc.pt/​~vmm/​|Vasco Manquinho]]
 +
 +
 +==== Funding ====
 +The developement of MSUnCore was partially supported by:
 +
 +[[http://​cordis.europa.eu/​fp7/​home_en.html | European Commission FP7]] and [[http://​www.sfi.ie/​ | Science Foundation Ireland]]
 +
 +{{:​images:​fp7.png?​nolink&​200|}} {{:​images:​sfi.jpeg?​nolink&​200|}}
 +
 +
 +==== Wiki Status ====
 +**Replicated [[http://​logos.ucd.ie/​web/​doku.php?​id=msuncore|Page]]**
Print/export