docs.md

Brand new SAT-solver using Kotlin

If you don't know any word in documentation, you can try to find it in Glossary with main terms used here.

KoSAT is solving problems given in DIMACS format. If you don't know how it looks like, you can find it here.

KoSAT heuristics and features

1. ReNumeration
2. Trail
3. Conflict analysis
4. Backjump
5. Propagation
6. 2-watched literals
7. VSIDS
8. Luby restarts
9. Polarity choice
10. ReduceDB based on LBD
11. Incremental solving

Interface

If you want to use KoSAT solver in your kotlin project, you can find more about its interface here

About CDCL

Conflict-driven clause learning (CDCL) is an algorithm for solving the Boolean satisfiability problem (SAT). It underlies almost all SAT solvers, so it's important to know its structure.

This is what a simple CDCL algorithm looks like:

while (true) {  
    propagate() // propagation of unit clauses
    if (conflict) {
        // Conflict
        if (topLevelConflict) {
            return Unsatisfiable
        }
        val lemma = analyze(conflictClause) // analyze conflict and learn a new clause
        backjump(lemma) // undo assignments until new clause is unit
    } else {
        // No conflict
        if (allVariablesAssigned) {
            return Satisfiable
        }
        pickNewBranchingLiteral()
    }
}

As you can see, the algorithm's main idea is to make partial assignments and learn information if something goes wrong. So if we get a conflict, we try to analyze it and learn new clause, based on this conflict. If all variables are assigned, and there is no conflict, this means we have found a solution.

Code structure

Storing data

All variables are stored in the vars array. It means they have some useful characteristics:

• value (TRUE, FALSE, UNDEFINED)
• reason (clause it was concluded from, if it's not a decision variable)
• level (decision level when variable was assigned)

Trail is used for decision literals and propagations. You can find more information about it here.

Clauses are stored in 2 arrays: constraints and learnts.

• Constraints array is used for clauses given in initial problem and doesn't change during solution.
• Learnts array is used for clauses learned during the process of partial assignment. This array can be modified many times, and sometimes its size can be rather big to prove problem has no solution.

Note: we don't keep clauses of size 1, as they are stored on trail 0-level.

More about basics of CDCL

Let's go through all functions mentioned in simple implementation:

1. propagate() — This function is important for making decisions based on current partial assignment. In details, it adds literals on trail, i.e. values of variables which follows from assignment

2. If propagate() got a conflict, we check whether level equals to 0 - this means that conflict follows from initial task, i.e. problem is UNSAT. Otherwise, we run analyze() function with a conflict clause to construct a new clause (called lemma).

3. backjump() is used to return to level where lemma would be unit clause (it's possible because we've constructed lemma in this way).

4. If there is no conflict, we need to check if all variables are assigned. In this case, problem is SAT, and we have a solution. Otherwise, we continue making decisions. That's why we need pickNewBranchingLiteral().