Max-SAT 2010

Fifth Max-SAT Evaluation

Solvers

• akmaxsat : Adrian Kuegel
  

  Branch and bound Maxsat solver with the following features:
  - transformation rules of the WMaxSatz solver
  - ternary resolution (x y z) (x y -z) -> (x y)
  - generalized unit propagation to identify inconsistent subformulas
  - lazy deletion data structure

• akmaxsat_ls : Adrian Kuegel
  

  Branch and bound Maxsat solver with the following features:
  - uses ubcsat to get an initial upper bound
  - transformation rules of the WMaxSatz solver
  - ternary resolution (x y z) (x y -z) -> (x y)
  - generalized unit propagation to identify inconsistent subformulas
  - lazy deletion data structure

• SAT4J MAXSAT 2.2.0 : Daniel Le Berre
  

  Yet another version of SAT4J MAXSAT. Uses Glucose like learned clause deletion strategy and rapid restarts.

• QMaxSAT : Miyuki Koshimura , Tong Zhang
  

  This is a Partial MaxSAT solver based on MiniSat 2.0.
  This uses cardinality constraints from
  O.Balileux and Y.Boufkhad, Efficient CNF encoding of Boolean cardinality constraints.

• IncMaxSatz : Han Lin , Kaile Su, Chu Min Li
  

  IncMaxSatz is based on maxsatz. Besides the powerful lower bound computation methods in maxsatz, IncMaxSatz incorporates a new technique with a nice property that guarantees the increment of lower bounds. At each branch point in the search-tree, the current node is enabled to inherit inconsistencies from its parent and learn information about effectiveness of the lower bound computing procedure from previous nodes. Furthermore, after branching on a new variable, the inconsistencies may shrink by applying unit propagation to them.

• IncWMaxSatz : Han Lin , Kaile Su, Chu Min Li, Josep Argelich
  

  IncWMaxSatz is a weighted version of IncMaxSatz.

• Maxsat_Power : Abdorrahim Bahrami , Seyed Rasoul Mousavi, Maryam Farshchian
  

  Maxsat_Power version 1.0
  

• LS_Power : Abdorrahim Bahrami , Seyed Rasoul Mousavi, Maryam Farshchian
  

  LS_Power version 1.0
  

• WMaxsat_Power : Abdorrahim Bahrami , Seyed Rasoul Mousavi, Maryam Farshchian
  

  WMaxsat_Power version 1.0
  

• LSW_Power : Abdorrahim Bahrami , Seyed Rasoul Mousavi, Maryam Farshchian
  

  LSW_Power version 1.0
  

• wbo 1.4a : Vasco Manquinho , Joao Marques-Silva, Jordi Planes
  

  wbo 1.4a is a solver for MaxSAT and variants based on the iterative identification of unsatisfiable cores, as described in the authors paper at SAT 2009.
  

• wbo 1.4b : Vasco Manquinho , Joao-Marques Silva and Jordi Planes
  

  wbo 1.4b is a variation of wbo 1.4a where proposals from SAT'10 paper are included.