diff --git a/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/AbstractInferCommand.kt b/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/AbstractInferCommand.kt index c046cc79..bec96153 100644 --- a/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/AbstractInferCommand.kt +++ b/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/AbstractInferCommand.kt @@ -24,6 +24,8 @@ abstract class AbstractInferCommand(name: String) : CliktCo with(extraOptions) { Globals.EPSILON_OUTPUT_EVENTS = epsilonOutputEvents Globals.START_STATE_ALGORITHMS = startStateAlgorithms + Globals.FIXED_OUTPUT_DECOMPOSITION = fixedOutputDecomposition + Globals.FIXED_ACTIVITY = fixedActivity Globals.IS_FORBID_OR = isForbidOr Globals.IS_FORBID_TRANSITIONS_TO_FIRST_STATE = isForbidTransitionsToFirstState Globals.IS_BFS_AUTOMATON = isBfsAutomaton @@ -42,7 +44,10 @@ abstract class AbstractInferCommand(name: String) : CliktCo Globals.IS_ENCODE_TRANSITION_FUNCTION = isEncodeTransitionFunction Globals.IS_ENCODE_EPSILON_PASSIVE = isEncodeEpsilonPassive Globals.IS_ENCODE_NOT_EPSILON_ACTIVE = isEncodeNotEpsilonActive + Globals.IS_ENCODE_CONJUNCTIVE_GUARDS = isEncodeConjunctiveGuards + Globals.IS_ENCODE_CARDINALITY_CKA = isEncodeCardinalityCKA Globals.IS_FIX_ACTIVE = isFixActive + Globals.IS_FIX_OUTPUT_DECOMPOSITION = isFixOutputDecomposition Globals.IS_REUSE_K = isReuseK Globals.IS_USE_ASSUMPTIONS = isUseAssumptions Globals.IS_RENDER_WITH_DOT = isRenderWithDot diff --git a/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/modular/parallel/AbstractInferParallelModularCommand.kt b/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/modular/parallel/AbstractInferParallelModularCommand.kt index 7ba04292..763f0bfd 100644 --- a/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/modular/parallel/AbstractInferParallelModularCommand.kt +++ b/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/modular/parallel/AbstractInferParallelModularCommand.kt @@ -16,14 +16,16 @@ abstract class AbstractInferParallelModularCommand(name: String) : } else { logger.info("Inferred parallel modular automaton consists of ${automaton.modules.shape.single()} modules:") for ((m, module) in automaton.modules.values.withIndex(start = 1)) { - logger.info("Module #$m (${module.getStats()}):") + logger.info("Module #$m (${module.getStats()}, vars = ${automaton.moduleOutputVariables[m]}):") module.pprint() } + logger.info("Output decomposition: ${automaton.outputVariableModule.values}") + for (m in 1..automaton.M) { + logger.info(" m = $m: ${automaton.moduleOutputVariables[m]}") + } logger.info("Inferred parallel modular automaton has:") automaton.printStats() - // TODO: print controlled variables of each module - // TODO: automaton.dump(outDir) if (automaton.verify(scenarioTree.toOld())) diff --git a/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/modular/parallel/InferParallelModularBasicMin.kt b/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/modular/parallel/InferParallelModularBasicMin.kt index dd2f5a8c..b784c67d 100644 --- a/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/modular/parallel/InferParallelModularBasicMin.kt +++ b/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/modular/parallel/InferParallelModularBasicMin.kt @@ -11,6 +11,7 @@ import ru.ifmo.fbsat.cli.command.infer.options.INPUT_OUTPUT_OPTIONS import ru.ifmo.fbsat.cli.command.infer.options.SolverOptions import ru.ifmo.fbsat.cli.command.infer.options.getInitialOutputValuesOption import ru.ifmo.fbsat.cli.command.infer.options.inputNamesOption +import ru.ifmo.fbsat.cli.command.infer.options.maxOutgoingTransitionsOption import ru.ifmo.fbsat.cli.command.infer.options.numberOfModulesOption import ru.ifmo.fbsat.cli.command.infer.options.numberOfStatesOption import ru.ifmo.fbsat.cli.command.infer.options.outDirOption @@ -32,6 +33,7 @@ private class ParallelModularBasicMinInputOutputOptions : OptionGroup(INPUT_OUTP private class ParallelModularBasicMinAutomatonOptions : OptionGroup(AUTOMATON_OPTIONS) { val numberOfModules: Int by numberOfModulesOption().required() val numberOfStates: Int? by numberOfStatesOption() + val maxOutgoingTransitions: Int? by maxOutgoingTransitionsOption() } class InferParallelModularBasicMinCommand : @@ -51,6 +53,7 @@ class InferParallelModularBasicMinCommand : inferrer.parallelModularBasicMin( scenarioTree = scenarioTree, numberOfModules = params.numberOfModules, - numberOfStates = params.numberOfStates + numberOfStates = params.numberOfStates, + maxOutgoingTransitionsForC = { params.maxOutgoingTransitions ?: it } ) } diff --git a/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/modular/parallel/InferParallelModularBasicMinC.kt b/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/modular/parallel/InferParallelModularBasicMinC.kt index 75deb7c6..3729d4c3 100644 --- a/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/modular/parallel/InferParallelModularBasicMinC.kt +++ b/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/modular/parallel/InferParallelModularBasicMinC.kt @@ -13,6 +13,7 @@ import ru.ifmo.fbsat.cli.command.infer.options.SolverOptions import ru.ifmo.fbsat.cli.command.infer.options.endNumberOfStatesOption import ru.ifmo.fbsat.cli.command.infer.options.getInitialOutputValuesOption import ru.ifmo.fbsat.cli.command.infer.options.inputNamesOption +import ru.ifmo.fbsat.cli.command.infer.options.maxOutgoingTransitionsOption import ru.ifmo.fbsat.cli.command.infer.options.numberOfModulesOption import ru.ifmo.fbsat.cli.command.infer.options.outDirOption import ru.ifmo.fbsat.cli.command.infer.options.outputNamesOption @@ -35,6 +36,7 @@ private class ParallelModularBasicMinCAutomatonOptions : OptionGroup(AUTOMATON_O val numberOfModules: Int by numberOfModulesOption().required() val startNumberOfStates: Int by startNumberOfStatesOption().default(1) val endNumberOfStates: Int by endNumberOfStatesOption().default(20) + val maxOutgoingTransitions: Int? by maxOutgoingTransitionsOption() } class InferParallelModularBasicMinCCommand : @@ -55,6 +57,7 @@ class InferParallelModularBasicMinCCommand : scenarioTree = scenarioTree, numberOfModules = params.numberOfModules, start = params.startNumberOfStates, - end = params.endNumberOfStates + end = params.endNumberOfStates, + maxOutgoingTransitionsForC = { params.maxOutgoingTransitions ?: it } ) } diff --git a/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/options/ExtraOptions.kt b/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/options/ExtraOptions.kt index 3ea3ab38..9de10d80 100644 --- a/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/options/ExtraOptions.kt +++ b/fbsat-cli/src/main/kotlin/ru/ifmo/fbsat/cli/command/infer/options/ExtraOptions.kt @@ -24,6 +24,8 @@ class ExtraOptions : OptionGroup(EXTRA_OPTIONS) { val isBfsGuard: Boolean by isBfsGuardOption() val epsilonOutputEvents: EpsilonOutputEvents by getEpsilonOutputEventsOption() val startStateAlgorithms: StartStateAlgorithms by getStartStateAlgorithmsOption() + val fixedOutputDecomposition: List? by getFixedOutputDecompositionOption() + val fixedActivity: List? by getFixedActivityOption() val isEncodeReverseImplication: Boolean by isEncodeReverseImplicationOption() val isEncodeTransitionsOrder: Boolean by isEncodeTransitionsOrderOption() val isEncodeTerminalsOrder: Boolean by isEncodeTerminalsOrderOption() @@ -38,7 +40,10 @@ class ExtraOptions : OptionGroup(EXTRA_OPTIONS) { val isEncodeTransitionFunction: Boolean by isEncodeTransitionFunctionOption() val isEncodeEpsilonPassive: Boolean by isEncodeEpsilonPassiveOption() val isEncodeNotEpsilonActive: Boolean by isEncodeNotEpsilonActiveOption() + val isEncodeConjunctiveGuards: Boolean by isEncodeConjunctiveGuardsOption() + val isEncodeCardinalityCKA: Boolean by isEncodeCardinalityCKAOption() val isFixActive: Boolean by isFixActiveOption() + val isFixOutputDecomposition: Boolean by isFixOutputDecompositionOption() val isReuseK: Boolean by isReuseKOption() val isUseAssumptions: Boolean by isUseAssumptionsOption() val isRenderWithDot: Boolean by isRenderWithDotOption() @@ -118,6 +123,28 @@ fun ParameterHolder.getStartStateAlgorithmsOption() = Globals.START_STATE_ALGORITHMS ) +fun ParameterHolder.getFixedOutputDecompositionOption() = + option( + "--fixed-output-decomposition", + help = "[modular-parallel] Comma-separated modules (1-based), controlling output variables" + ).convert { + require(it.isNotBlank()) { "string should not be blank" } + it.split(",").map { s -> + s.trim().toInt() + } + } + +fun ParameterHolder.getFixedActivityOption() = + option( + "--fixed-activity", + help = "[modular-parallel] Comma-separated values (boolean) of activity of scenario tree elements" + ).convert { + require(it.isNotBlank()) { "string should not be blank" } + it.split(",").map { s -> + s.trim().toBoolean() + } + } + fun ParameterHolder.isEncodeReverseImplicationOption() = option( "--encode-reverse-implication", @@ -244,6 +271,24 @@ fun ParameterHolder.isEncodeNotEpsilonActiveOption() = default = Globals.IS_ENCODE_NOT_EPSILON_ACTIVE ) +fun ParameterHolder.isEncodeConjunctiveGuardsOption() = + option( + "--encode-conjunctive-guards", + help = "Encode conjunctive guards" + ).flag( + "--no-encode-conjunctive-guards", + default = Globals.IS_ENCODE_CONJUNCTIVE_GUARDS + ) + +fun ParameterHolder.isEncodeCardinalityCKAOption() = + option( + "--encode-cardinality-CKA", + help = "Encode cardinalityCKA (just declare, but not use)" + ).flag( + "--no-encode-cardinality-CKA", + default = Globals.IS_ENCODE_CARDINALITY_CKA + ) + fun ParameterHolder.isFixActiveOption() = option( "--fix-active", @@ -253,6 +298,15 @@ fun ParameterHolder.isFixActiveOption() = default = Globals.IS_FIX_ACTIVE ) +fun ParameterHolder.isFixOutputDecompositionOption() = + option( + "--fix-output-decomposition", + help = "Fix moduleControllingOutputVariable after modular-parallel-basic-minC" + ).flag( + "--no-fix-output-decomposition", + default = Globals.IS_FIX_OUTPUT_DECOMPOSITION + ) + fun ParameterHolder.isReuseKOption() = option( "--reuse-k", diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/Automaton.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/Automaton.kt index abd0b04c..762f2c84 100644 --- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/Automaton.kt +++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/Automaton.kt @@ -11,6 +11,7 @@ import com.soywiz.klock.DateTime import kotlinx.serialization.Serializable import org.redundent.kotlin.xml.xml import ru.ifmo.fbsat.core.automaton.guard.BooleanExpressionGuard +import ru.ifmo.fbsat.core.automaton.guard.ConjunctiveGuard import ru.ifmo.fbsat.core.automaton.guard.Guard import ru.ifmo.fbsat.core.automaton.guard.NodeType import ru.ifmo.fbsat.core.automaton.guard.TruthTableGuard @@ -24,6 +25,7 @@ import ru.ifmo.fbsat.core.scenario.Scenario import ru.ifmo.fbsat.core.scenario.inputActionsSeq import ru.ifmo.fbsat.core.scenario.negative.NegativeScenario import ru.ifmo.fbsat.core.scenario.negative.OldNegativeScenarioTree +import ru.ifmo.fbsat.core.scenario.outputValues import ru.ifmo.fbsat.core.scenario.positive.OldPositiveScenarioTree import ru.ifmo.fbsat.core.scenario.positive.PositiveScenario import ru.ifmo.fbsat.core.scenario.positive.PositiveScenarioTree @@ -331,8 +333,10 @@ class Automaton( out@ for ((i, result) in eval(scenario).withIndex()) { val element = scenario.elements[i] if (result.outputAction != element.outputAction) { - // logger.error("No mapping for ${i + 1}-th element = $element, result = $result") - break@out + if (!Globals.IS_ENCODE_EVENTLESS || result.outputAction.values != element.outputValues) { + logger.error("No mapping for ${i + 1}-th element = $element, result = $result") + break@out + } } mapping[i] = result } @@ -530,11 +534,12 @@ class Automaton( fun getStats(): String { return "" + - "C = $numberOfStates, " + - "K = $maxOutgoingTransitions, " + - "P = $maxGuardSize, " + - "T = $numberOfTransitions, " + - "N = $totalGuardsSize" + "C = $numberOfStates" + + ", K = $maxOutgoingTransitions" + + ", P = $maxGuardSize" + + ", T = $numberOfTransitions" + + ", N = $totalGuardsSize" + + ", A = ${getA()}}" } fun printStats() { @@ -838,6 +843,7 @@ fun buildBasicAutomaton( val scenarioTree: PositiveScenarioTree = context["scenarioTree"] val C: Int = context["C"] val K: Int = context["K"] + val X: Int = context["X"] val Z: Int = context["Z"] val transitionDestination = context.convertIntVarArray("transitionDestination", model) val transitionInputEvent = context.convertIntVarArray("transitionInputEvent", model) @@ -855,6 +861,14 @@ fun buildBasicAutomaton( { true } } + // Only available if (Globals.IS_ENCODE_CONJUNCTIVE_GUARDS) + val inputVariableUsed by lazy { + context.convertBoolVarArray("inputVariableUsed", model) + } + val inputVariableLiteral by lazy { + context.convertBoolVarArray("inputVariableLiteral", model) + } + return Automaton( scenarioTree = scenarioTree, initialOutputValues = initialOutputValues @@ -879,15 +893,24 @@ fun buildBasicAutomaton( scenarioTree.inputEvents[transitionInputEvent[c, k] - 1] }, transitionGuard = { c, k -> - TruthTableGuard( - truthTable = scenarioTree.uniqueInputs - .withIndex(start = 1) - .associate { (u, input) -> - input to transitionTruthTable[c, k, u] - } - // inputNames = scenarioTree.inputNames, - // uniqueInputs = scenarioTree.uniqueInputs - ) + if (Globals.IS_ENCODE_CONJUNCTIVE_GUARDS) { + ConjunctiveGuard( + literals = (1..X) + .filter { x -> inputVariableUsed[x] } + .map { x -> if (inputVariableLiteral[c, k, x]) x else -x }, + inputNames = scenarioTree.inputNames + ) + } else { + TruthTableGuard( + truthTable = scenarioTree.uniqueInputs + .withIndex(start = 1) + .associate { (u, input) -> + input to transitionTruthTable[c, k, u] + } + // inputNames = scenarioTree.inputNames, + // uniqueInputs = scenarioTree.uniqueInputs + ) + } } ) } @@ -962,3 +985,17 @@ fun buildExtendedAutomaton( } ) } + +fun Automaton.getA(): Int? { + return (transitions.first().guard as? ConjunctiveGuard)?.literals?.size +} + +fun Automaton.getTA(): Int? { + var sum = 0 + for (t in transitions) { + val g = t.guard as? ConjunctiveGuard ?: return null + val a = g.literals.size + sum += a + } + return sum +} diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/ParallelModularAutomaton.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/ParallelModularAutomaton.kt index 7ee6bd27..2db0dd4e 100644 --- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/ParallelModularAutomaton.kt +++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/ParallelModularAutomaton.kt @@ -11,6 +11,7 @@ import com.github.lipen.satlib.core.Model import com.soywiz.klock.DateTime import org.redundent.kotlin.xml.xml import ru.ifmo.fbsat.core.automaton.guard.BooleanExpressionGuard +import ru.ifmo.fbsat.core.automaton.guard.ConjunctiveGuard import ru.ifmo.fbsat.core.automaton.guard.NodeType import ru.ifmo.fbsat.core.automaton.guard.TruthTableGuard import ru.ifmo.fbsat.core.scenario.InputEvent @@ -18,6 +19,7 @@ import ru.ifmo.fbsat.core.scenario.OutputAction import ru.ifmo.fbsat.core.scenario.OutputEvent import ru.ifmo.fbsat.core.scenario.OutputValues import ru.ifmo.fbsat.core.scenario.Scenario +import ru.ifmo.fbsat.core.scenario.outputValues import ru.ifmo.fbsat.core.scenario.positive.OldPositiveScenarioTree import ru.ifmo.fbsat.core.scenario.positive.PositiveScenario import ru.ifmo.fbsat.core.scenario.positive.PositiveScenarioTree @@ -59,6 +61,7 @@ class ParallelModularAutomaton( val numberOfStates: Int = modules.values.sumOf { it.numberOfStates } val numberOfTransitions: Int = modules.values.sumOf { it.numberOfTransitions } val totalGuardsSize: Int = modules.values.sumOf { it.totalGuardsSize } +// val numberOfActiveVertices = sumOf {it.active} init { require(modules.values.all { it.inputEvents == inputEvents }) @@ -107,10 +110,18 @@ class ParallelModularAutomaton( check(result.values.mapNotNull { it.outputAction.event }.all { it == outputEvent }) val outputValues = gather(MultiArray.new(M) { (m) -> result[m].outputAction.values }) - if (OutputAction(outputEvent, outputValues) == element.outputAction) { - results[j] = result + if (Globals.IS_ENCODE_EVENTLESS) { + if (outputValues == element.outputValues) { + results[j] = result + } else { + break + } } else { - break + if (OutputAction(outputEvent, outputValues) == element.outputAction) { + results[j] = result + } else { + break + } } for (m in 1..M) { @@ -152,12 +163,33 @@ class ParallelModularAutomaton( } fun getStats(): String { - return "M = $numberOfModules, " + - "C = ${modules.values.joinToString("+") { it.numberOfStates.toString() }} = $numberOfStates, " + - "K = ${modules.values.map { it.maxOutgoingTransitions }}, " + - "P = ${modules.values.map { it.maxGuardSize }}, " + - "T = ${modules.values.joinToString("+") { it.numberOfTransitions.toString() }} = $numberOfTransitions, " + - "N = ${modules.values.joinToString("+") { it.totalGuardsSize.toString() }} = $totalGuardsSize" + return "M = $numberOfModules" + + ", C = ${ + modules.values.joinToString("+") { + it.numberOfStates.toString() + } + } = $numberOfStates" + + ", K = ${ + modules.values.map { it.maxOutgoingTransitions } + }" + + ", P = ${ + modules.values.map { it.maxGuardSize } + }" + + ", T = ${ + modules.values.joinToString("+") { + it.numberOfTransitions.toString() + } + } = $numberOfTransitions" + + ", N = ${ + modules.values.joinToString("+") { + it.totalGuardsSize.toString() + } + } = $totalGuardsSize" + + ", A = ${ + modules.values.joinToString("+") { + it.getA()?.toString() ?: "?" + } + } = ${getA() ?: "?"}" } fun printStats() { @@ -309,9 +341,15 @@ fun buildBasicParallelModularAutomaton( val modularContext: ModularContext = context["modularContext"] val moduleControllingOutputVariable = context.convertIntVarArray("moduleControllingOutputVariable", model) + if (Globals.IS_ENCODE_EVENTLESS) { + val active = context.convertBoolVarArray("active", model) + logger.info("active = $active") + } + val modules = modularContext.mapIndexed { (m), ctx -> val C: Int = ctx["C"] val K: Int = ctx["K"] + val X: Int = ctx["X"] val Z: Int = ctx["Z"] val transitionDestination = ctx.convertIntVarArray("transitionDestination", model) val transitionInputEvent = ctx.convertIntVarArray("transitionInputEvent", model) @@ -322,6 +360,14 @@ fun buildBasicParallelModularAutomaton( val moduleOutputVariables = (1..Z).filter { z -> moduleControllingOutputVariable[z] == m } val initialOutputValues: OutputValues = ctx["initialOutputValues"] + // Only available if (Globals.IS_ENCODE_CONJUNCTIVE_GUARDS) + val inputVariableUsed by lazy { + ctx.convertBoolVarArray("inputVariableUsed", model) + } + val inputVariableLiteral by lazy { + ctx.convertBoolVarArray("inputVariableLiteral", model) + } + Automaton( inputEvents = scenarioTree.inputEvents, outputEvents = scenarioTree.outputEvents, @@ -349,15 +395,24 @@ fun buildBasicParallelModularAutomaton( scenarioTree.inputEvents[transitionInputEvent[c, k] - 1] }, transitionGuard = { c, k -> - TruthTableGuard( - truthTable = scenarioTree.uniqueInputs - .withIndex(start = 1) - .associate { (u, input) -> - input to transitionTruthTable[c, k, u] - } - // inputNames = scenarioTree.inputNames, - // uniqueInputs = scenarioTree.uniqueInputs - ) + if (Globals.IS_ENCODE_CONJUNCTIVE_GUARDS) { + ConjunctiveGuard( + literals = (1..X) + .filter { x -> inputVariableUsed[x] } + .map { x -> if (inputVariableLiteral[c, k, x]) x else -x }, + inputNames = scenarioTree.inputNames + ) + } else { + TruthTableGuard( + truthTable = scenarioTree.uniqueInputs + .withIndex(start = 1) + .associate { (u, input) -> + input to transitionTruthTable[c, k, u] + } + // inputNames = scenarioTree.inputNames, + // uniqueInputs = scenarioTree.uniqueInputs + ) + } } ) } @@ -436,3 +491,12 @@ fun buildExtendedParallelModularAutomaton( return ParallelModularAutomaton(modules, moduleControllingOutputVariable) } + +fun ParallelModularAutomaton.getA(): Int? { + var sum = 0 + for (module in modules.values) { + val a = module.getA() ?: return null + sum += a + } + return sum +} diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/guard/ConjunctiveGuard.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/guard/ConjunctiveGuard.kt new file mode 100644 index 00000000..801aa48a --- /dev/null +++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/guard/ConjunctiveGuard.kt @@ -0,0 +1,42 @@ +package ru.ifmo.fbsat.core.automaton.guard + +import kotlinx.serialization.SerialName +import kotlinx.serialization.Serializable +import ru.ifmo.fbsat.core.scenario.InputValues +import ru.ifmo.fbsat.core.utils.pow +import ru.ifmo.fbsat.core.utils.toBinaryString +import ru.ifmo.fbsat.core.utils.toBooleanList +import kotlin.math.absoluteValue + +@Serializable +@SerialName("ConjunctiveGuard") +class ConjunctiveGuard( + val literals: List, // signed 1-based + val inputNames: List, +) : Guard { + override val size: Int = literals.size + 1 + + override fun eval(inputValues: InputValues): Boolean { + return literals.all { lit -> + inputValues[lit.absoluteValue - 1] xor (lit < 0) + } + } + + override fun toSimpleString(): String { + return literals.joinToString(" & ") { lit -> + (if (lit < 0) "~" else "") + inputNames[lit.absoluteValue - 1] + } + } + + override fun toGraphvizString(): String { + return toSimpleString() + } + + override fun toFbtString(): String { + return toSimpleString().replace("~", "NOT ").replace(" & ", " AND ") + } + + override fun toSmvString(): String { + return toSimpleString().replace("~", "!") + } +} diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/guard/Guard.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/guard/Guard.kt index 2805a532..bd047fa9 100644 --- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/guard/Guard.kt +++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/automaton/guard/Guard.kt @@ -13,6 +13,7 @@ val guardModule = SerializersModule { subclass(UnconditionalGuard::class) subclass(TruthTableGuard::class) subclass(BooleanExpressionGuard::class) + subclass(ConjunctiveGuard::class) } } diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/AutomatonStructureConstraints.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/AutomatonStructureConstraints.kt index bdc9af71..8bf5d726 100644 --- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/AutomatonStructureConstraints.kt +++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/AutomatonStructureConstraints.kt @@ -6,16 +6,21 @@ import com.github.lipen.satlib.core.BoolVarArray import com.github.lipen.satlib.core.IntVarArray import com.github.lipen.satlib.core.eq import com.github.lipen.satlib.core.neq +import com.github.lipen.satlib.core.sign import com.github.lipen.satlib.op.atLeastOne import com.github.lipen.satlib.op.atMostOne import com.github.lipen.satlib.op.exactlyOne import com.github.lipen.satlib.op.iff import com.github.lipen.satlib.op.iffAnd +import com.github.lipen.satlib.op.iffImply import com.github.lipen.satlib.op.imply import com.github.lipen.satlib.op.implyAnd +import com.github.lipen.satlib.op.implyIffAnd import com.github.lipen.satlib.op.implyOr import com.github.lipen.satlib.solver.Solver +import ru.ifmo.fbsat.core.scenario.InputValues import ru.ifmo.fbsat.core.scenario.OutputValues +import ru.ifmo.fbsat.core.scenario.ScenarioTree import ru.ifmo.fbsat.core.solver.autoneg import ru.ifmo.fbsat.core.solver.clause import ru.ifmo.fbsat.core.solver.forEachModularContext @@ -50,6 +55,7 @@ fun Solver.declareNegativeAutomatonStructureConstraints(Us: Iterable) { fun Solver.declareParallelModularAutomatonStructureConstraints() { comment("Parallel modular automaton structure constraints") + val V: Int = context["V"] val M: Int = context["M"] val Z: Int = context["Z"] val moduleControllingOutputVariable: IntVarArray = context["moduleControllingOutputVariable"] @@ -75,7 +81,7 @@ fun Solver.declareParallelModularAutomatonStructureConstraints() { yield(moduleControllingOutputVariable[z] eq m) } - comment("Constraint free variables") + comment("Constrain free variables") forEachModularContext { m -> val C: Int = context["C"] val stateAlgorithmBot: BoolVarArray = context["stateAlgorithmBot"] @@ -86,6 +92,41 @@ fun Solver.declareParallelModularAutomatonStructureConstraints() { imply(moduleControllingOutputVariable[z] neq m, -stateAlgorithmBot[c, z]) } } + + if (Globals.FIXED_OUTPUT_DECOMPOSITION != null) { + comment("(adhoc) Fixing output decomposition") + for (z in 1..Z) { + val m = Globals.FIXED_OUTPUT_DECOMPOSITION!![z - 1] + if (m != null) { + clause(moduleControllingOutputVariable[z] eq m) + } + } + } + + forEachModularContext { m -> + comment("Parallel modular automaton structure constraints: for module m = $m") + } + + if (Globals.FIXED_ACTIVITY != null) { + comment("(adhoc) Fixing scenario tree node activity") + val activeValues: List = Globals.FIXED_ACTIVITY!! + + forEachModularContext { m -> + comment("Parallel modular automaton structure constraints: for module m = $m") + val active: BoolVarArray = context["active"] + for (v in 1..V) { + if (activeValues[v - 1] == null) { + continue + } + if (activeValues[v - 1]!!) { + clause(active[v]) + } else { + clause(-active[v]) + } + } + } + } + } fun Solver.declareConsecutiveModularAutomatonStructureConstraints() { @@ -429,6 +470,15 @@ internal fun Solver.declareAutomatonStructureConstraintsForInputs( } } + comment("Null-transitions have False guards") + for (c in 1..C) + for (k in 1..K) + for (u in Us) + imply( + transitionDestination[c, k] eq 0, + -transitionTruthTable[c, k, u] + ) + if (Globals.IS_ENCODE_DISJUNCTIVE_TRANSITIONS) { comment("Transitions are disjunctive (without priority function)") for (c in 1..C) @@ -439,4 +489,49 @@ internal fun Solver.declareAutomatonStructureConstraintsForInputs( yield(transitionFiring[c, k, e, u]) } } + + if (Globals.IS_ENCODE_CONJUNCTIVE_GUARDS) { + val tree: ScenarioTree<*, *> = context["tree"] + val uniqueInputs: List = tree.uniqueInputs + val X: Int = context["X"] + val inputVariableUsed: BoolVarArray = context["inputVariableUsed"] + val inputVariableLiteral: BoolVarArray = context["inputVariableLiteral"] + + comment("Conjunctive guard definition") + // (transitionDestination[c,k] != 0) => (tt[c,k,u] <=> AND_{x}(used[x] => (lit[c,k,x] <=> u[x]))) + for (c in 1..C) + for (k in 1..K) + for (u in Us) + implyIffAnd( + transitionDestination[c, k] neq 0, + transitionTruthTable[c, k, u] + ) { + for (x in 1..X) { + val aux = newLiteral() + iffImply( + aux, + inputVariableUsed[x], + inputVariableLiteral[c, k, x] sign uniqueInputs[u - 1][x - 1] + ) + yield(aux) + } + } + + comment("ALO inputVariableUsed") + // ALO_{x}(used[x]) + atLeastOne { + for (x in 1..X) + yield(inputVariableUsed[x]) + } + + comment("Fix free variables") + // (transitionDestination[c,k] = 0) => lit[c,k,x] + for (c in 1..C) + for (k in 1..K) + for (x in 1..X) + imply( + transitionDestination[c, k] eq 0, + inputVariableLiteral[c, k, x] + ) + } } diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/EventlessMappingConstraints.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/EventlessMappingConstraints.kt index f35ff2c2..8d91e99c 100644 --- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/EventlessMappingConstraints.kt +++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/EventlessMappingConstraints.kt @@ -1,5 +1,6 @@ package ru.ifmo.fbsat.core.constraints +import com.github.lipen.multiarray.MultiArray import com.github.lipen.satlib.core.BoolVarArray import com.github.lipen.satlib.core.IntVarArray import com.github.lipen.satlib.core.eq @@ -8,10 +9,13 @@ import com.github.lipen.satlib.op.iffAnd import com.github.lipen.satlib.op.iffOr import com.github.lipen.satlib.op.imply import com.github.lipen.satlib.op.implyIff +import com.github.lipen.satlib.op.implyImply import com.github.lipen.satlib.op.implyImplyIff +import com.github.lipen.satlib.op.implyImplyImply import com.github.lipen.satlib.solver.Solver import ru.ifmo.fbsat.core.scenario.ScenarioTree import ru.ifmo.fbsat.core.solver.clause +import ru.ifmo.fbsat.core.solver.forEachModularContext import ru.ifmo.fbsat.core.solver.imply2 import ru.ifmo.fbsat.core.utils.Globals import ru.ifmo.fbsat.core.utils.algorithmChoice @@ -237,3 +241,351 @@ fun Solver.declareEventlessPositiveMappingConstraints( } } } + +fun Solver.declarePositiveParallelModularEventlessMappingConstraints( + isEncodeReverseImplication: Boolean, +) { + comment("Eventless parallel modular positive mapping constraints") + // Note: yet we only consider the SYNC-ALL mapping semantics + val moduleControllingOutputVariable: IntVarArray = context["moduleControllingOutputVariable"] + + forEachModularContext { m -> + val tree: ScenarioTree<*, *> = context["tree"] + val V: Int = context["V"] + val C: Int = context["C"] + val K: Int = context["K"] + val Z: Int = context["Z"] + val stateOutputEvent: IntVarArray = context["stateOutputEvent"] + val stateAlgorithmTop: BoolVarArray = context["stateAlgorithmTop"] + val stateAlgorithmBot: BoolVarArray = context["stateAlgorithmBot"] + val actualTransitionFunction: IntVarArray = context["actualTransitionFunction"] + val transitionDestination: IntVarArray = context["transitionDestination"] + val mapping: IntVarArray = context["mapping"] + val active: BoolVarArray = context["active"] + + comment("Root maps to the first state") + clause(mapping[1] eq 1) + + comment("Root is passive") + clause(-active[1]) + + comment("Mapping constraints") + for (v in 2..V) { + val p = tree.parent(v) + val e = tree.inputEvent(v) + val u = tree.inputNumber(v) + val o = tree.outputEvent(v) + + // If any output value changed, then the node is definitely active + if ((1..Z).any { z -> tree.outputValue(v, z) != tree.outputValue(p, z) }) { + clause(active[v]) + } + + if (Globals.IS_ENCODE_EPSILON_PASSIVE) { + // If output event is epsilon, then the node is definitely passive + if (o == 0) { + clause(-active[v]) + } + } + + if (Globals.IS_ENCODE_NOT_EPSILON_ACTIVE) { + // If output event is not epsilon, then the node is definitely active + if (o != 0) { + clause(active[v]) + } + } + + if (Globals.IS_ENCODE_TRANSITION_FUNCTION) { + val transitionFunction: IntVarArray = context["transitionFunction"] + + comment("Positive mapping/transitionFunction definition for v = $v") + // (mapping[p] = q) => ((mapping[v] = q') <=> (transitionFunction[q,e,u] = q')) + for (i in 1..C) + for (j in 1..C) + implyIff( + mapping[p] eq i, + mapping[v] eq j, + transitionFunction[i, e, u] eq j + ) + } + + comment("Positive active-mapping definition for v = $v") + // active[v] => + // (mapping[v] = c) <=> (actualTransition[mapping[tp(v)],tie(v),tin(v)] = c) + for (i in 1..C) + for (j in 1..C) + implyImplyIff( + active[v], + mapping[p] eq i, + mapping[v] eq j, + actualTransitionFunction[i, e, u] eq j + ) + // active[v] => + // (mapping[v] = c) => (stateOutputEvent[c] = toe(v)) + for (c in 1..C) + imply2( + active[v], + mapping[v] eq c, + stateOutputEvent[c] eq o + ) + // active[v] => + // (mapping[v] = c) => AND_{z}(moduleControllingOutputVariable[z]=m) => (stateAlgorithm{tov(tp(v),z)}[c,z] = tov(v,z))) + // Note: here we use `moduleControllingOutputVariable`, because we are inside parallel-modular reduction + for (c in 1..C) + for (z in 1..Z) + implyImplyImply( + active[v], + mapping[v] eq c, + moduleControllingOutputVariable[z] eq m, + algorithmChoice( + tree = tree, + v = v, c = c, z = z, + algorithmTop = stateAlgorithmTop, + algorithmBot = stateAlgorithmBot + ) + ) + + comment("REVERSE actualTransitionFunction/active") + // (mapping[p] = q) & (actualTransitionFunction[q,e,u] != 0) => active[v] + for (c in 1..C) + imply2( + mapping[p] eq c, + actualTransitionFunction[c, e, u] neq 0, + active[v] + ) + + comment("Positive passive-mapping definition for v = $v") + // ~active[v] => + // mapping[v] = mapping[tp(v)] + for (c in 1..C) + imply2( + -active[v], + mapping[p] eq c, + mapping[v] eq c + ) + // ~active[v] => + // (mapping[tp(v)] = c) => (actualTransition[c,tie(v),tin(v)] = 0) + for (c in 1..C) + imply2( + -active[v], + mapping[p] eq c, + actualTransitionFunction[c, e, u] eq 0 + ) + + comment("REVERSE actualTransitionFunction/passive") + // (mapping[p] = q) & (actualTransitionFunction[q,e,u] = 0) => ~active[v] + for (c in 1..C) + imply2( + mapping[p] eq c, + actualTransitionFunction[c, e, u] eq 0, + -active[v] + ) + } + + if (isEncodeReverseImplication) { + comment("Mysterious reverse-implication") + // OR_k(transitionDestination[i,k,j]) => OR_{v}( mapping[p]=i & mapping[v]=j & active[v] ) + for (i in 1..C) + for (j in 1..C) { + val lhsAux = newLiteral() + iffOr(lhsAux) { + for (k in 1..K) + yield(transitionDestination[i, k] eq j) + } + + // val rhsAux = newLiteral() + val rhsAux = lhsAux // Note: when encoding `<=>` it is better to just use the same literal + iffOr(rhsAux) { + for (v in 2..V) { + val p = tree.parent(v) + val aux = newLiteral() + iffAnd(aux, mapping[p] eq i, mapping[v] eq j, active[v]) + yield(aux) + } + } + + // imply(lhsAux, rhsAux) + // + // // Adhoc: other way around! + // imply(rhsAux, lhsAux) + } + } + } +} + +fun Solver.declareDistributedPositiveEventlessMappingConstraints_compound( + modularIsEncodeReverseImplication: MultiArray, +) { + comment("Distributed [COMPOUND] positive eventless mapping constraints") + + forEachModularContext { m -> + comment("Distributed [COMPOUND] positive eventless mapping constraints: for module m = $m") + + val tree: ScenarioTree<*, *> = context["tree"] + val V: Int = context["V"] + val C: Int = context["C"] + val K: Int = context["K"] + val Z: Int = context["Z"] + val stateOutputEvent: IntVarArray = context["stateOutputEvent"] + val stateAlgorithmTop: BoolVarArray = context["stateAlgorithmTop"] + val stateAlgorithmBot: BoolVarArray = context["stateAlgorithmBot"] + val actualTransitionFunction: IntVarArray = context["actualTransitionFunction"] + val transitionDestination: IntVarArray = context["transitionDestination"] + val mapping: IntVarArray = context["mapping"] + val active: BoolVarArray = context["active"] + val stateUsed: BoolVarArray = context["stateUsed"] + + comment("Root maps to the first state") + clause(mapping[1] eq 1) + + comment("Root is passive") + clause(-active[1]) + + comment("Mapping constraints") + for (v in 2..V) { + val p = tree.parent(v) + val e = tree.inputEvent(v) + val u = tree.inputNumber(v) + val o = tree.outputEvent(v) + + // If any output value changed, then the node is definitely active + if ((1..Z).any { z -> tree.outputValue(v, z) != tree.outputValue(p, z) }) { + clause(active[v]) + } + + if (Globals.IS_ENCODE_EPSILON_PASSIVE) { + // If output event is epsilon, then the node is definitely passive + if (o == 0) { + clause(-active[v]) + } + } + + if (Globals.IS_ENCODE_NOT_EPSILON_ACTIVE) { + // If output event is not epsilon, then the node is definitely active + if (o != 0) { + clause(active[v]) + } + } + + if (Globals.IS_ENCODE_TRANSITION_FUNCTION) { + val transitionFunction: IntVarArray = context["transitionFunction"] + + comment("Positive mapping/transitionFunction definition for v = $v") + // (mapping[p] = q) => ((mapping[v] = q') <=> (transitionFunction[q,e,u] = q')) + for (i in 1..C) + for (j in 1..C) + implyIff( + mapping[p] eq i, + mapping[v] eq j, + transitionFunction[i, e, u] eq j + ) + } + + comment("Positive active-mapping definition for v = $v") + // active[v] => + // (mapping[v] = c) <=> (actualTransition[mapping[tp(v)],tie(v),tin(v)] = c) + for (i in 1..C) + for (j in 1..C) + implyImplyIff( + active[v], + mapping[p] eq i, + mapping[v] eq j, + actualTransitionFunction[i, e, u] eq j + ) + // active[v] => + // (mapping[v] = c) => (stateOutputEvent[c] = toe(v)) + for (c in 1..C) + imply2( + active[v], + mapping[v] eq c, + stateOutputEvent[c] eq o + ) + // active[v] => + // (mapping[v] = c) => AND_{z}(stateAlgorithm{tov(tp(v),z)}[c,z] = tov(v,z)) + for (c in 1..C) + for (z in 1..Z) + implyImply( + active[v], + mapping[v] eq c, + algorithmChoice( + tree = tree, + v = v, c = c, z = z, + algorithmTop = stateAlgorithmTop, + algorithmBot = stateAlgorithmBot + ) + ) + + comment("REVERSE actualTransitionFunction/active") + // (mapping[p] = q) & (actualTransitionFunction[q,e,u] != 0) => active[v] + for (c in 1..C) + imply2( + mapping[p] eq c, + actualTransitionFunction[c, e, u] neq 0, + active[v] + ) + + comment("Positive passive-mapping definition for v = $v") + // ~active[v] => + // mapping[v] = mapping[tp(v)] + for (c in 1..C) + imply2( + -active[v], + mapping[p] eq c, + mapping[v] eq c + ) + // ~active[v] => + // (mapping[tp(v)] = c) => (actualTransition[c,tie(v),tin(v)] = 0) + for (c in 1..C) + imply2( + -active[v], + mapping[p] eq c, + actualTransitionFunction[c, e, u] eq 0 + ) + + comment("REVERSE actualTransitionFunction/passive") + // (mapping[p] = q) & (actualTransitionFunction[q,e,u] = 0) => ~active[v] + for (c in 1..C) + imply2( + mapping[p] eq c, + actualTransitionFunction[c, e, u] eq 0, + -active[v] + ) + } + + /* Constraints for all vertices */ + for (v in 1..V) + for (c in 1..C) + imply( + -stateUsed[c], + mapping[v] neq c + ) + + val isEncodeReverseImplication = modularIsEncodeReverseImplication[m] + if (isEncodeReverseImplication) { + comment("Mysterious reverse-implication") + // OR_k(transitionDestination[i,k,j]) => OR_{v}( mapping[p]=i & mapping[v]=j & active[v] ) + for (i in 1..C) + for (j in 1..C) { + val lhsAux = newLiteral() + iffOr(lhsAux) { + for (k in 1..K) + yield(transitionDestination[i, k] eq j) + } + + // val rhsAux = newLiteral() + val rhsAux = lhsAux // Note: when encoding `<=>` it is better to just use the same literal + iffOr(rhsAux) { + for (v in 2..V) { + val p = tree.parent(v) + val aux = newLiteral() + iffAnd(aux, mapping[p] eq i, mapping[v] eq j, active[v]) + yield(aux) + } + } + + // imply(lhsAux, rhsAux) + // imply(rhsAux, lhsAux) + } + } + } +} diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/MappingConstraints.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/MappingConstraints.kt index 0631f80d..46f28b0b 100644 --- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/MappingConstraints.kt +++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/constraints/MappingConstraints.kt @@ -114,14 +114,14 @@ fun Solver.declareNegativeMappingConstraints( /* Constraints for active vertices */ comment("Negative mapping constraints: for active nodes") for (v in Vs.intersect(negativeScenarioTree.activeVertices)) { - // comment("Negative mapping constraints: for active node v = $v") + // comment("Negative mapping constraints: for active node v = $v".also{logger.debug(it) declareMappingConstraintsForActiveNode(v = v, isPositive = false) } /* Constraints for passive vertices */ comment("Negative mapping constraints: for passive nodes") for (v in Vs.intersect(negativeScenarioTree.passiveVertices)) { - // comment("Negative mapping constraints: for passive node v = $v") + // comment("Negative mapping constraints: for passive node v = $v".also{logger.debug(it) declareMappingConstraintsForPassiveNode(v = v, isPositive = false) } @@ -203,7 +203,8 @@ fun Solver.declarePositiveParallelModularMappingConstraints( yield(transitionDestination[i, k] eq j) } - val rhsAux = newLiteral() + // val rhsAux = newLiteral() + val rhsAux = lhsAux // Note: when encoding `<=>` it is better to just use the same literal iffOr(rhsAux) { for (v in scenarioTree.activeVertices) { val p = scenarioTree.parent(v) @@ -213,7 +214,8 @@ fun Solver.declarePositiveParallelModularMappingConstraints( } } - imply(lhsAux, rhsAux) + // imply(lhsAux, rhsAux) + // imply(rhsAux, lhsAux) } } } @@ -410,10 +412,10 @@ fun Solver.declarePositiveArbitraryModularMappingConstraints( fun Solver.declareDistributedPositiveMappingConstraints_modular( modularIsEncodeReverseImplication: MultiArray, ) { - // comment("Distributed positive mapping constraints") + // comment("Distributed positive mapping constraints".also{logger.debug(it) // with(distributedBasicVariables) { // for (m in 1..M) { - // comment("Distributed positive mapping constraints: module m = $m") + // comment("Distributed positive mapping constraints: module m = $m".also{logger.debug(it) // declarePositiveMappingConstraints( // basicVariables = modularBasicVariables[m], // isEncodeReverseImplication = modularIsEncodeReverseImplication[m] @@ -643,7 +645,7 @@ private fun Solver.declareArbitraryModularMappingConstraintsForActiveNode( val stateAlgorithmTop: BoolVarArray = context["stateAlgorithmTop"] val mapping: IntVarArray = context["mapping"] - // comment("Arbitrary modular mapping definition for active node v = $v, module m = $m") + // comment("Arbitrary modular mapping definition for active node v = $v, module m = $m".also{logger.debug(it) // (inputIndex[v]=u) => (mapping[tp(v)]=i) => (mapping[v]=j) <=> (actualTransition[i,u]=j)) // Note: implyImplyImply vs implyImplyIff @@ -797,7 +799,7 @@ private fun Solver.declareMappingConstraintsForActiveNode( ) ) } else { - // comment("Negative mapping definition for active node v = $v") + // comment("Negative mapping definition for active node v = $v".also{logger.debug(it) // // (mapping[v]=c) <=> (actualTransition[mapping[tp(v)],tie(v),tin(v)]=c) & (stateOutputEvent[c]=toe(v)) & AND_{z}(stateAlgorithm{tov(tp(v),z)}[c,z] = tov(v,z)) // for (i in 1..C) // for (j in 1..C) diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/Optimization.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/Optimization.kt index eb14ed2c..13317b4c 100644 --- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/Optimization.kt +++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/Optimization.kt @@ -7,6 +7,8 @@ import ru.ifmo.fbsat.core.automaton.Automaton import ru.ifmo.fbsat.core.automaton.ConsecutiveModularAutomaton import ru.ifmo.fbsat.core.automaton.DistributedAutomaton import ru.ifmo.fbsat.core.automaton.ParallelModularAutomaton +import ru.ifmo.fbsat.core.automaton.getA +import ru.ifmo.fbsat.core.automaton.getTA import ru.ifmo.fbsat.core.task.distributed.basic.inferDistributedBasic import ru.ifmo.fbsat.core.task.distributed.complete.inferDistributedComplete import ru.ifmo.fbsat.core.task.distributed.extended.inferDistributedExtended @@ -114,6 +116,23 @@ fun Inferrer.optimizeN( ) } +@Suppress("FunctionName") +fun Inferrer.optimizeTA( + start: Int? = null, + end: Int = 0, + useAssumptions: Boolean = Globals.IS_USE_ASSUMPTIONS, +): Automaton? { + logger.info("Optimizing T*A (${if (useAssumptions) "with" else "without"} assumptions) from $start to $end...") + val cardinality: Cardinality = solver.context["cardinalityTA"] + return cardinality.optimizeTopDown( + start = start, + end = end, + useAssumptions = useAssumptions, + infer = { inferBasic() }, + query = { it.getTA()!! } + ) +} + @Suppress("FunctionName") fun Inferrer.optimizeN_Forest( start: Int? = null, @@ -244,6 +263,42 @@ fun Inferrer.optimizeArbitraryModularN( ) } +fun Inferrer.optimizeParallelModularA( + start: Int? = null, + end: Int = 0, + useAssumptions: Boolean = Globals.IS_USE_ASSUMPTIONS, +): ParallelModularAutomaton? { + logger.info("Optimizing A (${if (useAssumptions) "with" else "without"} assumptions) from $start to $end...") + val cardinality: Cardinality = solver.context["cardinalityA"] + return cardinality.optimizeTopDown( + start = start, + end = end, + useAssumptions = useAssumptions, + infer = { inferParallelModularBasic() }, + query = { it.getA()!! } + ) +} + +fun Inferrer.optimizeParallelModularCKA( + start: Int? = null, + end: Int = 0, + useAssumptions: Boolean = Globals.IS_USE_ASSUMPTIONS, +): ParallelModularAutomaton? { + logger.info("Optimizing C*K*A (${if (useAssumptions) "with" else "without"} assumptions) from $start to $end...") + val cardinality: Cardinality = solver.context["cardinalityCKA"] + return cardinality.optimizeTopDown( + start = start, + end = end, + useAssumptions = useAssumptions, + infer = { inferParallelModularBasic() }, + query = { + it.modules.values.sumOf { module -> + module.numberOfTransitions * module.maxOutgoingTransitions * module.getA()!! + } + } + ) +} + fun Inferrer.optimizeDistributedSumC( start: Int? = null, end: Int = 0, diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/distributed/basic/DistributedBasicTask.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/distributed/basic/DistributedBasicTask.kt index e376d58b..3ef445d5 100644 --- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/distributed/basic/DistributedBasicTask.kt +++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/distributed/basic/DistributedBasicTask.kt @@ -6,6 +6,7 @@ import com.github.lipen.satlib.card.Cardinality import com.github.lipen.satlib.solver.Solver import ru.ifmo.fbsat.core.constraints.declareDistributedAutomatonBfsConstraints import ru.ifmo.fbsat.core.constraints.declareDistributedAutomatonStructureConstraints +import ru.ifmo.fbsat.core.constraints.declareDistributedPositiveEventlessMappingConstraints_compound import ru.ifmo.fbsat.core.constraints.declareDistributedPositiveMappingConstraints_compound import ru.ifmo.fbsat.core.scenario.positive.PositiveScenarioTree import ru.ifmo.fbsat.core.solver.forEachModularContext @@ -48,8 +49,12 @@ data class DistributedBasicTask( comment("$name: Constraints") declareDistributedAutomatonStructureConstraints() if (Globals.IS_BFS_AUTOMATON) declareDistributedAutomatonBfsConstraints() - // declareDistributedPositiveMappingConstraints_modular(vars, modularIsEncodeReverseImplication) - declareDistributedPositiveMappingConstraints_compound(modularIsEncodeReverseImplication) + if (Globals.IS_ENCODE_EVENTLESS) { + declareDistributedPositiveEventlessMappingConstraints_compound(modularIsEncodeReverseImplication) + } else { + // declareDistributedPositiveMappingConstraints_modular(vars, modularIsEncodeReverseImplication) + declareDistributedPositiveMappingConstraints_compound(modularIsEncodeReverseImplication) + } // declareDistributedBasicAdhocConstraints() /* Initial cardinality constraints */ diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasic.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasic.kt index 982d333e..65de9830 100644 --- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasic.kt +++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasic.kt @@ -1,12 +1,29 @@ package ru.ifmo.fbsat.core.task.modular.basic.parallel +import com.github.lipen.multiarray.forEachIndexed import com.soywiz.klock.measureTimeWithResult +import okio.buffer +import okio.sink import ru.ifmo.fbsat.core.automaton.ParallelModularAutomaton import ru.ifmo.fbsat.core.automaton.buildBasicParallelModularAutomaton +import ru.ifmo.fbsat.core.scenario.inputEvent +import ru.ifmo.fbsat.core.scenario.inputValues +import ru.ifmo.fbsat.core.scenario.outputEvent +import ru.ifmo.fbsat.core.scenario.outputValues import ru.ifmo.fbsat.core.scenario.positive.PositiveScenarioTree +import ru.ifmo.fbsat.core.solver.convertBoolVarArray +import ru.ifmo.fbsat.core.solver.convertIntVarArray import ru.ifmo.fbsat.core.task.Inferrer +import ru.ifmo.fbsat.core.task.optimizeParallelModularA import ru.ifmo.fbsat.core.task.optimizeParallelModularT +import ru.ifmo.fbsat.core.utils.Globals +import ru.ifmo.fbsat.core.utils.ModularContext import ru.ifmo.fbsat.core.utils.MyLogger +import ru.ifmo.fbsat.core.utils.ensureParentExists +import ru.ifmo.fbsat.core.utils.toBinaryString +import ru.ifmo.fbsat.core.utils.useWith +import ru.ifmo.fbsat.core.utils.write +import ru.ifmo.fbsat.core.utils.writeln private val logger = MyLogger {} @@ -37,6 +54,7 @@ fun Inferrer.parallelModularBasicMinC( numberOfModules: Int, // M start: Int = 1, // C_start end: Int = 20, // C_end + maxOutgoingTransitionsForC: (Int) -> Int = { it }, // lambda for computing K, input arg is C, K=C by default ): ParallelModularAutomaton { var best: ParallelModularAutomaton? = null for (C in start..end) { @@ -44,7 +62,8 @@ fun Inferrer.parallelModularBasicMinC( parallelModularBasic( scenarioTree = scenarioTree, numberOfModules = numberOfModules, - numberOfStates = C + numberOfStates = C, + maxOutgoingTransitions = maxOutgoingTransitionsForC(C) ) } if (result != null) { @@ -63,14 +82,79 @@ fun Inferrer.parallelModularBasicMin( scenarioTree: PositiveScenarioTree, numberOfModules: Int, // M numberOfStates: Int? = null, // C_start, 1 if null + maxOutgoingTransitionsForC: (Int) -> Int = { it }, // lambda for computing K, input arg is C, K=C by default ): ParallelModularAutomaton? { - parallelModularBasicMinC(scenarioTree, numberOfModules = numberOfModules, start = numberOfStates ?: 1) - return optimizeParallelModularT() + parallelModularBasicMinC( + scenarioTree, + numberOfModules = numberOfModules, + start = numberOfStates ?: 1, + maxOutgoingTransitionsForC = maxOutgoingTransitionsForC + ) + return if (Globals.IS_ENCODE_CONJUNCTIVE_GUARDS) { + optimizeParallelModularA() + } else { + optimizeParallelModularT() + } } fun Inferrer.inferParallelModularBasic(): ParallelModularAutomaton? { val model = solveAndGetModel() ?: return null val automaton = buildBasicParallelModularAutomaton(solver.context, model) + val moduleControllingOutputVariable = + solver.context.convertIntVarArray("moduleControllingOutputVariable", model) + + logger.info("output-decomposition = " + moduleControllingOutputVariable) + + if (Globals.IS_ENCODE_CONJUNCTIVE_GUARDS) { + val modularContext: ModularContext = solver.context["modularContext"] + modularContext.forEachIndexed { (m), ctx -> + val scenarioTree: PositiveScenarioTree = ctx["scenarioTree"] + val X: Int = ctx["X"] + val Z: Int = ctx["Z"] + val inputVariableUsed = ctx.convertBoolVarArray("inputVariableUsed", model) + logger.info("$m: input-used = $inputVariableUsed") + + val sliceInput = (1..X).filter { x -> + inputVariableUsed[x] + }.map { it - 1 } + val sliceOutput = (1..Z).filter { z -> + moduleControllingOutputVariable[z] == m + }.map { it - 1 } + logger.debug("Slice input indices for m = $m: $sliceInput") + logger.debug("Slice output indices for m = $m: $sliceOutput") + + val slicedScenarios = scenarioTree.scenarios.map { + it.slice(sliceInput, sliceOutput) + } + val outFile = outDir.resolve("sliced-scenarios-m$m") + logger.debug("Writing ${slicedScenarios.size} sliced scenario(s) for m = $m to '$outFile'") + outFile.ensureParentExists().sink().buffer().useWith { + writeln("${slicedScenarios.size}") + for (scenario in slicedScenarios) { + for (element in scenario.elements) { + if (element.inputEvent != null) { + write("in=${element.inputEvent}[${element.inputValues.values.toBinaryString()}]; ") + } + if (element.outputEvent != null) { + write("out=${element.outputEvent}[${element.outputValues.values.toBinaryString()}]; ") + } + } + writeln() + } + } + + outDir.resolve("input-names-m$m").ensureParentExists().sink().buffer().useWith { + for (name in scenarioTree.inputNames.slice(sliceInput)) { + writeln(name) + } + } + outDir.resolve("output-names-m$m").ensureParentExists().sink().buffer().useWith { + for (name in scenarioTree.outputNames.slice(sliceOutput)) { + writeln(name) + } + } + } + } // TODO: check automaton // log.warn("Mapping check is not implemented yet") diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasicTask.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasicTask.kt index c79ca956..1ff9e504 100644 --- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasicTask.kt +++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasicTask.kt @@ -2,6 +2,7 @@ package ru.ifmo.fbsat.core.task.modular.basic.parallel import com.github.lipen.satlib.card.Cardinality import com.github.lipen.satlib.solver.Solver +import ru.ifmo.fbsat.core.constraints.declarePositiveParallelModularEventlessMappingConstraints import ru.ifmo.fbsat.core.constraints.declareParallelModularAutomatonBfsConstraints import ru.ifmo.fbsat.core.constraints.declareParallelModularAutomatonStructureConstraints import ru.ifmo.fbsat.core.constraints.declarePositiveParallelModularMappingConstraints @@ -31,7 +32,11 @@ data class ParallelModularBasicTask( comment("$name: Constraints") declareParallelModularAutomatonStructureConstraints() if (Globals.IS_BFS_AUTOMATON) declareParallelModularAutomatonBfsConstraints() - declarePositiveParallelModularMappingConstraints(isEncodeReverseImplication) + if (Globals.IS_ENCODE_EVENTLESS) { + declarePositiveParallelModularEventlessMappingConstraints(isEncodeReverseImplication) + } else { + declarePositiveParallelModularMappingConstraints(isEncodeReverseImplication) + } /* Initial cardinality constraints */ comment("$name: Initial cardinality (T) constraints") diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasicVariables.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasicVariables.kt index 1faacacd..1a2e2345 100644 --- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasicVariables.kt +++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/modular/basic/parallel/ParallelModularBasicVariables.kt @@ -1,14 +1,20 @@ package ru.ifmo.fbsat.core.task.modular.basic.parallel import com.github.lipen.satlib.card.declareCardinality +import com.github.lipen.satlib.core.BoolVarArray import com.github.lipen.satlib.core.IntVarArray import com.github.lipen.satlib.core.neq +import com.github.lipen.satlib.core.newBoolVarArray import com.github.lipen.satlib.core.newIntVarArray import com.github.lipen.satlib.solver.Solver import ru.ifmo.fbsat.core.scenario.positive.PositiveScenarioTree import ru.ifmo.fbsat.core.solver.declareModularContext import ru.ifmo.fbsat.core.solver.forEachModularContext import ru.ifmo.fbsat.core.task.single.basic.declareBasicVariables +import ru.ifmo.fbsat.core.utils.Globals +import ru.ifmo.fbsat.core.utils.MyLogger + +private val logger = MyLogger {} @Suppress("LocalVariableName") fun Solver.declareParallelModularBasicVariables( @@ -36,9 +42,21 @@ fun Solver.declareParallelModularBasicVariables( context["Z"] = Z context["U"] = U + val active = if (Globals.IS_ENCODE_EVENTLESS) { + context("active") { + newBoolVarArray(V) + } + } else { + null + } + /* Modular */ declareModularContext(M) - forEachModularContext { + forEachModularContext { m -> + if (Globals.IS_ENCODE_EVENTLESS) { + logger.debug("Reusing active[v] for module m = $m") + context["active"] = active!! + } declareBasicVariables( positiveScenarioTree = scenarioTree, C = C, K = K, @@ -66,4 +84,66 @@ fun Solver.declareParallelModularBasicVariables( } } } + if (Globals.IS_ENCODE_CONJUNCTIVE_GUARDS) { + comment("Cardinality (A)") + val cardinalityA = context("cardinalityA") { + val nVars = numberOfVariables + val nCons = numberOfClauses + declareCardinality { + @Suppress("NAME_SHADOWING") + forEachModularContext { + val X: Int = context["X"] + val inputVariableUsed: BoolVarArray = context["inputVariableUsed"] + for (x in 1..X) + yield(inputVariableUsed[x]) + } + }.also { + val diffVars = numberOfVariables - nVars + val diffCons = numberOfClauses - nCons + logger.debug("Declared cardinalityA: $diffVars vars and $diffCons clauses") + } + } + if (Globals.IS_ENCODE_CARDINALITY_CKA) { + comment("Cardinality (C*K*A)") + val cardinalityCKA = context("cardinalityCKA") { + declareCardinality { + @Suppress("NAME_SHADOWING") + forEachModularContext { + val C: Int = context["C"] + val K: Int = context["K"] + val X: Int = context["X"] + val inputVariableUsed: BoolVarArray = context["inputVariableUsed"] + for (c in 1..C) + for (k in 1..K) + for (x in 1..X) + yield(inputVariableUsed[x]) + } + } + } + } + // comment("Cardinality (T*A)") + // val cardinalityTA = context("cardinalityTA") { + // declareCardinality { + // @Suppress("NAME_SHADOWING") + // forEachModularContext { + // val C: Int = context["C"] + // val K: Int = context["K"] + // val X: Int = context["X"] + // val transitionDestination: IntVarArray = context["transitionDestination"] + // val inputVariableUsed: BoolVarArray = context["inputVariableUsed"] + // for (c in 1..C) + // for (k in 1..K) + // for (x in 1..X) { + // val aux = newLiteral() + // iffAnd( + // aux, + // transitionDestination[c, k] neq 0, + // inputVariableUsed[x] + // ) + // yield(aux) + // } + // } + // } + // } + } } diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/single/basic/Basic.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/single/basic/Basic.kt index e7c26e8c..e023266c 100644 --- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/single/basic/Basic.kt +++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/single/basic/Basic.kt @@ -10,6 +10,7 @@ import ru.ifmo.fbsat.core.solver.numberOfConflicts import ru.ifmo.fbsat.core.solver.numberOfDecisions import ru.ifmo.fbsat.core.solver.numberOfPropagations import ru.ifmo.fbsat.core.task.Inferrer +import ru.ifmo.fbsat.core.task.optimizeTA import ru.ifmo.fbsat.core.task.optimizeT import ru.ifmo.fbsat.core.utils.Globals import ru.ifmo.fbsat.core.utils.MyLogger @@ -101,7 +102,11 @@ fun Inferrer.basicMin( end = end, isEncodeReverseImplication = isEncodeReverseImplication ) ?: return@run null - optimizeT() + if (Globals.IS_ENCODE_CONJUNCTIVE_GUARDS) { + optimizeTA() + } else { + optimizeT() + } } logger.info("Task basic-min done in %.2f s".format(timeSince(timeStart).seconds)) if (solver.isSupportStats()) { diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/single/basic/BasicVariables.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/single/basic/BasicVariables.kt index a3f1ce59..7ba95bf1 100644 --- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/single/basic/BasicVariables.kt +++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/task/single/basic/BasicVariables.kt @@ -1,17 +1,21 @@ package ru.ifmo.fbsat.core.task.single.basic import com.github.lipen.satlib.card.declareCardinality +import com.github.lipen.satlib.core.BoolVarArray import com.github.lipen.satlib.core.IntVarArray import com.github.lipen.satlib.core.eq import com.github.lipen.satlib.core.neq import com.github.lipen.satlib.core.newBoolVarArray import com.github.lipen.satlib.core.newIntVar import com.github.lipen.satlib.core.newIntVarArray +import com.github.lipen.satlib.op.* import com.github.lipen.satlib.solver.Solver import ru.ifmo.fbsat.core.scenario.initialOutputValues import ru.ifmo.fbsat.core.scenario.positive.PositiveScenarioTree -import ru.ifmo.fbsat.core.solver.literals import ru.ifmo.fbsat.core.utils.Globals +import ru.ifmo.fbsat.core.utils.MyLogger + +private val logger = MyLogger {} @Suppress("LocalVariableName") fun Solver.declareBasicVariables( @@ -98,6 +102,14 @@ fun Solver.declareBasicVariables( val stateAlgorithmTop = context("stateAlgorithmTop") { newBoolVarArray(C, Z) } + if (Globals.IS_ENCODE_CONJUNCTIVE_GUARDS) { + val inputVariableUsed = context("inputVariableUsed") { + newBoolVarArray(X) + } + val inputVariableLiteral = context("inputVariableLiteral") { + newBoolVarArray(C, K, X) + } + } /* Mapping variables */ comment("Mapping variables") @@ -105,8 +117,10 @@ fun Solver.declareBasicVariables( newIntVarArray(V) { 1..C } } if (Globals.IS_ENCODE_EVENTLESS) { - val active = context("active") { - newBoolVarArray(V) + if (!context.map.containsKey("active")) { + val active = context("active") { + newBoolVarArray(V) + } } } @@ -119,19 +133,29 @@ fun Solver.declareBasicVariables( yield(transitionDestination[c, k] neq 0) } } - - if (Globals.IS_DUMP_VARS_IN_CNF) { - comment("actualTransitionFunction = ${actualTransitionFunction.literals}") - comment("transitionDestination = ${transitionDestination.literals}") - comment("transitionInputEvent = ${transitionInputEvent.literals}") - comment("transitionTruthTable = ${transitionTruthTable.literals}") - comment("transitionFiring = ${transitionFiring.literals}") - comment("firstFired = ${firstFired.literals}") - comment("notFired = ${notFired.literals}") - comment("stateOutputEvent = ${stateOutputEvent.literals}") - comment("stateAlgorithmBot = ${stateAlgorithmBot.literals}") - comment("stateAlgorithmTop = ${stateAlgorithmTop.literals}") - comment("mapping = ${mapping.literals}") - comment("totalizerT = ${cardinalityT.totalizer}") + if (Globals.IS_ENCODE_CONJUNCTIVE_GUARDS) { + comment("Cardinality (T*A)") + val inputVariableUsed: BoolVarArray = context["inputVariableUsed"] + val cardinalityTA = context("cardinalityTA") { + val nVars = numberOfVariables + val nCons = numberOfClauses + declareCardinality { + for (c in 1..C) + for (k in 1..K) + for (x in 1..X) { + val aux = newLiteral() + iffAnd( + aux, + transitionDestination[c, k] neq 0, + inputVariableUsed[x] + ) + yield(aux) + } + }.also { + val diffVars = numberOfVariables - nVars + val diffCons = numberOfClauses - nCons + logger.debug("Declared cardinalityTA: $diffVars vars and $diffCons clauses") + } + } } } diff --git a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/utils/Globals.kt b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/utils/Globals.kt index 36a4f28b..583c86d2 100644 --- a/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/utils/Globals.kt +++ b/fbsat-core/src/main/kotlin/ru/ifmo/fbsat/core/utils/Globals.kt @@ -15,6 +15,8 @@ enum class StartStateAlgorithms { object Globals { var EPSILON_OUTPUT_EVENTS: EpsilonOutputEvents = EpsilonOutputEvents.ONLYSTART var START_STATE_ALGORITHMS: StartStateAlgorithms = StartStateAlgorithms.ZERO + var FIXED_OUTPUT_DECOMPOSITION: List? = null + var FIXED_ACTIVITY: List? = null var IS_FORBID_OR: Boolean = false var IS_FORBID_TRANSITIONS_TO_FIRST_STATE: Boolean = true var IS_BFS_AUTOMATON: Boolean = true @@ -33,7 +35,10 @@ object Globals { var IS_ENCODE_TRANSITION_FUNCTION: Boolean = false var IS_ENCODE_EPSILON_PASSIVE: Boolean = false var IS_ENCODE_NOT_EPSILON_ACTIVE: Boolean = false + var IS_ENCODE_CONJUNCTIVE_GUARDS: Boolean = false + var IS_ENCODE_CARDINALITY_CKA: Boolean = false var IS_FIX_ACTIVE: Boolean = false + var IS_FIX_OUTPUT_DECOMPOSITION: Boolean = false var IS_DEBUG: Boolean = false var IS_REUSE_K: Boolean = true var IS_DUMP_CNF: Boolean = false