What is KoSAT?

KoSAT is pure Kotlin CDCL SAT solver based on MiniSat core. It is solving boolean satisfiability problems given in DIMACS format. Solver supports incremental solving.

How to use KoSAT?

There are different ways how to use our solver:

On site

In the picture below you can see site dialog window. All you need is to enter the problem in DIMACS format and click CHECK SAT button.

The site is available at the link below:

http://www.utbot.org/kosat/

---

By Java/Kotlin

Use KoSAT directly from Kotlin. You can add it as a JitPack dependency.

To get a Git project into your build:

• Step 1. Add the JitPack repository to your build file

Add it in your root build.gradle at the end of repositories:

allprojects {
    repositories {
        ...
        maven(url = "https://jitpack.io")
    }
}

• Step 2. Add the dependency

dependencies {
    implementation("com.github.UnitTestBot.kosat:kosat:main-SNAPSHOT")
}

Now you can use KoSAT project.

Here is simple code example:

import org.kosat.Kosat

fun main() {
// Create the SAT solver:
val solver = Kosat(mutableListOf(), 0)

    // Allocate two variables:
    solver.addVariable()
    solver.addVariable()

    // Encode TIE-SHIRT problem:
    solver.addClause(-1, 2)
    solver.addClause(1, 2)
    solver.addClause(-1, -2)
    // solver.addClause(1, -2) // UNSAT with this clause

    // Solve the SAT problem:
    val result = solver.solve()
    println("result = $result")

    // Get the model:
    val model = solver.getModel()
    println("model = $model")
}

Find more about KoSAT interface here.

---

Heuristics and Features

Main features implemented in solver

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

Documentation

Our solver has a detailed documentation about everything you might need to know. It may be useful even if you are new to SAT problem.

Check this out here.

Contribution & Support ⭐

KoSAT is an open source project. If you have found any bugs or want to suggest some effective heuristics for solver, we are open for your help!

If you have any troubles while using our solver, you can contact us in telegram: @AlxVlsv, @dvrr9, @polinarria