Circuit Satisfaction

Problem Definition

A circuit can be defined with the @circuit macro as follows:

julia> using ProblemReductions
julia> circuit = @circuit begin
           c = x ∧ y
           d = x ∨ (c ∧ ¬z)
       endCircuit:
| c = ∧(x, y)
| d = ∨(x, ∧(c, ¬(z)))

The circuit can be converted to a CircuitSAT problem instance:

julia> sat = CircuitSAT(circuit)CircuitSAT:
| c = ∧(x, y)
| ##var#228 = ¬(z)
| ##var#227 = ∧(c, ##var#228)
| d = ∨(x, ##var#227)
Symbols: [:c, :x, :y, Symbol("##var#228"), :z, Symbol("##var#227"), :d]
julia> sat.symbols7-element Vector{Symbol}:
 :c
 :x
 :y
 Symbol("##var#228")
 :z
 Symbol("##var#227")
 :d

Note that the circuit is converted to the static single assignment (SSA) form, and the symbols are stored in the symbols field. The symbols are variables in the circuit to be assigned to true or false.

Interfaces

julia> variables(sat)7-element Vector{Int64}:
 1
 2
 3
 4
 5
 6
 7
julia> flavors(sat)2-element Vector{Int64}:
 0
 1

The circuit can be evaluated with the evaluate function:

julia> evaluate(sat, [true, false, true, true, false, false, true])1

The return value is 0 if the assignment satisfies the circuit, otherwise, it is the number of unsatisfied clauses.

To find all satisfying assignments, use the findbest function:

julia> findbest(sat, BruteForce())8-element Vector{Vector{Int64}}:
 [0, 0, 0, 1, 0, 0, 0]
 [0, 0, 1, 1, 0, 0, 0]
 [0, 0, 0, 0, 1, 0, 0]
 [0, 0, 1, 0, 1, 0, 0]
 [0, 1, 0, 1, 0, 0, 1]
 [0, 1, 0, 0, 1, 0, 1]
 [1, 1, 1, 0, 1, 0, 1]
 [1, 1, 1, 1, 0, 1, 1]

Here, the BruteForce solver is used to find the best assignment.