Enforcing Structure in the Gadget
GadgetoCompiler allows defining some structure requirements for the generated gadget through the AtMostStructureConstraint and AtLeastStructureConstraint:
These can be specified in the generate method of any of the supported Gadget Compilers through the out_structure_constrs parameter.
In the following, we show some examples on the usage of this feature of GadgetoCompiler.
In all the examples we are generating gadgets from kSAT to Max2SAT using the GurobiGadgetoCompiler compiler.
Example: Enforcing Unit Clauses¶
First, we present an example where we enforce that all the literals of the input constraint must appear in the gadget as unit clauses.
This can be easily achieved in GadgetoCompiler using the AtLeastStructureConstraint, as shown in this full example:
import argparse
from gadgetocompiler.compilers.gurobi import GurobiGadgetoCompiler
from gadgetocompiler.compilers import AtLeastStructureConstraint
from gadgetocompiler.constraints import Clause
def parse_args():
parser = argparse.ArgumentParser()
parser.add_argument("--input-clause-size", "-k", type=int, required=True)
parser.add_argument("--max-auxs", "-b", type=int, required=True)
parser.add_argument("--alpha_ub", "-ub", type=float, required=True)
return parser.parse_args()
def main(args):
input_constr = Clause([i + 1 for i in range(args.input_clause_size)])
out_constr_family = [(Clause, 2), (Clause, 1)]
structure_constrs = [
AtLeastStructureConstraint(
tuple([Clause([lit]) for lit in input_constr.relation]),
k=args.input_clause_size,
)
]
g = GurobiGadgetoCompiler.generate(
input_constr,
out_constr_family,
structure_constrs,
max_auxs=args.max_auxs,
alpha_ub=args.alpha_ub,
decimal_precision=1,
)
if g:
g.show()
is_gadget, is_strict = g.show_assignment_values()
alpha, beta = g.bounds[1], g.beta
print(f"This is {'' if is_gadget else 'NOT '}a ({alpha}-{beta})-gadget")
print("Is strict?", is_strict)
if __name__ == "__main__":
args = parse_args()
main(args)
Warning
The constraints passed to AtLeastStructureConstraint and AtMostStructureConstraint must be in a tuple, as shown in the example.
Example: Gadget Refinement¶
In this example, we disallow inconsistent subsets of output constraints in the gadget that can be simplified using the MaxSAT resolution rule. For more information about this, you can check this resource 1.
We set an AtMostStructureConstraint for each of these subsets, specifying that for a given subset of size \(n\), at most \(n-1\) constraints can be present (i.e., at least one must be outside the gadget).
The full example code is shown below:
import argparse
from gadgetocompiler.compilers.gurobi import GurobiGadgetoCompiler
from gadgetocompiler.compilers import AtMostStructureConstraint
from gadgetocompiler.constraints import Clause
def parse_args():
parser = argparse.ArgumentParser()
parser.add_argument("--input-clause-size", "-k", type=int, required=True)
parser.add_argument("--max-auxs", "-b", type=int, required=True)
parser.add_argument("--alpha_ub", "-ub", type=float, required=True)
return parser.parse_args()
def main(args):
input_constr = Clause([i + 1 for i in range(args.input_clause_size)])
out_constr_family = [(Clause, 2), (Clause, 1)]
structure_constrs = generate_structure_constrs(
k=args.input_clause_size, b=args.max_auxs
)
g = GurobiGadgetoCompiler.generate(
input_constr,
out_constr_family,
structure_constrs,
max_auxs=args.max_auxs,
alpha_ub=args.alpha_ub,
)
if g:
g.show()
is_gadget, is_strict = g.show_assignment_values()
alpha, beta = g.bounds[1], g.beta
print(f"This is {'' if is_gadget else 'NOT '}a ({alpha}-{beta})-gadget")
print("Is strict?", is_strict)
def generate_structure_constrs(k, b):
all_xvars = list(range(1, k + b + 1))
structure_constrs = set()
for x1 in all_xvars:
# (x1), (~x1)
structure_constrs.add(
AtMostStructureConstraint(tuple([Clause([lit]) for lit in (x1, -x1)]), 1)
)
for x2 in all_xvars:
if x1 == x2:
continue
for pol1 in (1, -1):
for pol2 in (1, -1):
# (x1 v x2), (~x1 v x2)
structure_constrs.add(
AtMostStructureConstraint(
(
Clause([x1 * pol1, x2 * pol2]),
Clause([x1 * -pol1, x2 * pol2]),
),
1,
)
)
# (x1), (x2), (~x1 v ~x2)
structure_constrs.add(
AtMostStructureConstraint(
(
Clause([x1 * pol1]),
Clause([x2 * pol2]),
Clause([x1 * -pol1, x2 * -pol2]),
),
2,
)
)
# (x1), (x2), (~x1 v x2)
structure_constrs.add(
AtMostStructureConstraint(
(
Clause([x1 * pol1]),
Clause([x2 * pol2]),
Clause([x1 * -pol1, x2 * pol2]),
),
2,
)
)
# (x1), (~x1 v x2), (x1 v ~x2)
structure_constrs.add(
AtMostStructureConstraint(
(
Clause([x1 * pol1]),
Clause([x1 * -pol1, x2 * pol2]),
Clause([x1 * pol1, x2 * -pol2]),
),
2,
)
)
# (x1), (x1 v x2), (~x1 v ~x2)
structure_constrs.add(
AtMostStructureConstraint(
(
Clause([x1 * pol1]),
Clause([x1 * pol1, x2 * pol2]),
Clause([x1 * -pol1, x2 * -pol2]),
),
2,
)
)
print(f"Computed {len(structure_constrs)} structure constraints")
return structure_constrs
if __name__ == "__main__":
args = parse_args()
main(args)
Example: Incremental Gadgets¶
In this example, we build a gadget incrementally. The idea is to start building a gadget that has a small arity \(k\) (in our case 3), and build subsequent gadgets enforcing that at least a given percentage of the gadget clauses for a gadget with arity \(k\) must be present in the gadget for arity \(k+1\). Additionally, we can enforce that the output constraint that did not appear in the gadget for arity \(k\) must not appear in the gadget for arity \(k+1\).
We can easily enforce these constraints using the AtMostStructureConstaint and the AtLeastStructureConstraint, as we show in the following full example:
import argparse
from typing import List, Tuple, Union, Optional, Sequence
from gadgetocompiler.gadgets import WeightedConstraint
from gadgetocompiler.compilers.gurobi import GurobiGadgetoCompiler
from gadgetocompiler.compilers import (
AtMostStructureConstraint,
AtLeastStructureConstraint,
)
from gadgetocompiler.constraints import Clause, Constraint
def parse_args():
parser = argparse.ArgumentParser()
parser.add_argument("--included-pctg", type=float, default=0.9)
parser.add_argument("--excluded-pctg", type=float, default=1.0)
return parser.parse_args()
def main():
args = parse_args()
start_input_clause_size = 3
start_max_auxs = 1
num_iterations = 7
first_aux_var = start_input_clause_size + num_iterations + 1
included_clauses, excluded_clauses = None, None
for i in range(num_iterations):
input_clause_size = start_input_clause_size + i
max_auxs = start_max_auxs + i
alpha_ub = 2.5 * (input_clause_size - 2) + 1
print(f"----- k={input_clause_size},#b={max_auxs},alpha_ub={alpha_ub} -----")
g, included_clauses_g, excluded_clauses_g = model_and_solve(
input_clause_size,
max_auxs,
alpha_ub,
args.included_pctg,
args.excluded_pctg,
included_clauses,
excluded_clauses,
first_aux_var=first_aux_var,
)
if g is None:
break
g.show()
is_gadget, is_strict = g.show_assignment_values()
alpha, beta = g.bounds[1], g.beta
print(f"This is {'' if is_gadget else 'NOT '}a ({alpha}-{beta})-gadget")
print("Is strict?", is_strict)
if included_clauses is not None:
assert len(
set(wc.constraint for wc in included_clauses)
& set(wc.constraint for wc in included_clauses_g)
) >= int(len(included_clauses) * args.included_pctg)
included_clauses = included_clauses_g
excluded_clauses = excluded_clauses_g
def _expand_output(
out_descr: List[Tuple[type[Constraint], int]], xvars: List[int]
) -> List[Constraint]:
constrs = []
for constraint_class, arity in out_descr:
constrs.extend(constraint_class.gen_constraints_from_vars(xvars, arity))
return constrs
def model_and_solve(
input_clause_size: int,
max_auxs: int,
alpha_ub: Union[float, int],
included_pctg: float,
excluded_pctg: float,
included_clauses: Sequence[WeightedConstraint],
excluded_clauses: Sequence[Constraint],
first_aux_var: int = 10,
):
input_constr = Clause([i + 1 for i in range(input_clause_size)])
out_constr_family = [(Clause, 2), (Clause, 1)]
restrictions = []
if included_clauses is not None:
# Enforce a percentage for the included clauses
min_num_included = int(len(included_clauses) * included_pctg)
restrictions.append(
AtLeastStructureConstraint(tuple(included_clauses), min_num_included)
)
print(f"Min num included: {min_num_included}")
# Enforce a percentage for the excluded clauses
min_num_excluded = int(len(excluded_clauses) * excluded_pctg)
restrictions.append(
AtMostStructureConstraint(tuple(excluded_clauses), min_num_excluded)
)
g = GurobiGadgetoCompiler.generate(
input_constr,
out_constr_family,
out_structure_constrs=restrictions,
alpha_ub=alpha_ub,
max_auxs=max_auxs,
first_aux_var=first_aux_var,
)
included_clauses_g = set(g.out_constrs)
excluded_clauses_g = set(_expand_output(out_constr_family, g.get_xvars()))
for c in g.out_constrs:
excluded_clauses_g.remove(c.constraint)
return g, included_clauses_g, excluded_clauses_g
if __name__ == "__main__":
main()
Note
You can set a specific weight for the desired constraint using a WeightedConstraint instead of a subclass of Constraint directly.
In this latest case, GadgetoCompiler can decide which weight to use.
-
Carlos Ansótegui and Jordi Levy. Reducing SAT to max2sat. In Zhi-Hua Zhou, editor, Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI 2021, Virtual Event / Montreal, Canada, 19-27 August 2021, 1367–1373. ijcai.org, 2021. ↩