dcsolver

package module
v0.9.1 Latest Latest
Warning

This package is not in the latest version of its module.

 Go to latest Published: Jul 30, 2025 License: MIT Imports: 13 Imported by: 0

README

DCSolver

DCSolver is a pure Go library for checking the satisfiability of Difference Constraints Systems (DCS), meaning a conjunction of linear inequalities of the form x - y ≤ a or x - y < b, where x and y are positive, real-valued variables, and a and b are integer constants.

We also provide a command-line tool, called dcsolve, used to showcase how to use our API. The tool can be used to check the satisfiability of a DCS expressed using a restricted subset of SMT-LIB syntax.

Usage

You can find an example in the code of the dcsolve command, see cmd/dcsolve/main.go. The following example shows the basic usage of the package: create a new constraint system (DCS), add some variables and some constraints between them, then output a feasible solution. You can also look at the documentation example on the pkgsite for this package.

package main

import (
 "fmt"
 "github.com/dalzilio/dcsolver"
)

func main() {
 // Create a new DCS and add variables x and y.
 cg := dcsolver.NewDCS()
 cg.AddVars("x", "y")

 // Each variable can be manipulated using its index. Since every system has
 // a reserved, default variable called "start" (with index 0), that stands
 // for the initial date, variables x and y have index 1 and 2 respectively.
 fmt.Printf("list of variables: %v\n", cg.Names)

 // We can add constraints using one of the five supported operations: LTHAN
 // (less-than, <), LTEQ (less-tha or equal, ≤), EQ (equal, =), GTHAN
 // (greater-than, >), and GTEQ (greater-than or equal, ≥). By default, we
 // have the constraint that every variable, say x, is positive: x ≥ 0.
 //
 // A call to Add(i, j, op, n) updates the DCS by adding the constraint 
 // Names[j] - Names[i] op n. For instance, to add the constraint y ≥ x + 1 
 // (that can be encoded as y - x GTEQ 1):
 cg.Add(1, 2, dcsolver.GTEQ, 1)

 // It is possible to print a human-readable representation of the system.
 fmt.Print(cg.PrintSystem())
 
 // You can check if the system is satisfiable by looking at the value of
 // cg.SAT. If true, it is possible to output one feasible
 // solution. A valuation of the form "x: 1⁻" stands for the fact that the
 // value of x is of the form 1 ± ε, for ε a small positive value.
 if (cg.SAT) {
   fmt.Printf("Feasible solution: %s\n", cg.PrintFeasible())
 }
}

About

We follow an approach described by Pratt, where satisfiability is reduced to the problem of checking the absence of negative cycles in a graph where variables are node, and there is an edge from y to x of length cto represent the constraint x - y < c.

We consider a special vertex for the starting date, associated with the (reserved) variable start. Hence, we can encode constraints of the form x ≤ b or x > a, using relations of the form x - start ≤ b and 0 - start < a, respectively.

We borrowed some ideas from the following work, that defines an incremental method for solving this kind of problem. At the moment, we follow a simpler approach based on a simplified version of Bellman-Ford algorithm.

One main difference if our support for both strict and weak inequalities. Also, supporting strict constraints (meaning answering if the system is SAT for rational/real values) is more difficult. Some solution is given in:

Dependencies

The library has no dependencies outside the standard Go library. It uses Go modules and has been tested with Go 1.24.

For function ExecZ3, we assume that the command z3 is installed locally and can be resolved by exec.LookPath.

License

This software is distributed under the MIT License. A copy of the license agreement is found in the LICENSE file.

Authors

Documentation

Overview

Package dcsolve implements a solver for linear systems of inequalities of the form x - y ≤ c or x - y < c, with c an integer constant, and z, y are positive, real-valued variables.

Example

This example shows the basic usage of the package: create a new constraint system (DCS), add some variables and some constraints between them, then output a feasible solution. 

package main

import (
	"fmt"

	"github.com/dalzilio/dcsolver"
)

func main() {
	// Create a new DCS and add variables x, y and z.
	cg := dcsolver.NewDCS()
	cg.AddVars("x", "y", "z")

	// Each variable can be manipulated using its index. Since every system has
	// a reserved, default variable called "start" (with index 0), that stands
	// for the initial date, variables x, y, z have index 1, 2 and 3
	// respectively.
	fmt.Printf("list of variables: %v\n", cg.Names)

	// We can add constraints using one of the five supported operations: LTHAN
	// (less-than, <), LTEQ (less-tha or equal, ≤), EQ (equal, =), GTHAN
	// (greater-than, >), and GTEQ (greater-than or equal, ≥). By default, we
	// have the constraint that every variable, say x, is positive: x ≥ 0.
	//
	// For instance, to add the constraint z - x > 5 and z > y ≥ x (that can be
	// encoded as y - z < 0 and x - y ≤ 0):
	cg.Add(1, 3, dcsolver.GTHAN, 5)
	cg.Add(3, 2, dcsolver.LTHAN, 0)
	cg.Add(2, 1, dcsolver.LTEQ, 0)

	// The constraint z = 6 can be encoded as z - start = 6:
	cg.Add(0, 3, dcsolver.EQ, 6)

	// It is possible to print a human-readable representation of the system.
	fmt.Print(cg.PrintSystem())

	// You can check if the system is satisfiable by looking at the value of
	// [cg.SAT]. Since we use an incremental method, we stop updating a DCS as
	// soon as it is unsatisfiable. If SAT, you can output one feasible
	// solution. A valuation of the form "x: 1⁻" stands for the fact that the
	// value of x is of the form 1 ± ε, for ε a small positive value.
	fmt.Printf("Feasible solution: %s\n", cg.PrintFeasible())
}

Output:

list of variables: [start x y z]
0 ≤ x
0 ≤ y
0 ≤ y - x
6 ≤ z ≤ 6
5 < z - x
0 < z - y
Feasible solution: [x: 1⁻, y: 6⁻, z: 6]

Index

Examples

Constants

This section is empty.

Variables

This section is empty.

Functions

func BCompare 

func BCompare(a, b Bound) int

BCompare returns an integer comparing two bounds. The result will be 0 if a and b are equal, negative if a < b, and positive otherwise. We return the difference between the bounds values, with some exceptions. We always return +1 when a and b have same values, but a is LTEQ whereas b is LTHAN. For intance, the bound ≤ 3 is considered strictly greater than < 3 with our choice. We return -1 in the symetric cases.

func Equal 

func Equal(cg1, cg2 CGraph) bool

Equal reports if two systems have the same set of edges, compared using ==. Note that two DCS with different Names slices can be equal.

Types

type Arc 

type Arc struct {
	Start  int
	End    int
	Length Bound
}

Arc is the type of constraints between variables in the DCS, encoding constraints of the form: End - Start ≤ Length.Value. The comparison is strict if the Bound operation is (and reciprocally). The only operation we use in edges are LTHAN (strict inequality) and LTEQ (weak inequality).

type Bound 

type Bound struct {
	Operation
	Value int
}

Bound is the type of bounds in a time interval.

func BAdd 

func BAdd(b1, b2 Bound) Bound

BAdd returns the sum of two bounds.

func BMax 

func BMax(a, b Bound) Bound

BMax returns the maximum of a and b.

func BMin 

func BMin(a, b Bound) Bound

BMin returns the mininum of a and b.

func BSubstract 

func BSubstract(b1, b2 Bound) Bound

BSubstract computes the diference, b1 - b2, between two bounds.

func (Bound) PrintLowerBound 

func (b Bound) PrintLowerBound() string

PrintLowerBound returns a textual representation of a bound used as a lower bound constraint, such as "4 <" or "5 ≤".

func (Bound) PrintUpperBound 

func (b Bound) PrintUpperBound() string

PrintUpperBound is the dual of PrintLowerBound and returns a representation of a bound used as a lower bound constraint.

func (Bound) String 

func (b Bound) String() string

String returns a human-readable description of the value in b with a superscript decoration to indicate if the bound is strict (e.g. 8⁺) or weak (8⁼)

type CGraph 

type CGraph struct {
	SAT   bool          // true if system is satisfiable
	Names []string      // Name of variables; 0 is for the start variables.
	D     []Bound       // Feasible solution.
	Edges map[int][]Arc // Edges[i][j] = c represents the constraint zj - zi ≤ c.
}

CGraph is the type of DCS encoded using directed graph between variables. We check satisifability by looking at the shortest distance between every node. We rely on the fact that the system is satisifable if and only if there are no cycles of negative length. We consider a "virtual" node (src) that is at distance 0 from every vertex and compute the minimal distance from src. Hence, this distance will be a negative integer -d in practice. This value is recorded in the slice D and can be interpreted as a feasible solution that maximize each variable.

func NewDCS 

func NewDCS() CGraph

NewDCS returns a new system containing only the (default) start variable and no constraints.

func ReadSMTLIB 

func ReadSMTLIB(r io.Reader, strict bool) (CGraph, error)

ReadSMTLIB parses an input SMT specification incrementally and adds constraints in a DCS. It also keeps an association list between variables names and their index to check that we do not declare the same variable twice. If the strict parameter is true, the function stops as soon as the system is not satisfiable. If false, we parse the entirety of the specification.

func (*CGraph) Add 

func (cg *CGraph) Add(start int, end int, op Operation, n int) bool

Add adds a constraint (end - start op n) to the graph, where op is one of {<, <=, =, >=, >}, and returns false if the resulting system is not satisfiable. We assume that start and end are both valid variable indices.

func (*CGraph) AddNVar 

func (cg *CGraph) AddNVar(n int)

AddNVar adds n new variables with names z(i) ... z(i+n), where i is the index of the first fresh variable. We start counting from 1, meaning that the first variable added is z(1), with the convention that z(0) is an alias for the start variable. Like with AddVars, we add the constraint that their values are all positive.

func (*CGraph) AddVars 

func (cg *CGraph) AddVars(names ...string) error

AddVars adds new (top) variables with the constraint that their value is positive. We assume that the names are different from each other, and different from the variables already defined in [cg.Names].

func (CGraph) Clone 

func (cg CGraph) Clone() CGraph

Clone returns a deep copy of a DCS graph.

func (*CGraph) CompareVarWith added in v0.9.1 

func (cg *CGraph) CompareVarWith(n int, op Operation, d int) bool

CompareVarWith returns true if the system cg is satisifiable after adding the constraint "z(n) op d", but does not modify cg. For instance, when the operation is LTEQ, this function returns true if it is possible for z(n) to be less or equal than d in a feasible solution. We assume that n is a valid variable index.

func (*CGraph) ExecZ3 

func (cg *CGraph) ExecZ3() (bool, string)

ExecZ3 executes the command z3 on a SMT script generated from cg. We assume that z3 is installed locally and can be resolved by exec.LookPath (see documentation for exec.Command). We return true if the system is satisfiable, by a call to "(check-sat)", and false otherwise. When satisifiable, the second returned value is a string representation of the feasible solution, by a call to "(get-model)". Otherwise it is the error message returned by z3.

func (CGraph) PrintFeasible 

func (cg CGraph) PrintFeasible() string

func (CGraph) PrintSMTLIB 

func (cg CGraph) PrintSMTLIB() string

func (CGraph) PrintSystem 

func (cg CGraph) PrintSystem() string

func (CGraph) Truncate 

func (cg CGraph) Truncate(n int) CGraph

Truncate returns a new DCS obtained from cg by deleting every variables except the last n. The remaining variable with the smallest index taking the role of start. We return an empty DCS if n is nul and we return a deep copy of cg if n is larger than the number of variables in cg. Otherwise, the result is a system with exactly n variables.

func (CGraph) Unique 

func (cg CGraph) Unique() Key

Unique creates a unique key from a DCS. Useful for quickly checking equality between DCS when we need to compare the same systems more than once.

type Key 

type Key unique.Handle[string]

Key is a unique identifier for each DCS generated using the unique package from the standard loibrary.

func (Key) Value 

func (dk Key) Value() string

type Operation 

type Operation uint8

Operation is the type of possible comparison operators. We only use < and ≤ in our encoding into graph, and when printing a system, but allow the use of the other operators when defining the set of constraints. For instance, we allow equality constraints (that can be expressed as a conjunction of two comparison), but we do not support "distinct" (≠), since it would require a disjunction. 

const (
	LTHAN Operation = iota // less-than, <
	LTEQ                   // less-than or equal, ≤
	EQ                     // equal, =
	GTHAN                  // greater-than, >
	GTEQ                   // greater-than or equal, ≥
)

func ReadOperation 

func ReadOperation(s string) (Operation, error)

ReadOperation parses an operation names and returns the right value. It returns an error if the operator is not one of <, <=, >, >= or =.

Source Files

View all Source files

Directories

Path Synopsis
internal
set
Package set provides primitives for operating on sparse sets of integer values, implemented as a sorted slice of int.
 Package set provides primitives for operating on sparse sets of integer values, implemented as a sorted slice of int.

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL
go.dev uses cookies from Google to deliver and enhance the quality of its services and to analyze traffic. Learn more.