Introduction

This article dives into the world of SAT solvers, inspired by Twitter post by Vipul Vaibhaw, where he shared his implementation of a concurrent SAT solver written in Rust. You can find his original post here.
SAT solvers are great tools used in various fields, from computer science research to practical applications like hardware verification and software testing.

The neighborhood is also called hood.

What is SAT?

SAT, short for "satisfiability", refers to the problem of determining whether there exists an interpretation, that satisfies a given Boolean formula. In simpler terms, it's about figuring out if there's a way to assign truth values to a set of variables such that the entire formula evaluates to true.
A formula is written in the form:

$$(F) = (A \rightarrow (B \vee \neg C)) \wedge (\neg A \vee B \wedge C) \wedge (D \rightarrow (\neg B \vee \neg C))$$

SAT is a classic problem in computer science. It is an NP-complete problem, meaning it is computationally challenging to find a solution for a problem and there is no known efficient algorithm for solving all instances of SAT in polynomial time (some special cases can be solved in polynomial time like 2-SAT and 3-SAT).

Why should I know about it?

SAT may seem just academic and even trivial, but it has practical applications in various fields such as AI, hardware design, and software testing. Many problems can be broken down into SAT.
SAT Solvers, tackle a wide range of real-world problems that require logical decision-making with some optimizations.
For example, SAT solvers are used to verify software correctness, check the correctness of a circuit, optimize supply chains, and even task scheduling.
I'm implementing it just for fun for now🙃.

A bit of math...

Before we begin with the implementation, let's dive into a bit of Boolean algebra, to understand SAT solvers. A Boolean formula is composed of variables, operators (AND, OR, NOT), and parentheses. For instance, a simple Boolean formula might look like this:

$$F = (A ∧ (B ∨ ¬C)) ∨ (D ∧ ¬B)$$

Let's look at the mathematical definitions, we should be aware of, for a better understanding of the code later. Consider the above boolean formula for example.

Literal: A literal is either a variable or its negation. Literals are the smallest components, representing a boolean variable that can either be true or false.

In the example:

• A, B, C, and D are variables, and each one can appear as a literal in the formula.

• A, D, ¬B, and ¬C are literals.

  • A and D are positive literals (the variable itself).

  • ¬B and ¬C are negative literals (the negation of the variable).

Clause: A clause is a disjunction (OR operation) of one or more literals. Each clause is essentially a group of literals that are OR-ed together.

In the example:

• The formula F has three clauses:

  1. (A ∨ D)

  2. (A ∨ ¬B)

  3. (B ∨ ¬C ∨ D)

Each of these clauses is a disjunction of literals.

Formula: A formula is a combination of clauses connected by the logical AND (∧). In Conjunctive Normal Form (CNF), the entire formula is a conjunction (AND operation) of one or more clauses.

For example:

• The CNF version of the formula given is:
  F = (A ∨ D) ∧ (A ∨ ¬B) ∧ (B ∨ ¬C ∨ D)

Here, F is the formula, and it is composed of three clauses: (A ∨ D), (A ∨ ¬B), and (B ∨ ¬C ∨ D).

Symbol Meanings:
∧: Conjunction (and)
∨: Disjunction (or)
¬: Negation (not)
A,B,C: Boolean variables

The task of a SAT solver is to determine if there is a way to assign true (T) or false (F) values to the variables (A, B, and C) such that the entire formula evaluates to true. If such an assignment exists, the formula is said to be satisfiable; otherwise, it is unsatisfiable.

A Boolean formula is typically expressed in Conjunctive Normal Form (CNF), which is a conjunction of clauses, where each clause is a disjunction of literals. Any valid boolean formula can be converted to CNF.

Writing a concurrent SAT Solver in Go

One last bit before we begin. We'll need a way to represent the input formula, for which we saw mathematical representation in the previous section. A common method is to replace, characters with numbers, with negative numbers representing negation. So the formula in CNF form:
F = (A ∨ B ∨ C) ∧ (¬A ∨ B ∨ ¬C) ∧ (A ∨ ¬B ∨ C) can be represented as:

1,2,3
-1,2,-3
1,-2,3

Now, let's finally start with the implementation. We'll be using the DPLL (Davis-Putnam-Logemann-Loveland) algorithm in our implementation of the SAT solver. DPLL is a fundamental and one of the simplest algorithms for solving SAT problems. It employs backtracking(which most NP-complete problems use) to find a satisfying assignment of variables.

Steps in the algorithm are:

1. Unit Propagation: assigns values to variables, by checking for clauses containing only one literal.

2. Pure Literal Elimination: Removes literals that appear only in one polarity in the whole formula.

3. Decision Making: If no unit clauses or pure literals remain, we make a decision by choosing an unassigned variable. We then make two recursive calls: one with the variable assigned true and one with it assigned false.

4. Backtracking: After making a decision, DPLL recursively solves the simplified formula. If a contradiction is found (i.e., a clause is unsatisfied), the algorithm backtracks to the previous decision point and tries the opposite value for the variable.

5. Termination: The algorithm continues this process of propagation, decision-making, and backtracking until it either finds a satisfying assignment for all variables (proving the formula is satisfiable) or exhausts all possibilities in the search space(proving it is unsatisfiable).

Let's start by defining the types:

type Literal int
type Clause []Literal
type Formula []Clause

type Assignment map[Literal]bool

The unitPropagate function simplifies the formula by assigning values to variables in unit clauses (clauses with only one literal). When a unit clause is found, the literal in that clause is assigned a value, and the formula is updated accordingly. We also remove all clauses that are satisfied by the new assignment and remove the negation of the assigned literal from the remaining clauses.

func unitPropagate(formula Formula, assignment Assignment) (Formula, Assignment) {
    updatedFormula := slices.Clone(formula)
    updatedAssignment := maps.Clone(assignment)
    for {
        var unitClauses []Clause
        for _, clause := range updatedFormula {
            if len(clause) == 1 {
                unitClauses = append(unitClauses, clause)
            }
        }

        if len(unitClauses) == 0 {
            break
        }

        for _, clause := range unitClauses {
            literal := clause[0]
            absLiteral := math.Abs(float64(literal))
            updatedAssignment[Literal(absLiteral)] = literal > 0

            var filteredFormula Formula
            for _, c := range updatedFormula {
                if !slices.Contains(c, literal) {
                    filteredFormula = append(filteredFormula, c)
                }
            }

            var simplifiedFormula Formula
            for _, c := range filteredFormula {
                updatedClause := slices.Clone(c)
                if index := slices.Index(updatedClause, -literal); index >= 0 {
                    updatedClause = slices.Delete(updatedClause, index, index+1)
                }
                simplifiedFormula = append(simplifiedFormula, updatedClause)
            }
            updatedFormula = simplifiedFormula
        }
    }

    return updatedFormula, updatedAssignment
}

Next, the pureLiteralAssignment function identifies literals that appear only in one polarity (either always positive or always negative) and assigns them accordingly. This further simplifies the formula:

func pureLiteralAssignment(formula Formula, assignment Assignment) (Formula, Assignment) {
    updatedFormula := slices.Clone(formula)
    updatedAssignment := maps.Clone(assignment)

    allLiteralsSet := set.NewSet[Literal]()
    for _, clauses := range formula {
        for _, literal := range clauses {
            allLiteralsSet.Add(literal)
        }
    }

    allLiterals := allLiteralsSet.Values()
    pureLiterals := set.NewSet[Literal]()
    for _, literal := range allLiterals {
        if !slices.Contains(allLiterals, -literal) {
            pureLiterals.Add(literal)
        }
    }

    for _, literal := range pureLiterals.Values() {
        absLiteral := math.Abs(float64(literal))
        updatedAssignment[Literal(absLiteral)] = literal > 0

        var filteredFormula Formula
        for _, clause := range updatedFormula {
            if index := slices.Index(clause, literal); index == -1 {
                filteredFormula = append(filteredFormula, clause)
            }
        }
        updatedFormula = filteredFormula
    }

    return updatedFormula, updatedAssignment
}

The isSatisfied function checks if the current assignment satisfies the formula. The function iterates over each clause in the formula. For each clause, it checks if at least one literal is satisfied by the current assignment. If all clauses are satisfied, it returns true. If any clause is not satisfied, it returns false.

func isSatisfied(formula Formula, assignment Assignment) bool {
    for _, clause := range formula {
        satisfied := false
        for _, literal := range clause {
            absLiteral := math.Abs(float64(literal))
            if val, ok := assignment[Literal(absLiteral)]; ok {
                if (literal > 0 && val) || (literal < 0 && !val) {
                    satisfied = true
                    break
                }
            }
        }
        if !satisfied {
            return false
        }
    }

    return true
}

If the formula still isn't satisfied, the selectLiteral function picks a variable that hasn't been assigned a value. This unassigned variable will be used in the next decision-making step.

func selectLiteral(formula Formula, assignment Assignment) (Literal, error) {
    for _, clause := range formula {
        for _, literal := range clause {
            absLiteral := math.Abs(float64(literal))
            if _, ok := assignment[Literal(absLiteral)]; !ok {
                return literal, nil
            }
        }
    }
    return 0, errors.New("no literal found")
}

The Solve function is the main recursive function that implements the DPLL algorithm. It utilizes the functions mentioned above to iteratively simplify the formula, make decisions, and check for satisfiability. Additionally, our implementation leverages Go's concurrency features (goroutines and channels) to explore multiple branches of the search space simultaneously, with each recursion running on a separate goroutine, potentially speeding up the search for a solution.

func Solve(formula Formula, assignment Assignment) (bool, Assignment) {
    if len(formula) == 0 {
        return false, assignment
    }

    if !checkClauseValidity(formula) {
        return false, assignment
    }

    if isSatisfied(formula, assignment) {
        return true, assignment
    }

    newFormula, newAssignment := unitPropagate(formula, assignment)

    newFormula, newAssignment = pureLiteralAssignment(newFormula, newAssignment)

    if isSatisfied(newFormula, newAssignment) {
        return true, newAssignment
    }

    if !checkClauseValidity(formula) {
        return false, assignment
    }

    selectedLiteral, err := selectLiteral(newFormula, newAssignment)
    if err != nil {
        return false, assignment
    }

    var wg sync.WaitGroup
    ch := make(chan Assignment, 2)

    wg.Add(2)

    go func() {
        defer wg.Done()
        assignment1 := maps.Clone(newAssignment)
        assignment1[selectedLiteral] = true
        simplifiedFormula := simplifyFormula(newFormula, selectedLiteral)
        recursiveSolution(simplifiedFormula, assignment1, ch)
    }()

    go func() {
        defer wg.Done()
        assignment2 := maps.Clone(newAssignment)
        assignment2[selectedLiteral] = false
        simplifiedFormula := simplifyFormula(newFormula, -selectedLiteral)
        recursiveSolution(simplifiedFormula, assignment2, ch)
    }()

    go func() {
        wg.Wait()
        close(ch)
    }()

    for finalAssignment := range ch {
        if isSatisfied(formula, finalAssignment) {
            return true, finalAssignment
        }
    }

    return false, assignment
}

func recursiveSolution(formula Formula, assignment Assignment, ch chan Assignment) {
    if len(formula) == 0 {
        return
    }

    if !checkClauseValidity(formula) {
        return
    }

    if isSatisfied(formula, assignment) {
        ch <- assignment
        return
    }

    newFormula, newAssignment := unitPropagate(formula, assignment)

    newFormula, newAssignment = pureLiteralAssignment(newFormula, newAssignment)

    if isSatisfied(newFormula, newAssignment) {
        ch <- newAssignment
        return
    }

    if !checkClauseValidity(formula) {
        return
    }

    selectedLiteral, err := selectLiteral(newFormula, newAssignment)
    if err != nil {
        return
    }

    var wg sync.WaitGroup
    subCh := make(chan Assignment, 2)

    wg.Add(2)

    go func() {
        defer wg.Done()
        assignment1 := maps.Clone(newAssignment)
        assignment1[selectedLiteral] = true
        simplifiedFormula := simplifyFormula(newFormula, selectedLiteral)
        recursiveSolution(simplifiedFormula, assignment1, subCh)
    }()

    go func() {
        defer wg.Done()
        assignment2 := maps.Clone(newAssignment)
        assignment2[selectedLiteral] = false
        simplifiedFormula := simplifyFormula(newFormula, -selectedLiteral)
        recursiveSolution(simplifiedFormula, assignment2, subCh)
    }()

    go func() {
        wg.Wait()
        close(subCh)
    }()

    for finalAssignment := range subCh {
        if isSatisfied(formula, finalAssignment) {
            ch <- finalAssignment
            return
        }
    }
}

The complete code can be found in the GitHub repo below:

Outro

In this article, we implemented a concurrent SAT solver in Go, utilizing the DPLL algorithm and Go's concurrency primitives to explore the search space in parallel. The process was straightforward, and I'm eager to dive deeper, with plans to explore CDCL in Go in the future.