Target-oriented model finding (TOMF) in Forge

CAUTION: This feature of Forge is experimental and subject to change. It will be added as a preview feature in version 4.3.

Forge uses a modified version of the Pardinus model finder as its back end. Pardinus supports a form of optimization that targets a specific goal instance (which may or may not satisfy the given constraints). We are grateful to Alcino Cunha, Nuno Macedo, and Tiago Guimarães for their engineering work and technical paper on target orientation.

How to enable TOMF

To enable target-oriented mode, switch solvers to partial max-SAT and use the target problem type:

option problem_type target
option solver PMaxSAT4J

This should only be done in Relational Forge (#lang forge). Do not attempt to use target mode in Temporal Forge, which requires a different backend solver mode.

Mode: Targeting a partial instance

To prioritize instances as close as possible to a target, use the target_pi keyword in a run command. The argument may be either be the name of a pre-defined inst or a {}-delimited partial-instance block.

Example: Minimal Instances

This example will produce the empty instance first, then a graph of 1 node, etc.

#lang forge
option problem_type target
option solver PMaxSAT4J
sig Node { edges: pfunc Node -> Int }
inst emptyGraph { no Node }
tomf_test_close_noretarget_noNode: run {}
  target_pi emptyGraph

Mode: Targeting an integer expression

It can sometimes be useful to minimize an integer expression, rather than a set. To do this, use either the minimize_int or maximize_int keywords, providing an integer-valued expression.

When optimizing with respect to an integer expression, keep in mind the bitwidth. E.g., the default bitwidth of 4 will instantiate the $2^{4} = 16$ integers in the interval [-8, 7]. Thus, minimizing an integer expression when the default bitwidth is in effect will target -8.

Example: Minimizing total edge weight

This example will produce graphs with minimal total edge weight, modulo potential underflow. E.g., the example may produce a graph with a single edge of weight -8, but it might also produce a graph with three distinct -8-weight edges.

#lang forge
option problem_type target
option solver PMaxSAT4J
sig Node { edges: pfunc Node -> Int }
tomf_test_close_noretarget_int_totalWeight4: run {} for exactly 2 Node
  minimize_int {sum m: Node | sum n: Node | m.edges[n]}

If this example used maximize_int rather than minimize_int, the solver would anti-target -8 and in effect target the maximum integer value 7.

Forge Documentation