Logical NOT

$$y=\text{Not}(x)=\{\begin{array}{ll}1,& \mathrm{\neg }x\\ \\ 0,& x\end{array}$$

Discrete Case

Constants

$$m=max(x)$$

Additional Variables

$y^{\prime }\in \{0,1\}$: Logical value indicating the polynomial is false.

Derived Symbol

$$y=y^{\prime }$$

Mathematical Model

$$\begin{array}{rlrl}\text{s.t.}& m\cdot (1-y^{\prime })& \ge & x\\ \\ & 1-y^{\prime }& \le & x\end{array}$$

That is:

$$y=\{\begin{array}{ll}1,& x=0\\ \\ 0,& x\ge 1\end{array}$$

Continuous (Non-Precise) Case

Constants

$$m=max(x)$$

Additional Variables

$b\in [0,1]$: Normalized value of the polynomial.

$y^{\prime }\in \{0,1\}$: Logical value indicating the polynomial is false.

Derived Symbol

$$y=y^{\prime }$$

Mathematical Model

$$\begin{array}{rlrl}\text{s.t.}& x& =& m\cdot b\\ \\ & 1-y^{\prime }& \ge & b\\ \\ & ϵ\cdot (1-y^{\prime })& \le & b\end{array}$$

That is:

$$y=\{\begin{array}{ll}1,& x=0\\ \\ 0,& x\ge ϵ\end{array}$$

Continuous (Precise) Case

Derived Symbol

$$y=\text{Ulp}(x)$$

$\text{Ulp}(x)$ can refer to Unit Linear Piecewise Function, using the sampling points $\{(0,1),(p-ϵ,1),(p,0),(max(x),0)\}$.

That is:

$$y=\{\begin{array}{ll}1,& 0\le x<p\\ \\ 0,& x\ge p\end{array}$$

Code Example

Discrete Case

kotlin

import kotlinx.coroutines.*
import fuookami.ospf.kotlin.utils.math.*
import fuookami.ospf.kotlin.core.frontend.variable.*
import fuookami.ospf.kotlin.core.frontend.expression.polynomial.*
import fuookami.ospf.kotlin.core.frontend.expression.symbol.linear_function.*
import fuookami.ospf.kotlin.core.frontend.inequality.*
import fuookami.ospf.kotlin.core.frontend.model.mechanism.*
import fuookami.ospf.kotlin.core.backend.plugins.scip.*

val x = BinVar("x")
val not = NotFunction(x, name = "not")
val solver = ScipLinearSolver()

val model1 = LinearMetaModel()
model1.add(x)
model1.add(not)
model1.addConstraint(not)
model1.maximize(x)
val result1 = runBlocking { solver(model1) }
assert(result1.value!!.obj eq Flt64.zero)

val model2 = LinearMetaModel()
model2.add(x)
model2.add(not)
model2.addConstraint(!not)
model2.minimize(x)
val result2 = runBlocking { solver(model2) }
assert(result2.value!!.obj eq Flt64.one)

Continuous Case

kotlin

import kotlinx.coroutines.*
import fuookami.ospf.kotlin.utils.math.*
import fuookami.ospf.kotlin.core.frontend.variable.*
import fuookami.ospf.kotlin.core.frontend.expression.polynomial.*
import fuookami.ospf.kotlin.core.frontend.expression.symbol.linear_function.*
import fuookami.ospf.kotlin.core.frontend.inequality.*
import fuookami.ospf.kotlin.core.frontend.model.mechanism.*
import fuookami.ospf.kotlin.core.backend.plugins.scip.*

val x = URealVar("x")
x.range.leq(Flt64.one)
val not = NotFunction(x, name = "not")
val solver = ScipLinearSolver()

val model1 = LinearMetaModel()
model1.add(x)
model1.add(not)
model1.addConstraint(not)
model1.maximize(x)
val result1 = runBlocking { solver(model1) }
assert(result1.value!!.obj eq Flt64.zero)

val model2 = LinearMetaModel()
model2.add(x)
model2.add(not)
model2.addConstraint(!not)
model2.minimize(x)
val result2 = runBlocking { solver(model2) }
assert(result2.value!!.obj geq Flt64(1e-6))

Complete Implementation Reference:

• Kotlin

Complete Example Reference:

• Kotlin