Rewrite BDD internals. Add PHP example

Author: Lipen

README.adoc

@@ -19,10 +19,11 @@ image:https://hitsofcode.com/github/Lipen/kotlin-bdd["Hits-of-Code",link="https:
 :link-lib-bdd: https://github.com/sybila/biodivine-lib-bdd[lib-bdd]
 :link-sylvan: https://github.com/trolando/sylvan[Sylvan]
 :link-adiar: https://github.com/SSoelvsten/adiar[Adiar]
+:link-kobdd: https://github.com/korifey/kobdd[kobdd]
 
 `kotlin-bdd` was heavily inspired by {link-cudd} (C/C++), {link-dd} (Python) and {link-lib-bdd} (Rust).
 
-CAUTION: `kotlin-bdd` is currently a purely educational project and may not be as feature-complete and/or performant as full-fledged BDD packages such as {link-cudd}, {link-sylvan}, {link-adiar}.
+CAUTION: `kotlin-bdd` is currently a purely educational project and may not be as feature-complete and/or performant as full-fledged BDD packages such as {link-cudd}, {link-sylvan}, {link-adiar}, {link-kobdd}.
 
 == Installation
 
@@ -44,9 +45,18 @@ dependencies {
 // TODO
 ----
 
+== Run examples
+
+=== PHP
+
+----
+gw :examples:shadowJar
+java -cp examples/build/libs/examples.jar com.github.lipen.bdd.PHPKt
+----
+
 '''
 
-=== Bibliography
+== Bibliography
 
 - R. E. Bryant.
 *"Graph-Based Algorithms for Boolean Function Manipulation,"* 1986. link:https://doi.org/10.1109/TC.1986.1676819[DOI].

build.gradle.kts

@@ -5,6 +5,7 @@ group = "com.github.Lipen"
 plugins {
     kotlin("jvm") version "1.6.0"
     application
+    id("com.github.johnrengelman.shadow") version "7.1.0" apply false
     id("fr.brouillard.oss.gradle.jgitver") version "0.9.1"
     id("com.github.ben-manes.versions") version "0.39.0"
     `maven-publish`
@@ -18,10 +19,11 @@ dependencies {
     implementation(platform(kotlin("bom")))
     implementation(kotlin("stdlib-jdk8"))
 
-    implementation("io.github.microutils:kotlin-logging:2.1.0")
-    runtimeOnly("ch.qos.logback:logback-classic:1.2.3")
+    implementation("io.github.microutils:kotlin-logging:2.1.15")
+    runtimeOnly("ch.qos.logback:logback-classic:1.2.7")
 
     testImplementation(kotlin("test"))
+    testImplementation("com.soywiz.korlibs.klock:klock-jvm:2.4.8")
 }
 
 tasks.test {

examples/build.gradle.kts

@@ -0,0 +1,32 @@
+import com.github.jengelman.gradle.plugins.shadow.tasks.ShadowJar
+import org.jetbrains.kotlin.gradle.tasks.KotlinCompile
+
+plugins {
+    kotlin("jvm")
+    id("com.github.johnrengelman.shadow")
+}
+
+repositories {
+    mavenCentral()
+}
+
+dependencies {
+    implementation(platform(kotlin("bom")))
+    implementation(kotlin("stdlib-jdk8"))
+
+    implementation(rootProject)
+    implementation("io.github.microutils:kotlin-logging:2.1.15")
+    runtimeOnly("ch.qos.logback:logback-classic:1.2.7")
+    implementation("com.soywiz.korlibs.klock:klock-jvm:2.4.8")
+    implementation("com.squareup.okio:okio:3.0.0")
+}
+
+tasks.withType<KotlinCompile> {
+    kotlinOptions.jvmTarget = "1.8"
+}
+
+tasks.withType<ShadowJar> {
+    archiveBaseName.set(project.name)
+    archiveClassifier.set("")
+    archiveVersion.set("")
+}

examples/src/main/kotlin/com/github/lipen/bdd/PHP.kt

@@ -0,0 +1,124 @@
+package com.github.lipen.bdd
+
+import com.soywiz.klock.PerformanceCounter
+import com.soywiz.klock.measureTime
+import okio.buffer
+import okio.sink
+import java.io.File
+
+private fun generatePhpClausesA(pigeons: Int, holes: Int): Sequence<List<Int>> = sequence {
+    fun v(i: Int, j: Int) = (i - 1) * holes + j
+
+    // A: p clauses
+    for (i in 1..pigeons)
+        yield((1..holes).map { j -> v(i, j) })
+}
+
+private fun generatePhpClausesBj(pigeons: Int, holes: Int, j: Int): Sequence<List<Int>> = sequence {
+    fun v(i: Int, j: Int) = (i - 1) * holes + j
+
+    // B[j] clauses
+    for (i in 1..pigeons) //(p-1) * p / 2
+        for (k in i + 1..pigeons)
+            yield(listOf(-v(i, j), -v(k, j)))
+}
+
+private fun generatePhpClausesB(pigeons: Int, holes: Int): Sequence<List<Int>> = sequence {
+    // B clauses
+    for (j in 1..holes) //h *
+        yieldAll(generatePhpClausesBj(pigeons, holes, j))
+}
+
+private fun generatePhpClauses(pigeons: Int, holes: Int): Sequence<List<Int>> = sequence {
+    require(pigeons > 0)
+    require(holes > 0)
+    // A: p clauses
+    yieldAll(generatePhpClausesA(pigeons, holes))
+    // B clauses
+    yieldAll(generatePhpClausesB(pigeons, holes))
+}
+
+fun php(pigeons: Int, holes: Int = pigeons - 1) {
+    require(pigeons > 0)
+    require(holes > 0)
+
+    println("Running PHP(p = $pigeons, h = $holes})...")
+
+    val timeStart = PerformanceCounter.reference
+    val bdd = BDD()
+    var f = bdd.one
+    var totaltime = 0.0
+
+    fun v(i: Int, j: Int) = (i - 1) * holes + j
+
+    println("Generating and adding PHP clauses...")
+    val file = File("data-php-${pigeons}.txt")
+    println("Writing data to: '$file'")
+    file.sink().buffer().use {
+        with(it) {
+            writeUtf8("step name BDD.size f.size steptime totaltime hits misses\n")
+
+            var count = 0
+
+            fun step(name: String, init: () -> Unit) {
+                val steptime = measureTime {
+                    init()
+                    if ((count + 1) % 50 == 0) {
+                        bdd.collectGarbage(listOf(f))
+                    }
+                }
+                val fsize = bdd.descendants(f).size
+                println(
+                    "Step #${count + 1} ($name) in %.3fs, BDD.size = ${bdd.size} (real size = ${bdd.realSize()}), f (size=$fsize) = $f, hits = ${bdd.cacheHits}, misses = ${bdd.cacheMisses}"
+                        .format(steptime.seconds)
+                )
+                totaltime += steptime.seconds
+                val nameSafe = name.replace(" ", "_")
+                writeUtf8(
+                    "${count + 1} $nameSafe ${bdd.realSize()} $fsize %.3f %.3f ${bdd.cacheHits} ${bdd.cacheMisses}\n"
+                        .format(steptime.seconds, totaltime)
+                )
+                count++
+            }
+
+            for (clause in generatePhpClausesA(pigeons, holes)) {
+                step("JoinA") {
+                    val c = bdd.clause(clause)
+                    f = bdd.applyAnd(f, c)
+                }
+            }
+
+            for (j in 1..holes) {
+                for (clause in generatePhpClausesBj(pigeons, holes, j)) {
+                    step("JoinB") {
+                        val c = bdd.clause(clause)
+                        f = bdd.applyAnd(f, c)
+                    }
+                }
+                if (j < holes) {
+                    for (i in 1..pigeons) {
+                        step("Proj") {
+                            f = bdd.exists(f, v(i, j))
+                        }
+                    }
+                }
+            }
+        }
+    }
+
+    println("final f = $f")
+    check(bdd.isZero(f)) {
+        "Formula must be Zero (UNSAT) after adding all PHP clauses"
+    }
+    val totalTime = PerformanceCounter.reference - timeStart
+    println("PHP($pigeons, $holes) done in %.2fs (totaltime=%.2f)".format(totalTime.seconds, totaltime))
+}
+
+fun main(args: Array<String>) {
+    val pigeons = if (args.isNotEmpty()) {
+        args[0].toInt()
+    } else {
+        10 // default
+    }
+    php(pigeons = pigeons)
+}

settings.gradle.kts

@@ -1 +1,3 @@
 rootProject.name = "kotlin-bdd"
+
+include("examples")

src/main/kotlin/com/github/lipen/bdd/BDD.kt

@@ -0,0 +1,23 @@
+@file:Suppress("FunctionName")
+
+package com.github.lipen.bdd
+
+import kotlin.math.absoluteValue
+
+fun BDD.clause(literals: Iterable<Int>): Int {
+    // TODO: check uniqueness and consistency
+    var current = zero
+    for (lit in literals.sortedByDescending { it.absoluteValue }) {
+        val x = variable(lit)
+        current = applyOr(current, x)
+    }
+    return current
+}
+
+fun BDD.clause_(literals: IntArray): Int {
+    return clause(literals.asList())
+}
+
+fun BDD.clause(vararg literals: Int): Int {
+    return clause_(literals)
+}

src/main/kotlin/com/github/lipen/bdd/Op.kt

@@ -5,7 +5,7 @@
         </encoder>
     </appender>
 
-    <root level="debug">
+    <root level="info">
         <appender-ref ref="STDOUT"/>
     </root>
 </configuration>