Examples

In this section, we show additional examples for defining different constraint families inheriting from the Constraint abstract base class.

Constraints

Cube

from gadgetocompiler.constraints import Constraint

class Cube(Constraint):
    """
    Represents a conjunction of literals.

    Example: Cube([-var1,var2,var3]) represents cube (not var1 and var2 and var3)
    """

    def __init__(self, relation):
        relation = frozenset(relation)
        if any(l == 0 for l in relation):
            raise ValueError("Clause has literal 0")
        super().__init__(relation)

    def __str__(self):
        return " ".join([str(item) for item in self.relation])

    def __repr__(self):
        return str(self)

    def get_arity(self) -> int:
        """Returns the arity of the constraint."""
        return len(self.relation)

    def get_vars(self):
        """Returns the vars in the constraint."""
        return [abs(lit) for lit in self.relation]

    def reify(self, var_mapping, model, assignment):
        pass

    def get_truth_value(self, assignment) -> int:
        """
        Given a full assignment to the vars of the constraint, return 1 if
        the constraint is satisfied, otherwise return 0.

        Args:
            assignment: a map of variables to their assigned value

        Returns:
            1 if the constraint is satisfied, 0 if not.
        """
        true_counter = 0
        for lit in self.relation:
            var = abs(lit)
            if var not in assignment:
                continue
            tv = Cube.get_lit_truth_value(lit, assignment[var])
            if tv == 0:
                return 0
            if tv == 1:
                true_counter += 1
        return 1 if true_counter == len(self.relation) else 2

    @staticmethod
    def get_lit_truth_value(lit: int, value: int):
        """Evaluates a literal under an assignment."""
        if value == 2:
            return 2
        elif (lit < 0 and value == 0) or (lit > 0 and value == 1):
            return 1
        else:
            return 0

    @classmethod
    def gen_constraints_from_vars(cls, vars, arity: int):
        """
        Generate all the possible constraints with
        the specified arity on the given set of variables.

        Args:
            vars: The variables to use when generating constraints.
            arity: The arity of the resulting constraints

        Returns:
            All the possible constraints.
        """
        constraints = []
        for indexs in itertools.combinations(range(len(vars)), arity):
            for value_tuple in itertools.product(*[[0, 1] for _ in range(arity)]):
                lits = []
                for i in range(len(value_tuple)):
                    (
                        lits.append(-vars[indexs[i]])
                        if value_tuple[i] == 0
                        else lits.append(vars[indexs[i]])
                    )
                constraints.append(cls(lits))
        return constraints

    def __eq__(self, other):
        return isinstance(other, self.__class__) and self.relation == other.relation

    def __hash__(self):
        return hash((self.__class__, self.relation))

PosClause

from gadgetocompiler.constraints import Clause
import itertools

class PosClause(Clause):
    """
    Represents a Clause with only positive literals.

    Example: PosClause([a,b,c]) represents Clause (a or b or c)

    """

    def __init__(self, relation):
        self.relation = frozenset(relation)
        if any(l <= 0 for l in relation):
            raise ValueError("PosClause has a negative literal")


    @classmethod
    def gen_constraints_from_vars(cls, vars, arity: int):
        """
        Generate all the possible constraints with
        the specified arity on the given set of variables.

        Args:
            vars: The variables to use when generating constraints.
            arity: The arity of the resulting constraints

        Returns:
            All the possible constraints.
        """
        constraints = []
        for indexs in itertools.combinations(range(len(vars)), arity):
            constraints.append(cls([vars[i] for i in indexs]))

        return constraints

CUT

from gadgetocompiler.constraints import Constraint
import itertools

class CUT(Constraint):
    """
    Represents a CUT constraint.

    Example: CUT([a,b]) represents CUT(a,b) = a xor b

    """

    def __init__(self, relation):
        self.relation = frozenset(relation)
        if any(v <= 0 for v in relation):
            raise ValueError("CUT has a variable with index <= 0")

    def __str__(self):
        return " ".join([str(item) for item in self.relation])

    def __repr__(self):
        return str(self)

    def get_arity(self) -> int:
        """Returns the arity of the constraint."""
        return len(self.relation)

    def get_vars(self):
        """Returns the vars in the constraint."""
        return [abs(lit) for lit in self.relation]

    def reify(self, var_mapping, model, assignment):
        pass

    def get_truth_value(self, assignment) -> int:
        """
        Given a full assignment to the vars of the constraint, return 1 if
        the constraint is satisfied, otherwise return 0.

        Args:
            assignment: a map of variables to their assigned value

        Returns:
            1 if the constraint is satisfied, 0 if not.
        """

        lit_a,lit_b = self.relation

        tv_a = self.get_lit_truth_value(lit_a, assignment[abs(lit_a)])
        tv_b = self.get_lit_truth_value(lit_b, assignment[abs(lit_b)])

        if tv_a == 2 or tv_b == 2: return 2 
        return tv_a ^ tv_b

    @staticmethod
    def get_lit_truth_value(lit: int, value: int):
        """Evaluates a literal under an assignment."""
        if value == 2:
            return 2
        elif (lit < 0 and value == 0) or (lit > 0 and value == 1):
            return 1
        else:
            return 0

    @classmethod
    def gen_constraints_from_vars(cls, vars, arity: int):
        """
        Generate all the possible constraints with
        the specified arity on the given set of variables.

        Args:
            vars: The variables to use when generating constraints.
            arity: The arity of the resulting constraints

        Returns:
            All the possible constraints.
        """
        constraints = []
        for indexs in itertools.combinations(range(len(vars)), arity):
            constraints.append(cls([vars[indexs[0]], vars[indexs[1]]]))

            """
            for value_tuple in itertools.product(*[[0, 1] for _ in range(arity)]):
                lits = []
                for i in range(len(value_tuple)):
                    (
                        lits.append(-vars[indexs[i]])
                        if value_tuple[i] == 0
                        else lits.append(vars[indexs[i]])
                    )
                constraints.append(cls(lits))
            """
        return constraints


    def __eq__(self, other):
        return isinstance(other, self.__class__) and self.relation == other.relation 

    def __hash__(self):
        return hash((self.__class__, self.relation))

DICUT

from gadgetocompiler.constraints import Constraint
import itertools

class DICUT(Constraint):
    """
    Represents DICUT constraint.

    Example: DICUT([a,b]) represents DICUT(a,b) = not a and b
    """

    def __init__(self, relation):
        self.relation = tuple(relation)
        if any(v <= 0 for v in relation):
            raise ValueError("DICUT has a variable index <= 0")

    def __str__(self):
        return " ".join([str(item) for item in self.relation])

    def __repr__(self):
        return str(self)

    def get_arity(self) -> int:
        """Returns the arity of the constraint."""
        return len(self.relation)

    def get_vars(self):
        """Returns the vars in the constraint."""
        return [abs(lit) for lit in self.relation]

    def reify(self, var_mapping, model, assignment):
        pass

    def get_truth_value(self, assignment) -> int:
        """
        Given a full assignment to the vars of the constraint, return 1 if
        the constraint is satisfied, otherwise return 0.

        Args:
            assignment: a map of variables to their assigned value

        Returns:
            1 if the constraint is satisfied, 0 if not.
        """

        lit_a,lit_b = self.relation

        tv_a = self.get_lit_truth_value(lit_a, assignment[abs(lit_a)])
        tv_b = self.get_lit_truth_value(lit_b, assignment[abs(lit_b)])

        if tv_b == 0: return 0
        if tv_a == 1: return 0
        if tv_a == 2 or tv_b == 2: return 2 
        return 1

    @staticmethod
    def get_lit_truth_value(lit: int, value: int):
        """Evaluates a literal under an assignment."""
        if value == 2:
            return 2
        elif (lit < 0 and value == 0) or (lit > 0 and value == 1):
            return 1
        else:
            return 0

    @classmethod
    def gen_constraints_from_vars(cls, vars, arity: int):
        """
        Generate all the possible constraints with
        the specified arity on the given set of variables.

        Args:
            vars: The variables to use when generating constraints.
            arity: The arity of the resulting constraints

        Returns:
            All the possible constraints.
        """
        constraints = []
        for indexs in itertools.permutations(range(len(vars)), arity):

            constraints.append(cls([vars[indexs[0]], vars[indexs[1]]]))

        return constraints


    def __eq__(self, other):
        return isinstance(other, self.__class__) and self.relation == other.relation 

    def __hash__(self):
        return hash((self.__class__, self.relation))

PC

from gadgetocompiler.constraints import Constraint

class PC(Constraint):
    """
    Represents Partity Check constraints.

    Example: PC([a,b,c],i) represents PC_i(a,b,c) where
        PC_i(a,b,c) = 1 if a xor b xor c == i.
        PC_i(a,b,c) = 0 otherwise.
    """

    def __init__(self, relation, i):
        self.relation = list(relation)
        self.i = i
        if any(v <= 0 for v in relation):
            raise ValueError("PC constraints has a variable index <= 0")

    def __str__(self):
        return " ".join([str(item) for item in self.relation])+" "+str(self.i)

    def __repr__(self):
        return str(self)

    def get_arity(self) -> int:
        """Returns the arity of the constraint."""
        return len(self.relation)

    def get_vars(self):
        """Returns the vars in the constraint."""
        return [abs(lit) for lit in self.relation]

    def reify(self, var_mapping, model, assignment):
        pass

    def get_truth_value(self, assignment) -> int:
        """
        Given a full assignment to the vars of the constraint, return 1 if
        the constraint is satisfied, otherwise return 0.

        Args:
            assignment: a map of variables to their assigned value

        Returns:
            1 if the constraint is satisfied, 0 if not.
        """

        lit_a,lit_b,lit_c = self.relation

        tv_a = self.get_lit_truth_value(lit_a, assignment[abs(lit_a)])
        tv_b = self.get_lit_truth_value(lit_b, assignment[abs(lit_b)])
        tv_c = self.get_lit_truth_value(lit_c, assignment[abs(lit_c)])
        if tv_a == 2 or tv_b == 2 or tv_c ==2: return 2 


        if tv_a ^ tv_b ^ tv_c ==  self.i: return 1
        return 0

    @staticmethod
    def get_lit_truth_value(lit: int, value: int):
        """Evaluates a literal under an assignment."""
        if value == 2:
            return 2
        elif (lit < 0 and value == 0) or (lit > 0 and value == 1):
            return 1
        else:
            return 0

    @classmethod
    def gen_constraints_from_vars(cls, vars, arity: int):
        pass

    def __eq__(self, other):
        return isinstance(other, self.__class__) and self.relation == other.relation and self.i == other.i

    def __hash__(self):
        return hash((self.__class__, self.relation, self.i))

RMBC

from gadgetocompiler.constraints import Constraint

class RMBC(Constraint):
    """
    Represents Respect of Monomial Basis Check cosntraint.

    Example: RMC([a,b,c,d],i,j) represents RMBC_{ij}(a,b,c,d).
    if a==0 and b == c xor i, RMBC_{ij}(a,b,c,d) = 1
    if a==1 and b == d xor j, RMBC_{ij}(a,b,c,d) = 1
    otherwise RMBC_{ij}(a,b,c,d) = 0 
    """

    def __init__(self, relation, i, j):
        self.relation = list(relation)
        self.i = i
        self.j = j
        if any(l == 0 for l in relation):
            raise ValueError("Clause has literal 0")

    def __str__(self):
        return " ".join([str(item) for item in self.relation])+" "+str(self.i)+" "+str(self.j)

    def __repr__(self):
        return str(self)

    def get_arity(self) -> int:
        """Returns the arity of the constraint."""
        return len(self.relation)

    def get_vars(self):
        """Returns the vars in the constraint."""
        return [abs(lit) for lit in self.relation]

    def reify(self, var_mapping, model, assignment):
        pass

    def get_truth_value(self, assignment) -> int:
        """
        Given a full assignment to the vars of the constraint, return 1 if
        the constraint is satisfied, otherwise return 0.

        Args:
            assignment: a map of variables to their assigned value

        Returns:
            1 if the constraint is satisfied, 0 if not.
        """

        lit_a,lit_b,lit_c,lit_d = self.relation

        tv_a = RMBC.get_lit_truth_value(lit_a, assignment[abs(lit_a)])
        tv_b = RMBC.get_lit_truth_value(lit_b, assignment[abs(lit_b)])
        tv_c = RMBC.get_lit_truth_value(lit_c, assignment[abs(lit_c)])
        tv_d = RMBC.get_lit_truth_value(lit_d, assignment[abs(lit_d)])
        if tv_a == 2 or tv_b == 2 or tv_c ==2 or tv_d == 2: return 2 

        if tv_a == 1 and (tv_b == (tv_c ^ self.i)): return 1
        if tv_a == 0 and (tv_b == (tv_d ^ self.j)): return 1
        return 0

    @staticmethod
    def get_lit_truth_value(lit: int, value: int):
        """Evaluates a literal under an assignment."""
        if value == 2:
            return 2
        elif (lit < 0 and value == 0) or (lit > 0 and value == 1):
            return 1
        else:
            return 0

    @classmethod
    def gen_constraints_from_vars(cls, vars, arity: int):
        pass

    def __eq__(self, other):
        return isinstance(other, self.__class__) and self.relation == other.relation and self.i == other.i and self.j == other.j

    def __hash__(self):
        return hash((self.__class__, self.relation, self.i, self.j))

Gadgets Compilation

3ConjSAT to 2SAT

from gadgetocompiler.constraints import Clause
from gadgetocompiler.compilers.gurobi import GurobiGadgetoCompiler
from Cube import Cube
g = GurobiGadgetoCompiler.generate(
    Cube([1, 2, 3]),  # The input constraint
    [(Clause, 2), (Clause, 1)],  # The output family constraints
    alpha_ub=10,  # We must set an upper bound for the alpha
    max_auxs=1,  # As well as the maximum number of aux variables that we will use

)
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)

PC to 2SAT

import argparse

from gadgetocompiler.constraints import Clause
from gadgetocompiler.compilers.gurobi import GurobiGadgetoCompiler
from PC import PC

parser = argparse.ArgumentParser()
parser.add_argument("--i", type=int, required=True)
parser.add_argument("--max-auxs", "-b", type=int, required=True)
args = parser.parse_args()

print(f"i: {args.i}")
print(f"max_auxs: {args.max_auxs}")

g = GurobiGadgetoCompiler.generate(
    PC([1, 2, 3], args.i),  # The input constraint
    [(Clause, 2), (Clause, 1)],  # The output family constraints
    alpha_ub=14,  # We must set an upper bound for the alpha
    max_auxs=args.max_auxs,  # As well as the maximum number of aux variables that we will use
)
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)

PC to 3SAT

import argparse

from gadgetocompiler.constraints import Clause
from gadgetocompiler.compilers.gurobi import GurobiGadgetoCompiler
from PC import PC

parser = argparse.ArgumentParser()
parser.add_argument("--i", type=int, required=True)
parser.add_argument("--max-auxs", "-b", type=int, required=True)
args = parser.parse_args()

print(f"i: {args.i}")
print(f"max_auxs: {args.max_auxs}")

g = GurobiGadgetoCompiler.generate(
    PC([1, 2, 3],args.i),  # The input constraint
    [(Clause, 3), (Clause, 2), (Clause, 1)],  # The output family constraints
    alpha_ub=14,  # We must set an upper bound for the alpha
    max_auxs=args.max_auxs,  # As well as the maximum number of aux variables that we will use
)
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)

PC to CUT/0

import argparse

from gadgetocompiler.constraints import Clause
from gadgetocompiler.compilers.gurobi import GurobiGadgetoCompiler
from PC import PC
from CUT import CUT
from PosClause import PosClause

parser = argparse.ArgumentParser()
parser.add_argument("--i", type=int, required=True)
parser.add_argument("--max-auxs", "-b", type=int, required=True)
args = parser.parse_args()

print(f"i: {args.i}")
print(f"max_auxs: {args.max_auxs}")

g = GurobiGadgetoCompiler.generate(
    PC([1, 2, 3],args.i),  # The input constraint
    [(CUT, 2), (PosClause,1)],  # The output family constraints
    alpha_ub=14,  # We must set an upper bound for the alpha
    max_auxs=args.max_auxs,  # As well as the maximum number of aux variables that we will use
)
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)

PC to DICUT

import argparse

from gadgetocompiler.compilers.z3 import Z3GadgetoCompiler
from gadgetocompiler.constraints import Clause
from gadgetocompiler.compilers.gurobi import GurobiGadgetoCompiler
from PC import PC
from DICUT import DICUT

parser = argparse.ArgumentParser()
parser.add_argument("--i", type=int, required=True)
parser.add_argument("--max-auxs", "-b", type=int, required=True)
args = parser.parse_args()

print(f"i: {args.i}")
print(f"max_auxs: {args.max_auxs}")

g = GurobiGadgetoCompiler.generate(
    PC([1, 2, 3], args.i),  # The input constraint
    [(DICUT, 2)],  # The output family constraints
    alpha_ub=14,  # We must set an upper bound for the alpha
    max_auxs=args.max_auxs,  # As well as the maximum number of aux variables that we will use
)
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)

RMBC to 2SAT

import argparse

from gadgetocompiler.constraints import Clause
from gadgetocompiler.compilers.gurobi import GurobiGadgetoCompiler
from RMBC import RMBC

parser = argparse.ArgumentParser()
parser.add_argument("--i", type=int, required=True)
parser.add_argument("--j", type=int, required=True)
parser.add_argument("--max-auxs", "-b", type=int, required=True)
args = parser.parse_args()

print(f"i: {args.i}")
print(f"j: {args.j}")
print(f"max_auxs: {args.max_auxs}")

g = GurobiGadgetoCompiler.generate(
    RMBC([1, 2, 3, 4], args.i, args.j),  # The input constraint
    [(Clause, 2), (Clause, 1)],  # The output family constraints
    alpha_ub=12.5,  # We must set an upper bound for the alpha
    max_auxs=args.max_auxs,  # As well as the maximum number of aux variables that we will use
)
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)

RMBC to 3SAT

import argparse

from gadgetocompiler.constraints import Clause
from gadgetocompiler.compilers.gurobi import GurobiGadgetoCompiler
from RMBC import RMBC

parser = argparse.ArgumentParser()
parser.add_argument("--i", type=int, required=True)
parser.add_argument("--j", type=int, required=True)
parser.add_argument("--max-auxs", "-b", type=int, required=True)
args = parser.parse_args()

print(f"i: {args.i}")
print(f"j: {args.j}")
print(f"max_auxs: {args.max_auxs}")

g = GurobiGadgetoCompiler.generate(
    RMBC([1, 2, 3, 4], args.i, args.j),  # The input constraint
    [(Clause, 3), (Clause, 2), (Clause, 1)],  # The output family constraints
    alpha_ub=12.5,  # We must set an upper bound for the alpha
    max_auxs=args.max_auxs,  # As well as the maximum number of aux variables that we will use
)
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)

RMBC to CUT/0

import argparse

from gadgetocompiler.constraints import Clause
from gadgetocompiler.compilers.gurobi import GurobiGadgetoCompiler
from RMBC import RMBC
from CUT import CUT
from PosClause import PosClause

parser = argparse.ArgumentParser()
parser.add_argument("--i", type=int, required=True)
parser.add_argument("--j", type=int, required=True)
parser.add_argument("--max-auxs", "-b", type=int, required=True)
args = parser.parse_args()

print(f"i: {args.i}")
print(f"j: {args.j}")
print(f"max_auxs: {args.max_auxs}")

g = GurobiGadgetoCompiler.generate(
    RMBC([1, 2, 3, 4], args.i, args.j),  # The input constraint
    [(CUT, 2), (PosClause,1)],  # The output family constraints
    alpha_ub=12.5,  # We must set an upper bound for the alpha
    max_auxs=args.max_auxs,  # As well as the maximum number of aux variables that we will use
)
g.show()

RMBC to DICUT

import argparse

from gadgetocompiler.constraints import Clause
from gadgetocompiler.compilers.gurobi import GurobiGadgetoCompiler
from RMBC import RMBC
from DICUT import DICUT

parser = argparse.ArgumentParser()
parser.add_argument("--i", type=int, required=True)
parser.add_argument("--j", type=int, required=True)
parser.add_argument("--max-auxs", "-b", type=int, required=True)
args = parser.parse_args()

print(f"i: {args.i}")
print(f"j: {args.j}")
print(f"max_auxs: {args.max_auxs}")

g = GurobiGadgetoCompiler.generate(
    RMBC([1, 2, 3, 4], args.i, args.j),  # The input constraint
    [(DICUT, 2)],  # The output family constraints
    alpha_ub=12.5,  # We must set an upper bound for the alpha
    max_auxs=args.max_auxs,  # As well as the maximum number of aux variables that we will use
)
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)

Optimal Gadgets

	\(\alpha\)	\(\beta\)	# Auxs Vars	Time (s)	Gadget
3SAT -> 2SAT	3.5	4	1	5	details
3ConjSAT -> 2SAT	4	4	1	5	details
\(PC_0\) -> 3SAT	4	4	0	2	details
\(PC_1\) -> 3SAT	4	4	0	7	details
\(PC_0\) -> 2SAT	11	12	4	11	details
\(PC_1\) -> 2SAT	11	12	4	7	details
\(PC_0\) -> CUT/0	8	10	8	23101	details
\(PC_1\) -> CUT/0	9	14	1	5	details
\(PC_0\) -> DICUT	6.5	15.5	7	761	details
\(PC_1\) -> DICUT	6.5	15.5	7	876	details
\(RMBC_{00}\) -> 3SAT	4	4	0	2	details
\(RMBC_{01}\) -> 3SAT	4	4	0	2	details
\(RMBC_{10}\) -> 3SAT	4	4	0	2	details
\(RMBC_{11}\) -> 3SAT	4	4	0	2	details
\(RMBC_{00}\) -> 2SAT	11	12	4	32	details
\(RMBC_{01}\) -> 2SAT	11	12	4	59	details
\(RMBC_{10}\) -> 2SAT	11	12	4	25	details
\(RMBC_{11}\) -> 2SAT	11	12	4	55	details
\(RMBC_{00}\) -> CUT/0	8	11	5	285	details
\(RMBC_{11}\) -> CUT/0	9	13	3	3	details
\(RMBC_{00}\) -> DICUT	6	16	2	2	details
\(RMBC_{01}\) -> DICUT	6.5	15.5	7	11454*	details
\(RMBC_{10}\) -> DICUT	6.5	15.5	7	5043*	details
\(RMBC_{11}\) -> DICUT	7	20	2	2	details

For results with "*" we used Gurobi with 40 threads. Otherwise, only one thread.