glucose.py

#!/usr/bin/env python3
# -*- coding: utf-8 -*-

"""Emulate glucose command line with python-sat module."""

import argparse
import sys

from pysat.formula import CNF
from pysat.solvers import Glucose4


def main(infile, outfile):
    """Call glucose v4.1 with infile and write output to outfile."""
    with Glucose4(bootstrap_with=CNF(from_file=infile).clauses) as s:
        if s.solve():
            print(" ".join(map(str, s.get_model())), "0", file=outfile)
        else:
            print("UNSAT", file=outfile)


if __name__ == "__main__":
    parser = argparse.ArgumentParser(description=sys.modules[__name__].__doc__)
    parser.add_argument(
        "infile", type=argparse.FileType("r"), help="CNF input file in DIMACS format"
    )
    parser.add_argument(
        "outfile", type=argparse.FileType("w"), help="UNSAT or solution in DIMACS style"
    )
    arguments = parser.parse_args(sys.argv[1:])
    main(arguments.infile.name, arguments.outfile)