This PR implements the first version of MaxSAT solver. It supports MaxRes core-based algorithm implemented in z3 solver. Implementation is based on the article.
Current solution is in progress. Cases when solver starts returning UNKNOWN are not fully supported yet. Also algorithm can be optimized: short expressions should not be reified with literals.
Description
This PR implements the first version of MaxSAT solver. It supports MaxRes core-based algorithm implemented in z3 solver. Implementation is based on the article.
Current solution is in progress. Cases when solver starts returning UNKNOWN are not fully supported yet. Also algorithm can be optimized: short expressions should not be reified with literals.