Defining Gadgets Manually
In this section, we show how to specify Gadgets manually in GadgetoCompiler.
The Regular Gadget 1¶
This code generates the Regular gadget from this work 1:
import sys
from gadgetocompiler.constraints import Clause
from gadgetocompiler.gadgets import Gadget, WeightedConstraint
def regular_gadget(clause: Clause) -> Gadget:
"""Regular gadget implementation.
Defined in this work [1].
[1] 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
"""
x = {i + 1: v for i, v in enumerate(clause.get_vars())}
k = len(x)
next_aux = max(map(abs, x.values())) + 1
b = {i + 1: next_aux + i for i in range(k - 1)}
b[k - 1] = x[k]
out = []
for i in range(1, k + 1):
out.append(WeightedConstraint(1, Clause([x[i]])))
for i in range(1, k):
out.append(WeightedConstraint(1, Clause([-x[i], -b[i]])))
for i in range(1, k - 1):
out.append(WeightedConstraint(1, Clause([-x[i + 1], b[i]])))
for i in range(1, k - 1):
out.append(WeightedConstraint(1, Clause([b[i], -b[i + 1]])))
alpha = 3 * (clause.get_arity() - 2) + 2
return Gadget(clause, out, (alpha - 1, alpha))
k = int(sys.argv[1])
g = regular_gadget(Clause(range(1, k + 1)))
g.show()
is_gadget, is_strict = g.show_assignment_values()
print("Is gadget?", is_gadget)
print("Is strict?", is_strict)
The Refined Regular Gadget 1¶
This code generates the Refined Regular gadget from this work 1:
import sys
from gadgetocompiler.constraints import Clause
from gadgetocompiler.gadgets import Gadget, WeightedConstraint
def refined_regular_gadget(clause: Clause) -> Gadget:
"""Refined regular gadget implementation.
Defined in this work [1].
[1] 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
"""
x = {i + 1: v for i, v in enumerate(clause.get_vars())}
k = len(x)
next_aux = max(map(abs, x.values())) + 1
b = {i + 1: next_aux + i for i in range(k - 1)}
b[k - 1] = x[k]
out = []
out.append(WeightedConstraint(1, Clause([x[1], b[1]])))
for i in range(1, k - 1):
out.append(WeightedConstraint(0.5, Clause([x[i + 1], -b[i]])))
out.append(WeightedConstraint(0.5, Clause([x[i + 1], b[i + 1]])))
out.append(WeightedConstraint(0.5, Clause([b[i], -b[i + 1]])))
out.append(WeightedConstraint(0.5, Clause([-x[i + 1], b[i]])))
out.append(WeightedConstraint(0.5, Clause([-x[i + 1], -b[i + 1]])))
out.append(WeightedConstraint(0.5, Clause([-b[i], b[i + 1]])))
alpha = 2.5 * (clause.get_arity() - 2) + 1
return Gadget(clause, out, (alpha - 1, alpha))
k = int(sys.argv[1])
g = refined_regular_gadget(Clause(range(1, k + 1)))
g.show()
is_gadget, is_strict = g.show_assignment_values()
print("Is gadget?", is_gadget)
print("Is strict?", is_strict)