Created
March 1, 2021 17:27
-
-
Save jix/f13eb0671d410fb8082ffb0b5ce1b569 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # 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) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment