Verifying Gadgets

These are the utilities in GadgetoCompiler to verify and analyze gadgets.

Showing Assignment Values and Verifying the Gadget

Method show_assignment_values in the Gadget class shows the values for all the possible assignments to the output constraints of the gadget. It will also check if the given gadget is valid, as well as if it is an strict gadget. For more details you can check the API Documentation.

This will be the code for the example in the Computing Gadgets section when adding this analysis and verification step:

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

g = GurobiGadgetoCompiler.generate(
    Clause([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)

And this will be the generated output:

Input: 1 2 3
Gadget:
0.50: -1 -2     (Clause)
0.50: 1 2       (Clause)
0.50: 4 -1      (Clause)
0.50: 1 -4      (Clause)
0.50: 4 -2      (Clause)
0.50: 2 -4      (Clause)
1.00: 3 4       (Clause)
Sat_gadget_bounds: (2.5, 3.5)
Beta 4.0
#Assigment #Min-Loss #Max-Gain #SAT/UNSAT
(0, 0, 0, 0) 1.5 2.5 UNSAT
(0, 0, 0, 1) 1.5 2.5 UNSAT
(0, 0, 1, 0) 0.5 3.5 SAT
(0, 0, 1, 1) 1.5 2.5 SAT
(0, 1, 0, 0) 1.5 2.5 SAT
(0, 1, 0, 1) 0.5 3.5 SAT
(0, 1, 1, 0) 0.5 3.5 SAT
(0, 1, 1, 1) 0.5 3.5 SAT
(1, 0, 0, 0) 1.5 2.5 SAT
(1, 0, 0, 1) 0.5 3.5 SAT
(1, 0, 1, 0) 0.5 3.5 SAT
(1, 0, 1, 1) 0.5 3.5 SAT
(1, 1, 0, 0) 2.5 1.5 SAT
(1, 1, 0, 1) 0.5 3.5 SAT
(1, 1, 1, 0) 1.5 2.5 SAT
(1, 1, 1, 1) 0.5 3.5 SAT
This is a (3.5-4.0)-gadget
Is strict? True