mis_to_gcnf.py

# Copyright 2021 Jannis Harder

# Permission to use, copy, modify, and/or distribute this software for any
# purpose with or without fee is hereby granted.
#
# THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
# WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
# MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
# SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
# WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
# ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR
# IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.

# This script reduces minimal/minimum independent support (MIS) computation for a CNF
# formula to the group-oriented minimal/minimum unsatisfiable subformula problem (GMUS)
# for a different CNF formula.
#
# The overall approach is the same as in [1] or the implementation [2], but a slightly
# different encoding is used.
#
# In [1] the encoding uses one group to encode `x_i = y_i` for each i. To force a
# different solution for x and y, literals b_i are added and the constraints `x_i = y_i
# -> b_i` as well as `-b_0 \/ ... \/ -b_n` are encoded unconditionally as part of the
# remainder.
#
# In [2] essentially the same encoding is used, but the group constraints are encoded as
# part of the remainder as `a_i -> x_i = y_i` and each group is replaced with a single
# unit clause `a_i`.
#
# This script adds variables b_i, p_i, and n_i constrained unconditionally as follows:
#
#   p_i = -x_i /\ y_i
#   n_i = x_i /\ -y_i
#   b_i = -p_i /\ -n_i   [ = (x_i = y_i) ]
#
# The groups are again the unit clauses `b_i`.
#
# The constraint that at least one variable differs between the solution is encoded via
# `n_0 \/ ... \/ n_n`, which breaks some of the symmetry resulting from the two
# identical copies.
#
# I think this encoding might also help via propagations between b_i, n_i and p_i, but I
# have not tried to substantiate this.
#
# In my preliminary manual testing using muser2 [3, 4], this performs much better than
# the encoding used in [2].
#
# [1] A. Ivrii, S. Malik, K. S. Meel, and M. Y. Vardi, “On computing minimal independent
# support and its applications to sampling and counting,” Constraints, vol. 21, no. 1,
# pp. 41–58, Jan. 2016, doi: 10.1007/s10601-015-9204-z.
#
# [2] https://github.com/meelgroup/mis
#
# [3] A. Belov and J. Marques-Silva, “MUSer2: An Efficient MUS Extractor,” SAT, vol. 8,
# no. 3–4, pp. 123–128, Dec. 2012, doi: 10.3233/SAT190094.
#
# [4] https://github.com/meelgroup/muser forked from
# https://bitbucket.org/anton_belov/muser2

import argparse

parser = argparse.ArgumentParser()
parser.add_argument("input", type=argparse.FileType("r"))
parser.add_argument("output", type=argparse.FileType("w"))

args = parser.parse_args()

header = "c"

while header.startswith("c"):
    header = next(args.input)
header = header.split()

if header[0] != "p" or header[1] != "cnf":
    raise ValueError("expected cnf file")

num_vars, num_clauses = map(int, header[2:])

clauses = []

for line in args.input:
    if line.startswith("c"):
        continue
    fields = line.split()
    if not fields:
        continue
    terminator = fields[-1]
    if int(terminator) != 0:
        raise ValueError("syntax error")

    clauses.append(list(map(int, fields[:-1])))

lit_map = [{} for i in range(5)]

for i in range(5):
    for var in range(1, 1 + num_vars):
        target = var + num_vars * i
        lit_map[i][var] = target
        lit_map[i][-var] = -target

eq_map, pos_map, neg_map, copy_x, copy_y = lit_map

out_clauses = []

for copy in (copy_x, copy_y):
    for clause in clauses:
        out_clauses.append([copy[lit] for lit in clause])

for var in range(1, 1 + num_vars):
    out_clauses.append([-pos_map[var], copy_y[var]])
    out_clauses.append([-pos_map[var], -copy_x[var]])
    out_clauses.append([-copy_y[var], copy_x[var], pos_map[var]])

    out_clauses.append([-neg_map[var], -copy_y[var]])
    out_clauses.append([-neg_map[var], copy_x[var]])
    out_clauses.append([copy_y[var], -copy_x[var], neg_map[var]])

    out_clauses.append([eq_map[var], pos_map[var], neg_map[var]])
    out_clauses.append([-pos_map[var], -eq_map[var]])
    out_clauses.append([-neg_map[var], -eq_map[var]])

out_clauses.append([neg_map[var] for var in range(1, 1 + num_vars)])

print("p gcnf", num_vars * 5, len(out_clauses) + num_vars, num_vars, file=args.output)
for clause in out_clauses:
    print("{0}", *clause, 0, file=args.output)
for var in range(1, 1 + num_vars):
    print("{%i}" % var, var, 0, file=args.output)