UnitTestBot/kosat

Pure Kotlin CDCL SAT solver http://www.utbot.org/kosat/

Download

Step 1. Add the JitPack repository to your build file

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

	dependencyResolutionManagement {
		repositoriesMode.set(RepositoriesMode.FAIL_ON_PROJECT_REPOS)
		repositories {
			mavenCentral()
			maven { url 'https://jitpack.io' }
		}
	}

Add it in your settings.gradle.kts at the end of repositories:

	dependencyResolutionManagement {
		repositoriesMode.set(RepositoriesMode.FAIL_ON_PROJECT_REPOS)
		repositories {
			mavenCentral()
			maven { url = uri("https://jitpack.io") }
		}
	}

Add to pom.xml

	<repositories>
		<repository>
		    <id>jitpack.io</id>
		    <url>https://jitpack.io</url>
		</repository>
	</repositories>

Add it in your build.sbt at the end of resolvers:

 
    resolvers += "jitpack" at "https://jitpack.io"

Add it in your project.clj at the end of repositories:

 
    :repositories [["jitpack" "https://jitpack.io"]]

Step 2. Add the dependency

	dependencies {
		implementation 'com.github.UnitTestBot:kosat:'
	}

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

	<dependency>
	    <groupId>com.github.UnitTestBot</groupId>
	    <artifactId>kosat</artifactId>
	    <version></version>
	</dependency>


                            
    libraryDependencies += "com.github.UnitTestBot" % "kosat" % ""


                            
    :dependencies [[com.github.UnitTestBot/kosat ""]]

Readme

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:

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/

</details> <details> <summary>By Java/Kotlin</summary> <br/>

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.

</details>

Heuristics and Features

<details> <summary>Main features implemented in solver</summary> <br/>

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