ahmaxsat solveur

Description

ahmaxsat is a branch and bound solver for the Max-SAT problem and its variants (Weighted, Partial and Weighted Partial Max-SAT). Its main specifities over other branch and bound Max-SAT solvers are:
    - a new unit propagation scheme which consider all the reasons of the propgations [AH14]
    - a new max-resolution application scheme, aimed at limiting the formula size groth [AH14b]
    - an extensive usage of the max-resolution rules to improve the lower bound quality [AH15e]
    - an extended learning scheme to limit redundancy in the lower bound computation [AH14a]

A complete description of ahmaxsat can be found in [AH15d].

Downloads

Version 1.55 (submited to the Max-SAT Evaluation 2014)
ahmaxsat-1.55 (without preprocessing)
ahmaxsat-ls-1.55 (with a local search preprocessing to compute a first good upper bound value)
Version 1.68 (submited to the Max-SAT Evaluation 2015)
This version is more robust than the previous one, with similar performances on almost all instance classes.
ahmaxsat-1.68 (without preprocessing)
ahmaxsat-ls-1.68 (with a local search preprocessing to compute a first good upper bound value)