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{Int64, UnitWeight, ProblemReductions.EXTREMA}:
| c = ∧(x, y)
| ##var#333 = ¬(c)
| ##var#334 = ¬(z)
| ##var#332 = ∧(##var#333, ##var#334)
| d = ∨(x, ##var#332)
Symbols: [:c, :x, :y, Symbol("##var#333"), Symbol("##var#334"), :z, Symbol("##var#332"), :d]
julia> variables(circuitsat)1:8
julia> circuitsat.symbols8-element Vector{Symbol}:
 :c
 :x
 :y
 Symbol("##var#333")
 Symbol("##var#334")
 :z
 Symbol("##var#332")
 :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{<:SimpleGraph}, circuitsat)ReductionCircuitToSpinGlass{SimpleGraph{Int64}, Int64}(8, SpinGlass{SimpleGraph{Int64}, Int64, Vector{Int64}}(SimpleGraph{Int64}(11, [[2, 3, 7, 8], [1, 3], [1, 2, 4], [3, 6, 7], [6], [4, 5, 7], [1, 4, 6, 8], [1, 7]]), [1, -2, 1, -2, -2, 1, 1, -2, 1, -2, -2], [0, 1, -2, 1, 0, 1, -3, 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(==(x), circuitsat.symbols[sortperm(result.variables)])indexof (generic function with 1 method)
julia> gadget = LogicGadget(result.spinglass, indexof.([:x, :y, :z]), [indexof(:d)])LogicGadget:
| Problem: SpinGlass{SimpleGraph{Int64}, Int64, Vector{Int64}}(SimpleGraph{Int64}(11, [[2, 3, 7, 8], [1, 3], [1, 2, 4], [3, 6, 7], [6], [4, 5, 7], [1, 4, 6, 8], [1, 7]]), [1, -2, 1, -2, -2, 1, 1, -2, 1, -2, -2], [0, 1, -2, 1, 0, 1, -3, 2])
| Inputs: [1, 2, 5]
| Outputs: [8]
julia> tb = truth_table(gadget; variables=circuitsat.symbols[result.variables])┌───┬───┬───┬───┐
│ y │ c │ z │ d │
├───┼───┼───┼───┤
│ 0 │ 0 │ 0 │ 1 │
│ 1 │ 0 │ 0 │ 1 │
│ 0 │ 1 │ 0 │ 1 │
│ 1 │ 1 │ 0 │ 1 │
│ 0 │ 0 │ 1 │ 0 │
│ 1 │ 0 │ 1 │ 1 │
│ 0 │ 1 │ 1 │ 0 │
│ 1 │ 1 │ 1 │ 1 │
└───┴───┴───┴───┘

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.