A unweighted MaxSAT Solver that uses Minisat2.2 as its backbone.

This solver implements Sequential Encoding to encode cardinality constraints and uses the LUS search algorithm.

• g++ (or any other C++ compiler)
• minisat2.2 (included as a submodule)
• GNU make

• Clone the repository

$ git clone --recurse-submodules https://github.com/sukrutrao/MaxSAT-Solver.git
$ cd MaxSAT-Solver

• Compile the program

$ make

If you use a different compiler, please edit the Makefile accordingly.

The solver accepts input from standard input (STDIN) and sends output to the standard output (STDOUT).

The input is a SAT formula is DIMACS format. A detailed description can be found here.

The first line of the output is a single integer that specifies the number of clauses that could be satisfied. The second line is any assignment that satisfies the maximum number of clauses satisfiable. It consists of space separated boolean variables in ascending order, where the variables have a negative sign if assigned false and no negative sign if assigned true. The last variable is followed by a space and then a 0.

If the input is in a file input.cnf, use

$ ./solver < input.cnf

Let the input be

c 3 variables, 6 clauses
p cnf 3 6
1 2 0
1 -2 0
3 2 0
-3 1 0
1 2 3 0
-1 0

The output is

5
-1 2 -3 0

Here, the 5 clauses in the formula are satisfiable. Variable 2 is assigned true, and variables 1 and 3 are assigned false. This is one possible assignment.

This project is licensed under the MIT License. This project uses Minisat2.2, whose license can be found here.

Sukrut Rao

For any issues, queries, or suggestions, please open an issue.

This project was created as a part of the course CS6403: Constraint Solving at IIT Hyderabad.