Minimum Vertex Cover using RC2 MaxSAT Solver from PySAT

minimum-vertex-cover.py

from pysat.examples.rc2 import RC2
from pysat.formula import WCNF, IDPool

vpool = IDPool(start_from=1)


def cover(v):
    return vpool.id(f'cover@{v}')


def main():
    n, m = map(int, input().split())
    edges = []
    for i in range(m):
        edges.append(tuple(map(int, input().split())))

    wcnf = WCNF()
    for (a, b) in edges:
        wcnf.append([cover(a), cover(b)])

    for v in range(1, n + 1):
        wcnf.append([-cover(v)], weight=1)

    print(f"hard clauses: {wcnf.hard}")
    print(f"soft clauses: {wcnf.soft}")

    with RC2(wcnf, solver="m22") as rc2:
        print("Solving...")
        for model in rc2.enumerate():
            print("=" * 42)
            covering = [model[cover(v) - 1] for v in range(1, n + 1)]
            covering = [x for x in covering if x > 0]
            print(f"Minimum Vertex Cover: {covering}")
            print(f"Cost: {rc2.cost}")


if __name__ == '__main__':
    main()

test1.txt

6 6
1 2
1 3
2 3
2 4
2 5
2 6

test2.txt

10 14
1 2
2 3
3 4
1 5
2 6
2 7
3 6
4 9
5 7
7 8
8 9
6 8
6 9
4 10