Skip to content

API Reference

Gadgets

gadgetocompiler.gadgets.Gadget dataclass

Represents a compiled gadget for a constraint.

Attributes:

  • in_constr (Constraint) –

    The input constraint

  • out_constrs (List[WeightedConstraint]) –

    The output constraints, with an associated weight

  • bounds (Tuple[Union[int, float, Fraction], Union[int, float, Fraction]]) –

    TODO

  • beta (Union[int, float, Fraction]) –

    the sum of all the weights for the output constraints

get_xvars()

Find all the variables in the gadget, including variables from the input constraint and all the output constraints.

show()

Pretty printing of a gadget to stdout

show_assignment_values()

Performs an exhaustive enumeration and checks that all interpretations satisfy the constraints for the gadget.

.. warning:: This method should be used only for small problem instances.

Returns:

  • –

    true if the gadget satisfies the constraints.

gadgetocompiler.gadgets.WeightedConstraint dataclass

Represents a clause with an associated weight

Source code in src/gadgetocompiler/gadgets.py 
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
@dataclasses.dataclass(frozen=True)
class WeightedConstraint:
    """Represents a clause with an associated weight"""

    weight: Union[int, float, Fraction]
    constraint: Constraint

    def __str__(self):
        if isinstance(self.weight, Fraction):
            weight_str = str(self.weight)  # exact representation like 3/4
        elif isinstance(self.weight, float):
            weight_str = f"{self.weight:.2f}"
        else:  # int (or anything else numeric)
            weight_str = str(self.weight)

        return (
            f"{weight_str}: {self.constraint}\t({self.constraint.__class__.__name__})"
        )

Constraints

gadgetocompiler.constraints.Constraint

Bases: ABC

Represents a constraint in a gadget, both for input and output constriants.

Parameters:

  • relation (Any) –

    a metastructure that defines the constraint

Attributes: relation: a metastructure that defines the constraint

Source code in src/gadgetocompiler/constraints.py 
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
class Constraint(ABC):
    """
    Represents a constraint in a gadget, both for input and output constriants.

    Args:
        relation: a metastructure that defines the constraint
    Attributes:
        relation: a metastructure that defines the constraint
    """

    def __init__(self, relation: Any):
        self.relation = relation

    @abstractmethod
    def get_arity(self) -> int:
        """Returns the arity of the constraint."""
        raise NotImplementedError

    @abstractmethod
    def get_vars(self) -> Sequence[int]:  # TODO: decide type
        """Returns the vars in the constraint."""  # TODO: leave the var type as implementation defined?
        raise NotImplementedError

    @abstractmethod
    def reify(
        self,
        var_mapping: Dict[int, List[gb.Var]],
        model: gb.Model,
        assignment=None,
    ) -> gb.Var:
        """
        Returns b, a new boolean binary gurobi var that reifies
        the constraint, i.e, b == 1 iff Constraint is True

        Args:
            x2gb: a dict of propositional vars to gurobi vars
            gb_model: a gurobi model

        Returns:
            A gurobi variable representing the reification
        """
        # TODO: type for x2gb, should be tuple? change this in gadgets.py if needed
        raise NotImplementedError

    # Genrate all the possible constraints on the set of vars
    @classmethod
    @abstractmethod
    def gen_constraints_from_vars(cls, vars: Sequence[int], arity: int) -> List[Self]:
        """
        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.
        """
        raise NotImplementedError

    # Evaluates the constraint under an assignment
    @abstractmethod
    def get_truth_value(self, assignment: Dict[int, bool]):
        """
        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.
        """
        # TODO: assignment dict[int, bool] or dict[int,int]?
        raise NotImplementedError

    @abstractmethod
    def __eq__(self, other):
        raise NotImplementedError

    @abstractmethod
    def __hash__(self):
        raise NotImplementedError

gen_constraints_from_vars(vars, arity) abstractmethod classmethod

Generate all the possible constraints with the specified arity on the given set of variables.

Parameters:

  • vars (Sequence[int]) –

    The variables to use when generating constraints.

  • arity (int) –

    The arity of the resulting constraints

Returns:

  • List[Self] –

    All the possible constraints.

Source code in src/gadgetocompiler/constraints.py 
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
@classmethod
@abstractmethod
def gen_constraints_from_vars(cls, vars: Sequence[int], arity: int) -> List[Self]:
    """
    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.
    """
    raise NotImplementedError

get_arity() abstractmethod

Returns the arity of the constraint.

Source code in src/gadgetocompiler/constraints.py 
27
28
29
30
@abstractmethod
def get_arity(self) -> int:
    """Returns the arity of the constraint."""
    raise NotImplementedError

get_truth_value(assignment) abstractmethod

Given a full assignment to the vars of the constraint, return 1 if the constraint is satisfied, otherwise return 0.

Parameters:

  • assignment (Dict[int, bool]) –

    a map of variables to their assigned value

Returns:

  • –

    1 if the constraint is satisfied, 0 if not.

Source code in src/gadgetocompiler/constraints.py 
76
77
78
79
80
81
82
83
84
85
86
87
88
89
@abstractmethod
def get_truth_value(self, assignment: Dict[int, bool]):
    """
    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.
    """
    # TODO: assignment dict[int, bool] or dict[int,int]?
    raise NotImplementedError

get_vars() abstractmethod

Returns the vars in the constraint.

Source code in src/gadgetocompiler/constraints.py 
32
33
34
35
@abstractmethod
def get_vars(self) -> Sequence[int]:  # TODO: decide type
    """Returns the vars in the constraint."""  # TODO: leave the var type as implementation defined?
    raise NotImplementedError

reify(var_mapping, model, assignment=None) abstractmethod

Returns b, a new boolean binary gurobi var that reifies the constraint, i.e, b == 1 iff Constraint is True

Parameters:

  • x2gb –

    a dict of propositional vars to gurobi vars

  • gb_model –

    a gurobi model

Returns:

  • Var –

    A gurobi variable representing the reification

Source code in src/gadgetocompiler/constraints.py 
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
@abstractmethod
def reify(
    self,
    var_mapping: Dict[int, List[gb.Var]],
    model: gb.Model,
    assignment=None,
) -> gb.Var:
    """
    Returns b, a new boolean binary gurobi var that reifies
    the constraint, i.e, b == 1 iff Constraint is True

    Args:
        x2gb: a dict of propositional vars to gurobi vars
        gb_model: a gurobi model

    Returns:
        A gurobi variable representing the reification
    """
    # TODO: type for x2gb, should be tuple? change this in gadgets.py if needed
    raise NotImplementedError

gadgetocompiler.constraints.Clause

Bases: Constraint

Represents a disjunction of literals.

Example: Clause([-var1,var2,var3]) represents clause (not var1 or var2 or var3)

Source code in src/gadgetocompiler/constraints.py 
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
class Clause(Constraint):
    """
    Represents a disjunction of literals.

    Example: Clause([-var1,var2,var3]) represents clause (not var1 or var2 or 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 reify(self, var_mapping, model, assignment=None):

        if assignment:
            # We return the truth value if clause is satisfied or unsatisfied
            is_sat = self.get_truth_value(assignment)
            if is_sat != 2:
                return is_sat

            # Otherwise, reify only the auxiliary variables
            # We can do that because at this point these are
            # the only ones remaining in the clause (the others are falsified)
            lits = []
            for lit in self.relation:
                var = abs(lit)
                if var not in var_mapping:
                    continue
                lits.append(var_mapping[var][1] if lit > 0 else var_mapping[var][0])

            if len(lits) == 1:
                return lits[0]
            expr = sum(lits)
            b = model.addVar(vtype=gb.GRB.BINARY)
            model.addConstr((b == 1) >> (expr >= 1))
            model.addConstr((b == 0) >> (expr <= 0))
            return b

        expr = 0
        for lit in self.relation:
            var = abs(lit)
            if lit < 0:
                expr += 1 - (var_mapping[var][1])
            else:
                expr += var_mapping[var][1]

        b = model.addVar(vtype=gb.GRB.BINARY)
        model.addConstr((b == 1) >> (expr >= 1))
        model.addConstr((b == 0) >> (expr <= 0))

        return b

    def get_arity(self):
        return len(self.relation)

    def get_vars(self):
        return [abs(lit) for lit in self.relation]

    def get_truth_value(self, assignment):
        false_counter = 0
        for lit in self.relation:
            var = abs(lit)
            if var not in assignment:
                continue
            tv = Clause.get_lit_truth_value(lit, assignment[var])
            if tv == 1:
                return 1
            if tv == 0:
                false_counter += 1
        return 0 if false_counter == len(self.relation) else 2

    # Evaluates a literal under an assignment
    @staticmethod
    def get_lit_truth_value(lit, value):
        # TODO: do we keep this method?
        # TODO: value int? bool?
        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):
        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))

GadgetoCompilers

gadgetocompiler.compilers.AtMostStructureConstraint dataclass

Represents a restriction stating that at most K constraints appear with a specific weight.

If a constraint in the restriction is a weighted constraint, the specific weight is the one provided. If it is a constraint (i.e. without weight) then the weight is set to be larger than 0.

Attributes constraints: the constraints involved in the AMK k: The bound of the restriction

Source code in src/gadgetocompiler/compilers/__init__.py 
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
@dataclasses.dataclass(frozen=True)
class AtMostStructureConstraint:
    """
    Represents a restriction stating that at most K constraints
    appear with a specific weight.

    If a constraint in the restriction is a weighted constraint, the
    specific weight is the one provided. If it is a constraint
    (i.e. without weight) then the weight is set to be larger than 0.

    Attributes
        constraints: the constraints involved in the AMK
        k: The bound of the restriction
    """

    constraints: Tuple[Union[Constraint, WeightedConstraint]]
    k: int

gadgetocompiler.compilers.AtLeastStructureConstraint dataclass

Represents a restriction stating that at least K constraints appear with a specific weight.

If a constraint in the restriction is a weighted constraint, the specific weight is the one provided. If it is a constraint (i.e. without weight) then the weight is set to be larger than 0.

Attributes constraints: the constraints involved in the ALK k: The bound of the restriction

Source code in src/gadgetocompiler/compilers/__init__.py 
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
@dataclasses.dataclass(frozen=True)
class AtLeastStructureConstraint:
    """
    Represents a restriction stating that at least K constraints
    appear with a specific weight.

    If a constraint in the restriction is a weighted constraint, the
    specific weight is the one provided. If it is a constraint
    (i.e. without weight) then the weight is set to be larger than 0.

    Attributes
        constraints: the constraints involved in the ALK
        k: The bound of the restriction
    """

    constraints: Tuple[Union[Constraint, WeightedConstraint]]
    k: int

gadgetocompiler.compilers.gurobi.GurobiGadgetoCompiler

Compiles optimal gadgets using Gurobi

generate(in_constr, out_constr_family, out_structure_constrs=None, max_auxs=None, first_aux_var=None, *, minimize_alpha=True, strict_gadget=True, alpha_lb=0.0, alpha_ub=sys.maxsize, alpha_gap=1.0, decimal_precision=5, float_weights=True, weights_lb=0.0, weights_ub=sys.maxsize, expand_all=True, seed=None, gurobi_output_flag=1, gurobi_threads=1, gurobi_parameters=None, gurobi_callback=None, initial_solution=None) classmethod

Compile a gadget

Parameters:

  • in_constr (Constraint) –

    The input constraint.

  • out_constr_family (List[Tuple[type[Constraint], int]]) –

    The type of constraints the generator can use as output. This is a list of type of constraint and its arity.

  • out_structure_constrs (Optional[List[AtMostStructureConstraint | AtLeastStructureConstraint]], default: None ) –

    A set of restrictions to impose on the output constraints.

  • minimize_alpha (bool, default: True ) –

    TODO

  • strict_gadget (bool, default: True ) –

    Enforce that for each unsatisfiable assignment on the original constraint, there exist one extension s.t \(I'(P) = lpha - lpha_{gap}\)

  • max_auxs (Optional[int], default: None ) –

    How many auxiliary variables the generator can use

  • first_aux_var (Optional[int], default: None ) –

    the starting auxiliary variable

  • alpha_lb (float, default: 0.0 ) –

    A lower bound on \(lpha\)

  • alpha_ub (float, default: maxsize ) –

    An upper bound on \(lpha\)

  • alpha_gap (float, default: 1.0 ) –

    TODO

  • decimal_precision (int, default: 5 ) –

    How many decimal digits to consider for the solution

  • float_weights (bool, default: True ) –

    If false, enforces the weights of the output constraints to be integers

  • weights_lb (float, default: 0.0 ) –

    A lower bound on the weights for the clauses

  • weights_ub (float, default: maxsize ) –

    An upper bound on the weights for the clauses

  • expand_all (bool, default: True ) –

    TODO

  • seed (Optional[int], default: None ) –

    The random seed that Gurobi will use

  • gurobi_output_flag (int, default: 1 ) –

    How verbose Gurobi is (see https://docs.gurobi.com/projects/optimizer/en/current/reference/parameters.html#parameteroutputflag)

  • gurobi_threads (int, default: 1 ) –

    The number of parallel threads for Gurobi to use during the solving process

  • gurobi_parameters (Optional[Dict[str, Any]], default: None ) –

    A dictionary of parameters to set for Gurobi.

  • gurobi_callback –

    See https://docs.gurobi.com/projects/optimizer/en/current/reference/python/callback.html

  • initial_solution (Optional[Gadget], default: None ) –

    A compiled gadget that can be used as a starting point for Gurobi

Returns:

  • –

    An optimal gadget if found, None otherwise

verify(gadget, verbose=False) classmethod

Verifies that a compiled gadget is valid.

Parameters:

  • gadget (Gadget) –

    The gadget to verify

  • verbose (bool, default: False ) –

    Print extra information when verifying the gadget

Returns:

  • bool –

    True if the gadget is valid, false otherwise.

gadgetocompiler.compilers.pb.PbGadgetoCompiler

Compiles optimal gadgets using a Pseudo Boolean solver