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.
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:
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.
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.
Main features implemented in solver
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.
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