CircuitSAT -> SpinGlass

In this tutorial, we will demonstrate how to use the Spinglass model to solve the circuit satisfiability problem.

We first define a simple Circuit using the @circuit macro. And then we convert the circuit to a CircuitSAT problem.

julia> using ProblemReductions
julia> circuit = @circuit begin
           c = x ∧ y
           d = x ∨ (¬c ∧ ¬z)
       endCircuit:
| c = ∧(x, y)
| d = ∨(x, ∧(¬(c), ¬(z)))
julia> circuitsat = CircuitSAT(circuit)CircuitSAT:
| c = ∧(x, y)
| ##var#230 = ¬(c)
| ##var#231 = ¬(z)
| ##var#229 = ∧(##var#230, ##var#231)
| d = ∨(x, ##var#229)
Symbols: [:c, :x, :y, Symbol("##var#230"), Symbol("##var#231"), :z, Symbol("##var#229"), :d]
julia> variables(circuitsat)8-element Vector{Int64}:
 1
 2
 3
 4
 5
 6
 7
 8
julia> circuitsat.symbols8-element Vector{Symbol}:
 :c
 :x
 :y
 Symbol("##var#230")
 Symbol("##var#231")
 :z
 Symbol("##var#229")
 :d

The resulting circuitsat expands the expression to a list of simple clauses. The variables are mapped to integers that pointing to the symbols that stored in the symbols field.

The we can convert the circuit to a SpinGlass problem using the reduceto function.

julia> result = reduceto(SpinGlass, circuitsat)ReductionCircuitToSpinGlass{HyperGraph, Vector{Int64}}(8, SpinGlass{HyperGraph, Vector{Int64}}(HyperGraph(8, [[1, 2], [1, 3], [2, 3], [1], [2], [3], [3, 4], [4], [5, 6], [5], [6], [4, 6], [4, 7], [6, 7], [7], [1, 7], [1, 8], [7, 8], [8]]), [1, -2, -2, 0, 1, -2, 1, 1, 1, 0, 1, 1, -2, -2, -3, 1, -2, -2, 2]), [3, 1, 2, 4, 6, 5, 7, 8])

The resulting result is a ReductionCircuitToSpinGlass instance that contains the spin glass problem.

With the result instance, we can define a logic gadget that maps the spin glass variables to the circuit variables.

julia> indexof(x) = findfirst(==(findfirst(==(x), circuitsat.symbols)), result.variables)indexof (generic function with 1 method)
julia> gadget = LogicGadget(result.spinglass, indexof.([:x, :y, :z]), [indexof(:d)])LogicGadget:
| Problem: SpinGlass{HyperGraph, Vector{Int64}}(HyperGraph(8, [[1, 2], [1, 3], [2, 3], [1], [2], [3], [3, 4], [4], [5, 6], [5], [6], [4, 6], [4, 7], [6, 7], [7], [1, 7], [1, 8], [7, 8], [8]]), [1, -2, -2, 0, 1, -2, 1, 1, 1, 0, 1, 1, -2, -2, -3, 1, -2, -2, 2])
| Inputs: [3, 1, 5]
| Outputs: [8]
julia> tb = truth_table(gadget; variables=circuitsat.symbols[result.variables])ERROR: AssertionError: length(d) == 2 ^ ni

The gadget is a LogicGadget instance that maps the spin glass variables to the circuit variables. The truth_table function generates the truth table of the gadget.