Satisfiability

Problem Definition

Satisfiability (also called SAT) problem is to find the boolean assignment that satisfies a Conjunctive Normal Form (CNF). A tipical CNF would look like:

\[\left(l_{11} \vee \ldots \vee l_{1 n_1}\right) \wedge \ldots \wedge\left(l_{m 1} \vee \ldots \vee l_{m n_m}\right)\]

where literals are joint by $\vee$ to form clauses and clauses are joint by $\wedge$ to form a CNF.

We should note that all the SAT problem problem can be reduced to the $3$-SAT problem and it can be proved that $3$-SAT is NP-complete.

Interfaces

To define an Satisfiability problem, we need to construct boolean variables, clauses, CNF.

julia> using ProblemReductions
julia> bv1 = BoolVar("x")x
julia> bv2 = BoolVar("y")y
julia> bv3 = BoolVar("z", true)¬z
julia> clause1 = CNFClause([bv1, bv2, bv3])x ∨ y ∨ ¬z
julia> clause2 = CNFClause([BoolVar("w"), bv1, BoolVar("x", true)])w ∨ x ∨ ¬x
julia> cnf_test = CNF([clause1, clause2])(x ∨ y ∨ ¬z) ∧ (w ∨ x ∨ ¬x)
julia> sat_test = Satisfiability(cnf_test)Satisfiability{String}(["x", "y", "z", "w"], (x ∨ y ∨ ¬z) ∧ (w ∨ x ∨ ¬x))

Besides, the required functions, variables, flavors, and evaluate, and optional functions, findbest, are implemented for the Satisfiability problem.

julia> variables(sat_test)  # degrees of freedom4-element Vector{String}:
 "x"
 "y"
 "z"
 "w"
julia> flavors(sat_test)  # flavors of the literals2-element Vector{Int64}:
 0
 1
julia> evaluate(sat_test, [1, 1, 1, 1]) # Positive sample0
julia> evaluate(sat_test, [0, 0, 1, 0]) # Negative sample1
julia> findbest(sat_test, BruteForce())  # solve the problem with brute force14-element Vector{Vector{Int64}}:
 [0, 0, 0, 0]
 [1, 0, 0, 0]
 [0, 1, 0, 0]
 [1, 1, 0, 0]
 [1, 0, 1, 0]
 [0, 1, 1, 0]
 [1, 1, 1, 0]
 [0, 0, 0, 1]
 [1, 0, 0, 1]
 [0, 1, 0, 1]
 [1, 1, 0, 1]
 [1, 0, 1, 1]
 [0, 1, 1, 1]
 [1, 1, 1, 1]

Relation with the Circuit SAT

The circuit SAT can include other boolean expression beyond CNF such as Disjunctive Normal Form (DNF). However, all the boolean expressions can be generally transformed to CNF, so the circuit SAT is "equivalent" with SAT.