(Early) Draft
Using ToQ
ToQ is a High Level Language (HLL) for expressing
certain types of optimization problems for execution on a D-Wave
Quantum Computer System™. It manages most of the details of program
preparation for the D-Wave without user interaction — this is
a major goal of the language: to make it easy to use
the D-Wave by allowing users to focus on their areas of expertise, not
the interesting but intricate details of how the D-Wave quantum
computing system works.
ToQ programs are hybrids, meaning that part of the
program runs on the host system, and part runs on a D-Wave. That
is,
ToQ is an interpreter which runs in concert with, and
acts as an intermediary for, a host classical system and a D-Wave
Quantum Computer System. However, it does many operations (e.g.,
Sin, BitCount, LCM, BitMask, Sqrt, VectCompare, ...) at full
compiled code speed.
This document has four major components, each liberally sprinkled
with links for exploring topics and sample programs in detail, then
provides links for "jumping back."
- A "cookbook" for building some starter ToQ programs
and introducing the language features via simple examples
- A series of sections which can serve as a reference manual and
describe several of the language features in more detail.
- The Help/Index, from which a user can
easily jump to any topic of interest.
- An Olio section which contains a variety of
detailed information about selected ToQ language
topics. This section is not in any order, and is not intended for
serial review, but rather serves as a depository for many of the links
from the first three sections.
This document can serve as a cookbook for beginners (the early
chapters), but the later chapters describe the language characteristics
in a more formal (reference manual) manner.
In the early chapters, new ideas and sample code are presented as
needed (although they are also grouped together in navigable
links). The cookbook component may be ideal for beginners, but it
can also be useful for any experience level. The
document contains numerous examples and links for navigating easily to
points of interest. The
Help/Index provides links to hundreds of
help topics, and can be particularly helpful for looking up a detail,
then returning to the main text. The final section (titled
Olio) is not meant for serial review, but rather it is a collection
of a variety of topics that the reader would "click" to, read, then
head back to the point of departure via the [Back] button.
A ToQ program is a collection
of asserts acting on boolean variables.
The asserts define an optimization problem of
interest, and
ToQ finds the set(s) of boolean variable
values that satisfy all the asserts. This is the key concept for
developing and understanding
ToQ programs.
ToQ can be run as a standalone program or as a
program-callable library function.
For beginners, a good way to start would be to review the
Rules,
Data Types, and
Vignettes sections, followed by looking at
the various Sample code chapters.
(Early) Draft
Copyright © 2016 D-Wave Systems, Inc.
Cookbook
(Early) Draft
ToQ is a standalone or program-callable translator. It accepts
a C-like syntax which controls a series of assert
statements. The asserts act on logical entities (booleans) which
define an optimization problem. The collection of run-time active
asserts are transformed internally and presented to the D-Wave
system, which finds the optimal solution to the input problem,
and the results (values of the booleans) are passed back to the
caller.
- Input is case-insensitive (although input case is retained
for output presentation).
- Blanks and tabs are ignored.
- Statements are terminated by the end-of-line.
- Variable names are 1−12 characters from (a-z, A-Z, 0-9), and the
first character must be alphabetic. The only exception is that
the first character of constraint variables (bool:, mbool:, bmask:)
is "@" which is followed by 1−11 characters from (a-z, A-Z,
0-9).
- The valid alphabet
is a-z, A-Z, 0-9, #+-*/\^%~|&()!=<>@:.,
The newline (\n) and tab (\t) characters are also valid. The
linefeed character (\r) common on Window systems is silently ignored.
The underscore character ("_") is only valid as a line
Continuation character.
- Using an uninitialized variable is an error (constraint
variables are automatically initialized).
- A comment begins with the "#" character, which may
appear anywhere on a line. The rest of the line is ignored (and
thus the comment ends at the end of the line).
- Variables may be the arguments to functions. Functions may
be the arguments to functions.
- All entities share a single name-space; thus, for example neither
sin nor pi are valid names.
- All declaration statements must appear before the first executable
statement. (Asserts are executable.)
- Bool variables (which can take on only the values (0,1)), are not
available for programmer use. They are used only in assert
statements and their values are set by the run-time system such that
all combinations of all the booleans are exercised. A
ToQ program searches for one or more sets of the boolean
values which make all the asserts TRUE.
- Each ToQ program should contain two or more
assert statements.
- Each assert statement must contain two or more boolean variables.
- Each boolean must appear in two or more "contributing" asserts.
A contributing assert is one that can be evaluated as both
TRUE and FALSE for different sets of boolean values. For
example, given bools (@a,@b,@c), assert: @a+@b+@c <= 2 may
be either TRUE or FALSE, but assert: @a+@b > 3 is always
FALSE (this would be flagged as an input error).
- Bool variables (0,1) can be only used in assert statements.
But note that they can utilized both arithmetically via {+,-,*,...}
and logically via {&,|,>,<,...}. Groups of boolean can also be
utilized - e.g., assert: (((@a + @b + @c) > 1) || (@x & @y)).
Click here (or enter "toq -H operator") to see a list of all the
operators and the precedence rules.
- Assert statements can act only on bool: variables. When you
use extended boolean variables {mbool:, bmask:} in an assert statement,
ToQ silently converts them to an expression built from
hidden boolean variables. Use "listboolfuncs:" for a list of all
the functions which accept bool: variables as arguments.
- The last statement should be end: - all statements
after that will be silently ignored.
- When an error is detected during compile-time (e.g., mismatched
parentheses), a message is generated and the error-scan continues,
but no execution will occur. When an error is detected during
run-time, a message is generated, and the error scan may continue,
but no further execution will occur. All error conditions are
passed back to the caller.
- Enter "help: token" for a description of keyword "token,"
where token is a directive name, function name, constant name,
or a keyword. "token" must be at least three characters.
- Enter "print: var1 [,...]" for a list of the current value of
the listed variable name(s).
- Enter "printvars:" for a list of the current values of all the
variables.
- All non-executable statements (except comments) must contain
exactly one ":" character. Note that the assert statement
and control-flow statements also contain exactly one ":"
character.
- All executable statements (except asserts and control-flow) must
have exactly one replacement operator.
- Replacement (assignment)
statements in ToQ take the form:
var [repl] expression
where var is a regular variable name (i.e., a non-constraint
variable (constraint variables start with "@")).
The replacement operators [repl] are:
= |
+= |
−= |
*= |
/= |
&= |
|= |
>>= |
<<= |
Replacement operators work the same as in most other languages.
Note that since constraint variables may appear only in assert
statements, they may not appear in replacement statements. Here
is a sample:
omega += (Pi/2+Sqrt(zork))
is the same as
omega = omega + (Pi/2+Sqrt(zork))
Note that these four operators { &= |= >>= <<=
} work only on integers.
- Here are the basic operators. Click
Operators and Precedence Rules for details.
+ Add |
|
& Bitwise AND |
− Subtract |
|
| Bitwise OR |
* Multiply |
|
! Unary NOT |
/ Divide |
|
~ Bitwise NOT |
^ Raise to power |
|
% Remainder |
** Raise to power |
|
^^ Bitwise XOR |
- Executable statements, assert statements, and if statements may
use comparison and logical operators.
- Here are the comparison and logical operators. Click
Operators and Precedence Rules
for details.
== Equal |
|
!= Not equal |
&& And |
|
|| Or |
/\ And |
|
\/ Or |
> Greater than |
|
< Less than |
>= Greater than or equal |
|
<= Less than or equal |
---|
−> Implies |
|
<−> If-and-only-if |
Note that { &&, /\, ||, \/ } work only on integers.
- ToQ accepts five types of statements:
Simple assignment and control-flow
statements are interpreted and determine which assert statements
are active. Executable statements (Assignments, Control-flow,
and Asserts) may employ any of the
available 125+ functions and 75+ constants.
Click Functions and
Constants for lists of the functions and
constants and their descriptions. Alternately, enter
- toq -f for a list of the functions
- toq -F for a list of the functions with definitions
- toq -c for a list of the constants
- toq -C for a list of the constants with definitions
Here are some samples
bool: @b1, @b2, @b3, @b4, @b5
real: press, temp, dilbert, omega
# ~~~
omega = 34.5*PI
press = 744.3
temp = 199.3*Sqrt(press-150)
assert: Xor( @b2,@b5 )
assert: NOrMore( 1,@b1,@b3,@b5 )
if: (temp*Sin(omega*D2RADIANS) > 511) # Critically hot
assert: And( @b5, Or(@b2,@b3) )
else: # Temp in normal range
assert: TwoOf( @b1,@b3,@b5 )
assert: And( @b2, Or(@b1,@b3) )
endif:
assert: Xor( @b1,@b2 )
# ~~~
end:
Incidently, this code snippet would generate two warnings: (@b4
and dilbert are never used). If press was less than
150, a run-time error would have been captured (Sqrt of a negative
number), and the execution would be terminated with a message back to
the caller.
ToQ provides a wide range of help topics which can be
accessed via the commandline:
toq −H xyz
will give you information about topic
xyz. There are about
350 help topics. The
Help/Index section provides a (linkable)
list of all topics.
ToQ supports the variable types listed below.
All variables must be declared.
The
constraint variable types may not be
read or written by the programmer, rather they are set by the run-time
system and carry the result set(s). The other data types may
be initialized on the declaration line. All data must be
initialized before being used.
All declarations must appear
before the first executable statement.
All constraint variable names (of types
bool, mbool, bmask)
start with the "
@" character.
- bool:
Constraint variable type: boolean entities
(0,1) for use in assert statements
- int: 32-bit integer values
- real: 64-bit floating point values
- mbool:
Constraint variable type: multi-bit logical
entities for use in assert statements. Format is:
mbool: N, M, [i,] @var1, @var2, ...
where N, M, i are integers, (0 ≤ N < M
≤ 65,535), and each of the one or more variables in the list
may take on any value in (N,M).
The increment term (i > 0) is optional (default = 1),
and implies that the variable values skip through the range
(N−M) - thus the variables only take on values
N, N+i, N+2*i, ...
- bmask:
Constraint variable type: multi-bit logical
entities for use in assert statements. Format is:
bmask: J, K, @m1, @m2, ...
where J and K are integers, (0 < J < K ≤ 8), and each of
the one or more variables in the list is a K-bit word which
has exactly J 1-bits. Click here
for some examples.
- vect: A 1-D bit array of arbitrary length for use in a
ToQ program (a .toq file) or in a variable-value file (-z option or
initfile: directive). Size is set on the declaration, must be a
multiple of 32, and cannot be changed.
Vectors are actually packed bit arrays, which can be set,
interrogated, and interact with other vectors, as well as matrices
and tensors.
Direct access to vect
variables is restricted, but there are a variety of functions available
for data manipulation (enter: "toq -H vect"
or click here for details).
When using vectors in the functions listed below, they are
treated atomically, that is, operations interact with the entire
vector, so there is no need to be aware of word boundaries.
Some access is limited to (1-32) bits, and access may be over 32-bit
boundaries. Vect variables are uninitialized (using an
uninitialzed variable is a fatal error).
When initialized, the entire matrix must be covered.
Use the > symbol to fill out vectors (as in sample
3 below). Format is
vect: nBits, v1, v2, ...
where nBits is is an integer (>0) multiple of 32.
Here are some samples:
vect: 96, v1, v2, xmask = 0xAAAAAAAA,0xFFFFFFFF,37
vect: 64, ymask = 2*0xAFAFAFAF, tbar=2*0
vect: 256, hitVec = 0,MASK32,0,>MASK3202
- mtx:
A 2-D bit array of arbitrary length for use in a ToQ
program (a .toq file) or in a variable-value file (-z option or
initfile: directive). Size is set on the declaration
as nRows and nCols.
Matrices are actually packed bit arrays, which can be set,
interrogated, and interact with other matrices, as well as
vectors and tensors.
The dimensions cannot be changed.
When using matrices in the functions listed below, they are
treated atomically, that is, operations interact with the
entire tensor, so there is no need to be aware of word/row/column
boundaries. Direct access
to mtx variables is restricted, but there are a variety
of functions available for data manipulation
(click here for a list).
Mtx variables are uninitialized
(using an uninitialzed variable is a fatal error).
When initialized, the entire matrix must be covered.
Use the > symbol to fill out vectors (as in sample
3 below). Format is
mtx: nRows,nCols, m1, m2, ...
where "nRows" is an integer (>0) and "nCols" is
an integer multiple of 32. Here are some samples:
mtx: 16,96, m1, m2, mMask = 0xAAAAAAAA,47*0
mtx: 30,64, ymask = 60*0xAFAFAFAF, zbar = 60*0
mtx: 12,128, tPush = >MASK3202, tPull = >MASK32
- tnsr:
A 3-D bit array of arbitrary length for use in a ToQ
program (a .toq file) or in a variable-value file (-z option or
initfile: directive). Size is set on the declaration
as (nx,ny,nz),
internally called rows, columns, stacks.
(nx,ny,nz) are
set at compile-time and cannot be changed.
Tensors are actually packed bit arrays, which can be
set, interrogated, and interact with other tensors,
as well as vectors and matrices.
Direct access to tensor variables is restricted, but
there are a variety of functions available for data
manipulation (click here for a list).
When using tensors in the functions listed below, they are
treated atomically, that is, operations interact with the
entire tensor, so there is no need to be aware of
word/row/column/stack boundaries.
Tensor variables are uninitialized (using an uninitialzed
variable is a fatal error). When a tensor is inititialized,
the entire tensor must be covered. Use the >
symbol to fill out tensors (as in sample 2).
The format is
tnsr: nx,ny,nz, t1, t2, ...
where nx, ny, nz are integers (>0). Here are some samples:
tnsr: 8,8,10, t1, t2 = 0x6789FFFF, -1, 0, >0x55555555
tnsr 4,5,6, tBox = >MASK32
- intp: 32-bit integer values (post processing
only). Automatically initialized to zero. May be read
and written by the programmer. May be set to any combination
of regular and constraint variables.
- realp: 64-bit floating point values (post processing only). Automatically initialized to zero. May be read
and written by the programmer. May be set to any combination
of regular and constraint variables.
- vectp: Same as "vect:" except:
- may be used only after a "post:" directive
- are automatically initialized to zero
- may use any combination of regular and constraint vars
(vect: variables may not reference constraint vars)
- mtxp: Same as "mtx:" except:
- may be used only after a "post:" directive
- are automatically initialized to zero
- may use any combination of regular and constraint vars
(mtx: variables may not reference constraint vars)
- tnsrp: Same as "tnsr:" except:
- may be used only after a "post:" directive
- are automatically initialized to zero
- may use any combination of regular and constraint vars
(tnsr: variables may not reference constraint vars)
Also, constants may be declared using the
const: directive
(only one per line).
Const: variables are read-only.
Here are some sample declaratons:
bool: @a, @b, @glorp
int: i, j, counter, numb = 3
real: x, gamma = 344.561, zorro = 2, pink
const: NPATHS = 12
const: OMEGA2 = 1.4556
Reminder:
A ToQ program is a
collection of asserts acting on boolean variables.
Since 42 is the "Answer to the Ultimate Question of Life, The
Universe, and Everything," let's build our first program to find some
factors of this important number, and let's limit ourselves to 3-bit
factors (call them A and B). We can use booleans to represent
the bits, and thus A := (@a1+2*@a2+4*@a3), and B := (@b1+2*@b2+4*@b3),
and build
an assert to define the problem. Recall that all variables
must be declared (before the first executable statement), so we must
first declare the variables we use to represent the two multiplicands
(each being made up of 3 bits). All boolean variable names
start with the "
@" character - thus we can start our program
with the declaration statement:
bool: @a1,@a2,@a3, @b1,@b2,@b3
which allows us to define our multiplicands as three bits each
(with one boolean representing each bit).
Boolean variables may not be read or written by the programmer,
rather they are used (only) in assert statements and the system
sets their values such that each set of boolean values produces
a TRUE in all the assert statements in the program. Now we are
ready to build our assert statement (using the keyword
assert:).
An assert statement contains an expression which must
be a function of multiple boolean variables.
Each assert statement is evaluated for all the possible combinations
of values for all the boolean variables it contains.
An expression which evalutes to zero is considered FALSE, all others
are TRUE. The system filters
out the FALSEs, and the sets of boolean variable values which
evaluate to TRUE for all the assert statements in the program
represent the results. Our first assert statement can
then be:
assert: (((@a1+2*@a2+4*@a3) * (@b1+2*@b2+4*@b3)) == 42)
All
ToQ programs must have
end: as their last
statement. Since it is always a good practice for programs to
contain descriptive comments, our entire first program can be:
# ~~~ factor42.toq ~~~
#
# Find two 3-bit factors of 42
#
bool: @a1,@a2,@a3, @b1,@b2,@b3
# ~~~
assert: (((@a1+2*@a2+4*@a3) * (@b1+2*@b2+4*@b3)) == 42)
# ~~~
end:
You may wish to create a version of this program and run it yourself
to see what the answers are. Be sure to name the file with
a
.toq suffix (e.g., xyz.toq). Then, to execute it,
enter
toq -i xyz.toq
For a full, mouse-ready version of this sample code, click
here.
Below is the expected result. The program had six boolean
variables, therefore there were 2
6 possible solutions,
of which only two satisfied the assert statement. By
converting the booleans into base-10 integers, we see that
the two solutions were (6,7) and (7,6).
First Solution Set
======================
1) @a1 0
2) @a2 1
3) @a3 1
4) @b1 1
5) @b2 1
6) @b3 1
2 Solution Sets
========================
All variables are bools
1) @a1 0 1
2) @a2 1 1
3) @a3 1 1
4) @b1 1 0
5) @b2 1 1
6) @b3 1 1
We can garner some important information from this very simple
example. The two most important points are in green:
- A ToQ program is a
collection of asserts acting on boolean variables.
- A ToQ program is itself
the solution. That is, you do not need to tell the
program what to do, what steps to take when, et cetera. Executing
the ToQ program does all the steps of trying all the
combinations of all the boolean variables and all the communication
with the D-Wave. Essentially, when the D-Wave drops out of
the quantum state of superposition, it "collapses" to the solution.
- A ToQ-language program filename has .toq as
its suffix.
- A given program may have more than one solution.
- Every time we add another boolean variable, the solution
space doubles in size.
- ToQ is actually a hybrid program, with part of the
execution (e.g., parsing, error checking, problem setup, submission,
answer retrieval) occurring on your local machine, and the actual
solution to the optimization problem occurring on the D-Wave.
- The user did not need to know anything about the size,
interconnect, quantum nature, or other attributes of the
underlying D-Wave hardware.
- The underlying D-Wave hardware is probablistic. For this
simple problem, sometimes we might get (6,7) and (7,6), and other
times we might get (7,6) and (6,7).
Here are a bunch of ToQ code snippets. Some of them may contain
errors - can you spot them? This objective of this exercise
is to expose the beginner to some frequently-occurring errors and
typos before building her first ToQ programs.
int: a, b a = 17 bool: @y3,
@y4, @ynot |
|
real: x1, x2 x1 = 51.33 x2 =
sin(sqrt((x1-2)*(x1+2)) |
|
bool: @a, @b assert: ((@a+@b) > 3) |
|
real: acre, tBar, x, Acre, beta |
|
real: @x, @y x = sqrt(PI*y) |
|
bool: @q, @b int: pp, kk kk = 37 pp
= kk*(@a+@b) |
|
int: @pp, @kk kk = 17 pp = kk*((kk1−1)/2) |
|
real: ee = 1.057, ff = 17.3 assert: (ee > ((ff+1)/ff)) |
|
bool: @r, @s assert: (sqrt(2*PI-4*(@r+@s)) > 1) |
|
bool: @looney, @tooney @looney = 7 |
Click here for answers. See the next
section for sample Error and Warning messages.
When you run a ToQ program, the first thing you should
do is check the last two lines of the Dayfile (Summary),
which should be the last two lines of output. When an error
has been detected (whether at "compile-time" or "run-time"),
a message is generated and execution of the problem is
abandoned, although error-checking may continue.
It is a good practice to always check/correct
the first error first, since it may induce or hide other errors.
When an error or warning has been detected, a dump of the current
variable values will be generated. Below are three sample codes
which show the format of the error and warning messages (the messages
are shown in red here so they stand out).
- A "compile-time" error message
- A "run-time" error message
- A warning message
1 # --- err003.toq --- Regression test
2 int: a,x
3 bool: @c, @d, @e, @f
4 a = 33
5 x = sqrt(x+y)
6 assert: ((@c+@d) > (@e+@f))
7 end:
ToQ: ####> Error at line 5: "x = sqrt(x+y)"
--> "y" is not declared
-------------------------------------------------------------
| |
| ToQ: Partial error scan may continue - but no execution |
| |
-------------------------------------------------------------
1 # --- err011.toq --- Regression test
2 real: a,x,y
3 bool: @c, @d, @e, @f
4 assert: ((@c+@d) > (@e+@f))
5 a = 31
6 x = 9.79*PI
7 y = sqrt(x-a)
8 if: (y > 3)
9 assert: (@c == @e)
10 endif:
11 end:
This code produces the output below (the error message is shown
in red). When an error occurs,
ToQ dumps out the values of the variables at the point
of error. And note that y is shown as un-initialized
because the point of error was in the Sqrt function, and
thus execution stopped there.
ToQ: \\\\\ Fatal Runtime Error
///// at line 7: "y = sqrt(x-a)"
--> Sqrt(-0.243808) => Square root of a negative number
-------------------------------------------------------------
| |
| ToQ: Partial error scan may continue - but no execution |
| |
-------------------------------------------------------------
7 Variables (4 constraints, 3 regulars)
Decl Scan Runtime Variable
Type Src Line Refs Refs Name Value
---- --- ---- ---- ------- -------- ---------
1) real Pgm+ 2 3 2 a 31
2) real Pgm+ 2 3 2 x 30.7562
3) real Pgm+ 2 2 1 y Un-init! <---
======================
| |
| ErrorCount: 1 |
| No execution |
| |
======================
(qOp 2.2)
ToQ Summary v4.4.2: 14:11 Tue Aug23,16
=============== Tstamp: 14:12 Tue Aug23,16
err003.toq Input file
11 lines (5 executables, 0 directives)
PreQuantum Analysis only (16 cases)
4 Active bool variables
3 Regular variables (real: 3, int: 0)
2 Assert statements
20 Assert evaluations
19 Other evaluations
0 Warnings
1 Error <####################
And here is a sample file which generates a warning (shown in red):
1 # --- warn003.toq --- Regression test
2 bool: @a,@b, @c,@d, @e,@f, @g,@h
3 assert: ((@a+@b) > (@g+@h))
4 assert: ((@c+@d) > (@g+@h))
5 assert: And(Or(@c,@h),OR(@a,@d))
6 assert: @a+@b+@d > 1
7 end:
6 Solution Sets
========================
All variables are bools
1) @a 1 1 0 1 1 1 | 0:1 = 1:5 (84% 1s)
2) @b 1 0 1 1 1 1 | 0:1 = 1:5 (84% 1s)
3) @c 1 1 1 1 1 1 | const!
4) @d 0 1 1 1 1 1 | 0:1 = 1:5 (84% 1s)
7) @g 0 0 0 0 1 0 | 0:1 = 5:1
8) @h 0 0 0 0 0 1 | 0:1 = 5:1
----
5) @e --(not used)--
6) @f --(not used)--
Note: 1 constant constraint variable
@c = 1
ToQ: ::::> Warning
--> 2 constraint variables declared but not used
(Constraint variable dump)
8 Variables (8 constraints, 0 regulars)
Decl Scan Runtime Variable
Type Src Line Refs Refs Name Value
---- --- ---- ---- ------- -------- ---------
1) bool Pgm+ 2 4 40 @a ~~(0,1)~~
2) bool Pgm+ 2 3 24 @b ~~(0,1)~~
3) bool Pgm+ 2 3 32 @c ~~(0,1)~~
4) bool Pgm+ 2 4 40 @d ~~(0,1)~~
5) bool Pgm 2 1 0 @e Unused(0,1)
6) bool Pgm 2 1 0 @f Unused(0,1)
7) bool Pgm+ 2 3 32 @g ~~(0,1)~~
8) bool Pgm+ 2 4 48 @h ~~(0,1)~~
(qOp 2.2)
ToQ Summary v4.4.2: 14:11 Tue Aug23,16
=============== Tstamp: 14:28 Tue Aug23,16
warn003.toq Input file
7 lines (4 executables, 0 directives)
ToQ (internal) Solver
6 Solution Sets
6 Active bool variables (+2 unused)
0 Regular variables
4 Assert statements
56 Assert evaluations
408 Other evaluations
6/256 Results: Pass1/Cases (2.3%)
1 Warning <::::::::::::::
0 Errors
Consider the simple test case below, and look over the results.
This sample also illustrates that booleans can be used with
logical and arithmetic operators. Note that
booleans can only take on the values {0,1}, and thus (@a+@d)
can be any value in the set
{0,1,2}, while (@a&@d) can only be in the set {0,1}.
# sample.toq --- Regression test
# # Exercise And() and Or() #
bool: @a, @b, @c, @d
# ~~~
assert: And(Or(@a,@b), Or(@c,@d))
assert: @c != @d
assert: (@a+@d >= (@b+@c))
# ~~~
end:
|
|
|
4 Results |
|
1) @a 1 1 0 1
2) @b 0 0 1 1
3) @c 1 0 0 0
4) @d 0 1 1 1
|
|
For a full, mouse-ready version of this sample code, click
here.
Now we modify sample.toq (above) to create simpleIF.toq (the added code
is in blue), then run it. In this case, the IF-test has removed
the assert requiring @c and @d to be different,
and thus we get a different set of results. This sample also
illustrates how a variable can be initialized on the declaration line.
# simpleIF.toq --- Regression test
# # Simple IF-THEN-ELSE test #
bool: @a, @b, @c, @d
real: x = PI, y, z
# ~~~
y = Sqrt(x+2)
z = x-y
assert: And(Or(@a,@b), Or(@c,@d))
if: ((z*x)/3 > 3.11)
assert: @c != @d
endif:
assert: (@a+@d >= (@b+@c))
# ~~~
end:
|
|
|
6 Results |
|
1) @a 1 1 0 1 1 1
2) @b 0 0 1 1 0 1
3) @c 1 0 0 0 1 1
4) @d 0 1 1 1 1 1
|
|
For a full, mouse-ready version of this sample code, click
here.
Graph coloring is a component of the general discipline of graph
theory. It "...enjoys many practical applications as well as
theoretical challenges. Beside the classical types of problems,
different limitations can also be set on the graph, or on the way a
color is assigned, or even on the color itself. It has even
reached popularity with the general public in the form of the popular
number puzzle Sudoku. Graph coloring is still a very active field
of research." (ref: Wikipedia) For our sample codes, we will
use a simple map coloring exercise (an analog of graph coloring),
where we require that touching entities are different colors.
Consider this simple map which we want to color with {Red,Green,Blue}:
# --- map51.toq --- Class exercise
#
# Find a 3-color map for these 5 countries
#
# -------------------------
# | A |
# | ----------------- |
# | | B
| |
# | |---------------- |
# | | | | | |
# | | C | D | E | |
# | | | | | |
# -------------------------
#
We start by declaring a boolean for each of the 15 possible
Color/Country combinations.
bool: @Ared, @Ablue, @Agreen
bool: @Bred, @Bblue, @Bgreen
bool: @Cred, @Cblue, @Cgreen
bool: @Dred, @Dblue, @Dgreen
bool: @Ered, @Eblue, @Egreen
Next, we can use the OneOf() function to
assure that each country is exactly one color.
assert: OneOf(@Ared,@Ablue,@Agreen) # A may be only 1 color
assert: OneOf(@Bred,@Bblue,@Bgreen) # B may be only 1 color
assert: OneOf(@Cred,@Cblue,@Cgreen) # C may be only 1 color
assert: OneOf(@Dred,@Dblue,@Dgreen) # D may be only 1 color
assert: OneOf(@Ered,@Eblue,@Egreen) # E may be only 1 color
And finally, we need to enforce the rule that countries that share
a border must be different colors. We can use the
Nand() function for this rule, as follows
for A and B.
assert: Nand(@Ared,@Bred) # A,B not both red
assert: Nand(@Ablue,@Bblue) # A,B not both blue
assert: Nand(@Agreen,@Bgreen) # A,B not both green
These 3 lines need to be repeated for the other 7 borders: { AC,
AE, BC, BD, BE, CD, CE }.
(For the full, mouse-ready version of this sample code, click
here.)
Then we tack an end: on it
all and run it. This yields the following six solutions:
1) @Ablue 0 0 1 0 1 0
2) @Agreen 1 0 0 0 0 1
3) @Ared 0 1 0 1 0 0
4) @Bblue 0 0 0 1 0 1
5) @Bgreen 0 1 0 0 1 0
6) @Bred 1 0 1 0 0 0
7) @Cblue 1 1 0 0 0 0
8) @Cgreen 0 0 1 1 0 0
9) @Cred 0 0 0 0 1 1
10) @Dblue 0 0 1 0 1 0
11) @Dgreen 1 0 0 0 0 1
12) @Dred 0 1 0 1 0 0
13) @Eblue 1 1 0 0 0 0
14) @Egreen 0 0 1 1 0 0
15) @Ered 0 0 0 0 1 1
This result covers all the possible colorings, but somehow it is
not very satisfying. ToQ has set out to make
using the D-Wave easy, and yet this problem (which a five-year old
and a box of crayons could easily solve) took 34 lines of code.
The next section addresses this issue using this same problem.
In this section we introduce the use of the multi-bit data
type mbool.
We use mbools to address the simple map coloring problem
from Sample-03.
We use mbools to color our simple map. Mbools represent
a range of values, and bmasks represent bit masks with a specified
number of 1-bits. For our mapping problem, we can use a
simple declaration statement
mbool: 1,3, @A, @B, @C, @D, @E
This declares five variables corresponding to the five countries,
and each can take any value in {1,2,3}. This one line
replaces the first eight lines in our previous solution.
That is, each of @A, @B,...,@E now represent exactly one of three
colors. Note that this does not reduce the size of the
problems we are asking the D-Wave to solve, but the language now
implicitly does some work that the programmer had to do explicitly
in the previous solution. And the 24 asserts we used in the
previous solution to enforce the coloring of states with common borders
is now replaced by eight asserts. Note that the first
assert below
assert: @A != @B
is evaluated nine times (for each combination of the three values
for @A and the three values of @B).
Now we place the same restrictions on the other borders.
assert: @A != @B
assert: @A != @C
assert: @A != @E
assert: @B != @C
assert: @B != @D
assert: @B != @E
assert: @C != @D
assert: @D != @E
# ~~~
end:
As above, we append an end: statement and
run it. This yields the following six solutions:
1) mbool 1,3 @A 2 3 1 3 1 2
2) mbool 1,3 @B 3 2 3 1 2 1
3) mbool 1,3 @C 1 1 2 2 3 3
4) mbool 1,3 @D 2 3 1 3 1 2
5) mbool 1,3 @E 1 1 2 2 3 3
Note that whenever at least one of the result variables is not
a bool, all the result variable types are shown with the results.
For a full, mouse-ready version of this sample code, click
here.
This 10-line (8-assert) program is much easier for the
programmer to understand
and write (but note that the D-Wave is asked to solve the same
problem). Using mbool variables puts some of the work on
the language processor, relieving the programmer from some of
the repetitive drudgery of setting up this simple program.
While the 10-line program above is an improvement over the original
34-line version, we can build the same program with even less
busywork by using the Diff1() function,
as this 5-line (3-assert) version illutrates.
All three versions of this code make similar
computational demands on the D-Wave, and
all get the same answer. And as we have come to expect in
our programming careers, using a high-level language (ToQ
in this instance) saves us programmer development time, and often
it can be a significant amout of time.
mbool: 1,3, @A, @B, @C, @D, @E
# ~~~
assert: Diff1(@A, @B,@C,@E)
assert: DIff1(@B, @C,@D,@E)
assert: Diff1(@D, @C,@E)
# ~~~
end:
For a full, mouse-ready version of this sample code, click
here.
Diff1() is a
"Special" Function: a member of a group of
infrequently-used but very powerful functions.
They may occasionally make a "Deer in the Headlights" problem
seem like a "Piece of Cake."
Consider the simple Sudoku-like puzzle below. The
objective is to place 1,2,3 in each row and column. That
is, find values of A-F (in 1-3) that follow the rules of Sudoku.
___________________
___________________
| | | |
| | | |
| 1 | | |
| 1 | A | B |
|_____|_____|_____|
|_____|_____|_____|
| | | |
| | | |
| | | 2 | ==>
| C | D | 2 |
|_____|_____|_____|
|_____|_____|_____|
| | | |
| | | |
| | 3 | |
| E | 3 | F |
|_____|_____|_____|
|_____|_____|_____|
As usual, we start by declaring our variables. In this case,
using mbools seems most appropriate:
mbool: 1,3, @A, @B, @C, @D, @E, @F
Now we must build the assert statements (one for each row and column).
We can use the
Diff() function for this task.
assert: Diff(1,@A,@B)
# Row 1 entries different
assert: Diff(@C,@D,2)
# Row 2 entries different
assert: Diff(@E,3,@F)
# Row 3 entries different
assert: Diff(1,@C,@E)
# Col 1 entries different
assert: Diff(@A,@D,3)
# Col 2 entries different
assert: Diff(@B,2,@F)
# Col 3 entries different
Now we tack on an end: statement and run it to
produce these results:
1) mbool 1,3 @A 2
2) mbool 1,3 @B 3
3) mbool 1,3 @C 3
4) mbool 1,3 @D 1
5) mbool 1,3 @E 2
6) mbool 1,3 @F 1
For a full, mouse-ready version of this sample code, click
here. But note that this example
is just a mechanism to show one way to solve a Sudoku puzzle using
"classic" ToQ constructs.
Click here for a special sudoku:
directive, or
click here for an easier and much more
general way to solve Sudokus of various sizes (with alternate
alphabets).
You have 3 teenagers (Al, Bobby, Chris) whose ages (all integers)
combine in the following ways. Find their ages
2A - 3B + 2C = 0
3A + B - 4C = 1
Although this seems like it is 2 equations in 3 unknowns (Diophantine
Analysis could help us get the answer), we have additional information
in the ranges of their ages. A simple ToQ program
will allow us to look at all the possibilities at once, then
the D-Wave will "collapse" them down to the sets which satisfy
all the requirements.
As usual, we declare our variables first.
mbool: 13,19, @a, @b, @c
Here we see that the language processor is doing some of the work
for us (limiting the ages to the teen years). After you
finish this sample, you may wish to review
Sample-01 and try to do this problem
with only bool variables (it's not a pretty story).
Now we need to build assert statements to operate on the constraint
variables to satisfy the conditions of the problem:
assert: (2*@a-3*@b+2*@c) == 0
assert: (3*@a+@b-4*@c) == 1
We now tack an end: statement on and run it, which shows
us that there is only one solution.
Results
======================
1) mbool 13,19 @a 13
2) mbool 13,19 @b 18
3) mbool 13,19 @c 14
For a full, mouse-ready version of this sample code, click
here.
The post: directive initiates post processing, which grants
access to the values of the computed constraint variable sets.
This permits additional conditions to be applied to the sets of
constraint variables which have survived the initial "assert:"
statements. Special variables (of types "intp:" and "realp:") are
available only in the POST processing section - they may be used to hold
computed combinations of these formerly restricted variables.
Both "intp:" and "realp:" variables may be used on both the left- and
right-hand sides of replacement statements. All "intp;" and
"realp:" variables which are not set in their declaration statement are
initialized to zero. Normal "int:" and "real:" variables and
constraint variables may appear only on the right-hand side of
replacement statements in the POST section. "assert:" statements
may not be used in the POST section, but "assertp:" statements are
available in the POST section. They operate on any data
type. Only the constraint variable sets for which all the POST
section "assertp:" statements evaluate to TRUE are part of the final
solution. By default, all I/O (and other directives) are ignored in
the POST section (unless the postio:
directive has been encountered). See the
FedEx Problem or the
Simple TSP problem below for a sample use of
the post directive.
On SlothOrb, the third planet from the Slink, sloths are the
dominant life form, complete with cities, money, art, and smog.
Their coinage is: the Slent, the Trey (3 slents) and
the Urp (9 slents). Their paper money is the Slork (27 slents).
We want to know how many ways are there to make change for a
Slork. Assume we have a jar full of more than enough coins of each
type. First we build our variables, call them slent, trey
and urp for the coinage, and then variables for how many of each it
takes (@s, @t, @u). We will use mbools
to represent the number of each type. After we pass the problem
to the D-Wave, the results will be sets of (@s, @t, @u).
int: slent=1, trey=3, urp=9
mbool: 0,27, @s
mbool: 0,9, @t
mbool: 0,3, @u
Then we can simply assert the condition(s) we want and add the
end: statement.
assert: (@s*slent + @t*trey + @u*urp == 27)
end:
Now we are ready to run. The solution is
22 Solution Sets
======================
1 V X V X
1) mbool 0,27 @s 27 24 21 18 15 12 9 6 3 0 18 15 12 9 6 3 0 9 6 3 0 0 | 0-27
2) mbool 0,9 @t 0 1 2 3 4 5 6 7 8 9 0 1 2 3 4 5 6 0 1 2 3 0 | 0-9
3) mbool 0,3 @u 0 0 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 2 2 2 2 3 | 0-3
But we want more information − how many of them have at
least one of each coin, less than 11 slents and less than 6 urps?
What are they? Thus we want to look at all 22 solutions, and
determine how many of them fit our parameters. Using a
post: directive is a good way to attack this problem: it uses
the results of the above "collapse" and avoids using a heavy
assert statement (code in the post section uses an analog
of the assert, the assertp: statement).
In this case, we can use the simple InRangeEq
function. Now we just add these two statements before the
end:
post:
assertp: (InRangeEq(@s,1,10) && InRangeEq(@t,1,5) && (@u > 0))
(Note that we could have used three separate assertp statements in
place of the longer one above.)
This brings us to the final solution:
5 Solution Sets
========================
1) mbool 0,27 @s 9 6 3 6 3 | 3-9'
2) mbool 0,9 @t 3 4 5 1 2 | 1-5'
3) mbool 0,3 @u 1 1 1 2 2 | 1-2'
' partial range
Using the post: directive gives us two advantages:
- It allows the D-Wave to address a larger problem since we
do part of the work classically after the post:.
That is, we make better use of the power of the D-Wave to "collapse"
a large, complex problem into a solution by making the best use
of its resources (number of qubits).
- It allows us to classically determine which of the set of
solutions from the main part of the program meet our criteria.
This component may have processed a part of the problem which
may have been "more difficult to fit" into the D-Wave.
For a full, mouse-ready version of this sample code, click
here.
A special form of the assertp: directive
allows one to interrogate valid sets from above a post:
statement and pick out the maximum (or minimum) value based on
some criteria. These criteria are programmed into the
assert-like maximize: or
minimize: statement. These
statements differ from assert and assertp in that they
produce a computed result (not just 0 or 1), and the maximum
(minimum) result is retained, and its location and constraint
variable values are reported back to the caller.
Only one maximize or minimize statement may appear in a
ToQ program, and it must occur after a
post: directive. As with assertp directives,
maximize and minimize have access to the full set of constraint
variable values from the regular part of the program (i.e., those
asserts from above the post: directive). See
Sample-09 (The FedEx Problem) below
for a simple sample of maximize.
You have 5 packages to deliver (in a truck
with finite capacity). You want to maximize the priorities
of the packages you choose. The packages (in order) weigh
{ 813, 719, 120, 575, 235 } pounds, and their volumes are
{ 79, 78, 18, 72, 27 } cubic feet. The priorities are
{ 1, 2, 3, 2, 3 } where the higher the priority
number, the more important the package. Your truck can
carry 1550 pounds and has 179 cubic feet of space. For
each run, you want to maximize the sum of the priorities of
the packages on board. Without concern for packing nor for
distances, which packages do you take on your first trip?
As usual, our first task is to declare all the variables we will
need to describe our problem. In this case, we need a boolean
for each package (to see whether it is on the truck for this trip
or not), and also the {weights,volumes,priorities} for each package.
This is straightforward, as follows:
bool: @a,@b,@c,@d,@e
int: aw=813, bw=719, cw=120, dw=575, ew=235
int: av=79, bv=78, cv=18, dv=72, ev=27
int: ap=1, bp=2, cp=3, dp=2, ep=3
Note that the next section
(Reading External Files)
provides a way to hide some of the above busywork.
Now we are ready to determine which sets of packages can fit in
the truck (using assert statements to assure that the weight and
volume limits are not exceeded).
assert: (@a*aw + @b*bw + @c*cw + @d*dw + @e*ew) < 1550
assert: (@a*av + @b*bv + @c*cv + @d*dv + @e*ev) < 179
And finally, we want to look at all the sets which fit on the truck,
and choose the one with the highest priority summation. For
this task, we use the post: directive, then a
maximize: to pick the winner.
post:
maximize: (@a*ap + @b*bp + @c*cp + @d*dp + @e*ep)
We complete the program with an end: and run it. Here are the
results.
Pass1
22 Solution Sets
========================
All variables are bools
1 V X V X
1) @a 0 1 0 1 0 1 0 0 1 0 0 1 0 0 1 0 0 1 0 0 0 0 | 0:1 = 15:7
2) @b 0 0 1 1 0 0 1 0 0 1 0 0 1 0 0 1 0 0 1 0 1 0 | 0:1 = 14:8
3) @c 0 0 0 0 1 1 1 0 0 0 1 1 1 0 0 0 1 1 1 0 0 1 | 0:1 = 12:10
4) @d 0 0 0 0 0 0 0 1 1 1 1 1 1 0 0 0 0 0 0 1 1 1 | 0:1 = 13:9
5) @e 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1 1 | 0:1 = 13:9
Pass2
Max Result = 8
(#19 of 22 cases)
0 @a
1 @b
1 @c
0 @d
1 @e
Our first trip will have a priority sum of 8, will weigh 1,074 pounds,
and occupy 123 cubic feet. For a full, mouse-ready version of
this sample code, click here.
You can ask ToQ to read in file(s) of initialized
variables into your program. Note that only "regular" variables
(int:, real:) can be read, not constraint
variables (bool:, mbool:, bmask:). It can also hold
"prototype definitions" - a topic not covered yet in this
document. Here is a description: The first line contains three
fields ("sentinel", "show" and "N") − where "sentinel" must be
the 4-character string "vars", "show" is one of (0,1) for
(DoNotShow,Show) the contents of this file in the output, and "N" is
the number of lines. Then the next N lines contain the data for
one variable or one prototype per line. The format of these lines
is
Type VarName = Value
- or -
prototype: id, type, FuncName(type1,type2,type3)
(Enter: "toq -H prototype" for details on prototypes.)
The valid Type values are { int:, real:, const: }. Here is a
simple example:
vars 1 3
real: beta = 17.935
real: prob = 0.68
int: size = 42
Given a file ("vfile"), access it as follows:
Batch mode: toq -z vfile -i xyz.toq
-or-
Embedded mode: Include the line "initfile: vfile" at the beginning
of the program. Note that "varfile:" is an alias
for "initfile:" - so "varfile: vfile" also works
In the next section, a simple variable file will be used to keep the
program text simple.
This simple example illustrates the use of an
External Variable File and using the minimize: directive in a post processing clause.
Note that this is not intended as a general solution to the Traveling
Salesman Problem.
Consider five cities (A,B,C,D,E) with these distances between them:
Distances
A ===========
A B C D E
---------------------------
B E A | - 500 200 185 205 |
B | 500 - 305 360 340 |
C | 200 305 - 320 165 |
C D D | 185 360 320 - 302 |
E | 205 340 165 302 - |
---------------------------
First, we define a file (dist5) to hold the distance
data (and we assume that the distance (X → Y) is the same
as the distance (Y → X).
Here is how it could look:
vars: 1 10
int: ab = 500
int: ad = 200
int: ad = 185
int: ae = 205
int: bc = 305
int: bd = 360
int: be = 340
int: cd = 320
int: ce = 165
int: de = 302
For our ToQ program, the file dist5 can
serve as part of our declarations, so we use the
varfile: directive to read the
dist5 file. Now we must declare
a boolean for each pair of cities − at the end of the program,
the booleans which are TRUE will tell us the shortest path.
varfile: dist5
bool: @ab, @ac, @ad, @ae, @bc
bool: @bd, @be, @cd, @ce, @de
To set
up our problem, we must recognize that for a Traveling Salesman
problem solution, we must visit each city exactly once (including our
return to the original city). We can translate that into
a set of simple assert statements by realizing that each city must
have exactly two active paths (on the final solution) connected to
it. Thus we simply add these assert statements to assure
those conditions are met.
assert: TwoOf(@ab,@ac,@ad,@ae) # All the A paths
assert: TwoOf(@ab,@bc,@bd,@be) # All the B paths
assert: TwoOf(@ac,@bc,@cd,@ce) # All the C paths
assert: TwoOf(@ad,@bd,@cd,@de) # All the D paths
assert: TwoOf(@ae,@be,@ce,@de) # All the E paths
Now we need to find the full path, which touches each city exactly
twice and has the minimum length. We can use the
minimize: directive (with all the booleans
telling us which paths are in/out)
acting in the post: section (and we need
an end: statement). Each boolean will be either a zero or
one for each set which satisfied all the asserts. In the
post section, we interrogate all the sets which passed all the
asserts.
post:
minimize: (@ab*ab + @ac*ac + @ad*ad + @ae*ae + _
_ @bc*bc + @bd*bd + @be*be + @cd*cd + _
_ @ce*ce + @de*de)
end:
Here is the result:
Pass1
12 Solution Sets
========================
All variables are bools
1 V X
1) @ab 0 0 0 0 1 1 0 0 1 1 1 1 | 0:1 = 6:6
2) @ac 0 1 0 1 0 0 1 1 0 1 0 1 | 0:1 = 6:6
3) @ad 1 0 1 1 0 1 0 1 0 0 1 0 | 0:1 = 6:6
4) @ae 1 1 1 0 1 0 1 0 1 0 0 0 | 0:1 = 6:6
5) @bc 1 0 1 0 0 0 1 1 1 0 1 0 | 0:1 = 6:6
6) @bd 0 1 1 1 1 0 1 0 0 0 0 1 | 0:1 = 6:6
7) @be 1 1 0 1 0 1 0 1 0 1 0 0 | 0:1 = 6:6
8) @cd 1 1 0 0 1 1 0 0 1 1 0 0 | 0:1 = 6:6
9) @ce 0 0 1 1 1 1 0 0 0 0 1 1 | 0:1 = 6:6
10) @de 0 0 0 0 0 0 1 1 1 1 1 1 | 0:1 = 6:6
Min Result = 1220
(#3 of 12 cases)
0 @ab
0 @ac
1 @ad
1 @ae
1 @bc
1 @bd
0 @be
0 @cd
1 @ce
0 @de
=== End Post Processing === (Min = 1220)
The best path is (A → D → B → C → E →
A) which is 1220 miles (185+360+305+165+205).
For a full, mouse-ready version of
this sample code, click here.
The quant: directive (along with its partner, endquant:)
delineates a block of statements which act
together to prepare a problem for resolution by the D-Wave.
Each statement in the block is executed once for each
possible combination of the values of the constraint
(boolean and extended boolean) variables which appear
in the QUANT block. These results are combined with all the
other QUANT block results, then presented to the D-Wave,
which finds the sets of constraint variable values for which
all the assert statements are TRUE. Each QUANT block must
contain exactly one assert statement, and it must be the
last executable statement in the block. QUANT blocks
may not nest. A standalone assert statement behaves
as if it were in a QUANT block. Statements in a QUANT
block can read (but not write) constraint
variable values. Regular variables may be read and
written in a QUANT block, but changed regular variables
should not be read after a QUANT block (their values
may be unpredictable). A QUANT block must appear after
the last declaration statement and before a post:
statement (if any). QUANT blocks are syntactic constructs
which are typically used to simplify the text in an assert
statement by allowing boolean and other constraint variable
values to be combined. I/O is silently ignored in QUANT
blocks unless a quantio: directive has been encountered.
An assert statement in a QUANT block need not directly
reference boolean or other constraint variables so long as
its expression contains variables which are derivatives
of constraint variables. QUANT blocks may not be used
with autopartitioning (-QP option).
Quant blocks are supplied as a programmer aid (reducing the size
of assert statements and making them easier to read/understand).
In some cases, Quant blocks may simplify the work needed to be done by
the code which builds the data structures for the D-Wave to
ingest. The next section contains
a simple example.
Consider a problem which wants to use a series of computations
operating on constraint variables. ToQ rules
require that all constraint variable usage be limited to
assert statements. Using QUANT blocks relieves that
restriction. In the simple example below, we introduce
four int: variables to hold intermediate results and work in
the final assert statement (only one assert may be in a
QUANT block, and it must be the last executable statement).
int: n1, n2, n3, n4
Now we declare our constraint variables.
bool: @b1, @b2
mbool: 3,14,2, @m1
Now we can build our QUANT block. We use the
Max() and InRangeEq()
functions to perform simple computations on the regular
and constraint variables. The entire QUANT block is executed
for all combinations of the possible values of the constraint
varialbes. Note that it is OK that
the assert statement does not contain any explicit constraint
variables, the n4 variable is a function of the constraint
variables in the problem.
quant:
n1 = @b1+3*@b2
n2 = Max(n1,(@m1-6*@b2))
n3 = (@b1+@b2)*@m1
n4 = n1+n2+n3
assert: InRangeEq(n4,5,11)
endquant:
Of course, this program could contain more code (some of it
using the constraint variables in the QUANT block), but for
now we just add an end: statement and execute it (QUANT
blocks do not require any special options to enable them).
This leads to these results, which show the sets of constraint
variable values for which n4 is in the inclusive range
(5−11).
8 Solution Sets
=======================
1 V
1) bool @b1 1 0 0 1 0 0 0 0 | 0:1 = 7:2
2) bool @b2 0 1 0 0 1 0 0 0 | 0:1 = 6:3
3) mbool 3,14,2 @m1 3 3 5 5 5 7 9 11 | 3-11'
' partial range
For a full, mouse-ready version of
this sample code, click here.
ToQ takes a general optimization problem, transforms
it into a QUBO, and dispatches it to the D-Wave. The
transformation steps are size-dependent and may
be quite intricate. However, for
some problems, there are easier ways to convert a problem to a
QUBO. Map coloring (a subset of the general graph coloring
problems) is such a case. ToQ provides a
mechanism to convert a simple set of map information directly
into a QUBO. Put the data into a file with a .adj
suffix. Click here for a description
of the file format. A mouse-ready sample file
(nm.adj − for the counties
of New Mexico) can be found here.
nm.adj calls for 3 different 4-Color maps of the 33
counties of New Mexico. The requested colors are
{ Red, Green, Blue, Yellow }. To run this case, enter
toq -i nm.adj
Here is the output for this case:
33 Areas
4 Colors
3 ColorSets
-------------
B Y G Bernalillo | Y G R Harding | R B Y Roosevelt
R B Y Catron | R B Y Hidalgo | G R B San_Juan
G R B Chaves | B Y G Lea | B Y G San_Miguel
G R B Cibola | Y G R Lincoln | R B Y Sandoval
R B Y Colfax | G R B Los_Alamos | Y G R Santa_Fe
B Y G Curry | Y G R Luna | G R B Sierra
B Y G De_Baca | B Y G McKinley | B Y G Socorro
B Y G Dota_Ana | G R B Mora | Y G R Taos
Y G R Eddy | R B Y Otero | G R B Torrance
B Y G Grant | G R B Quay | B Y G Union
R B Y Guadalupe | B Y G Rio_Arriba | Y G R Valencia
Color Frequency Report
(1st ColorSet)
==========================
Red-(1) 7 (21.2%) Blue-(3) 11 (33.3%)
Greeen-(2) 8 (24.2%) Yellow-(4) 7 (21.2%)
(qOp 2.2)
ToQ Summary v4.4.2: 15:49 Tue Jul12,16
=============== Tstamp: 11:41 Sun Aug07,16
nm.adj Input file
49 lines (33 areas, 78 borders, 4 colors,
density: 2.36, difficulty: 3.7)
nmADJ.qubo Qubo input file created (sz=132,#n=132,#c=510)
nmADJ.qbout Qubo output file created
<0.1 Qbsolv CP-seconds
0 Errors
This section contains the skeletons of a number of simple test
cases, as well as results for each. Some of the problems
are easy, some are very easy, and some are tough. Most of
factor problems are straightforward, but factorx
may require some thought (to fit onto the target machine).
Note that since the
D-Wave is probablistic, your results may be different.
Each is mouse-ready − so you may pick them up, add the
code to solve the problem, and compare your answers to the
published results. The files are in alphabetic order
with the exception of map51, which asks for three different
solutions (with 36, 12, 5 lines of executable code).
# --- map51.toq --- Class exercise
#
# Find a 3-color map of the 5 counties in the map below
#
#
# _________________________
# | |
# | A |
# | ________________ |
# | | | |
# | | B | |
# | |_______________| |
# | | | | | |
# | | C | D | E | |
# |___|___|_______|___|___|
#
#~~~
#~~~
end: #==========================================
==== Result 1 - SolutionCode: 36 lines (not counting comments)
Results
============================
1) @ablue 1 0 0 1 0 0
2) @agreen 0 0 1 0 1 0
3) @ared 0 1 0 0 0 1
4) @bblue 0 1 1 0 0 0
5) @bgreen 1 0 0 0 0 1
6) @bred 0 0 0 1 1 0
7) @cblue 0 0 0 0 1 1
8) @cgreen 0 1 0 1 0 0
9) @cred 1 0 1 0 0 0
10) @dblue 1 0 0 1 0 0
11) @dgreen 0 0 1 0 1 0
12) @dred 0 1 0 0 0 1
13) @eblue 0 0 0 0 1 1
14) @egreen 0 1 0 1 0 0
15) @ered 1 0 1 0 0 0
(qOp 2.2)
ToQ Summary v4.14: 12:13 Sat Aug20,16
=============== Tstamp: 08:12 Tue Aug23,16
map51.toq Input file
63 lines (29 executables, 1 directive)
<.rc,env> Configuration info (Engine: c4-sw_sample)
15 Active bool variables
0 Regular variables
29 Assert statements
136 Assert evaluations
0 Other evaluations
6/32,768 Results: Pass1/Cases
0 Warnings
0 Errors
==== Result 2 - SolutionCode: 12 lines (not counting comments)
6 Results
============================
1) @a 1 1 2 3 2 3
2) @b 3 2 3 1 1 2
3) @c 2 3 1 2 3 1
4) @d 1 1 2 3 2 3
5) @e 2 3 1 2 3 1
(qOp 2.2)
ToQ Summary v4.14: 12:13 Sat Aug20,16
=============== Tstamp: 08:22 Tue Aug23,16
map52.toq Input file
31 lines (8 executables, 1 directive)
<.rc,env> Configuration info (Engine: c4-sw_sample)
0 Active bool variables
5 Constraint variables
10 bool 5 mBool 0 bMask
(10 constraintBools)
0 Regular variables
8 Assert statements (+5 generated)
128 Assert evaluations
0 Other evaluations
6/1,024 Results: Pass1/Cases (0.6%)
0 Warnings
0 Errors
==== Result 3 - SolutionCode: 5 lines (not counting comments)
6 Solution Sets
========================
1) @A 3 1 3 1 2 2 | 1-3
2) @B 1 2 2 3 3 1 | 1-3
3) @C 2 3 1 2 1 3 | 1-3
4) @D 3 1 3 1 2 2 | 1-3
5) @E 2 3 1 2 1 3 | 1-3
(qOp 2.1)
ToQ Summary v4.4.2: 08:49 Sun Jun26,16
=============== Tstamp: 08:48 Tue Aug23,16
map531.toq Input file
5 lines (3 executables, 0 directives)
<.rc,env> Configuration info (Engine: c4-sw_sample)
6 Solution Sets
0 Active bool variables
5 Constraint variables
10 bool 5 mBool 0 bMask
(10 constraintBools)
0 Regular variables
3 Assert statements (+5 generated)
1,172 Assert evaluations
1,172 Other evaluations
6/1,024 Results: Pass1/Cases (0.6%)
(10,3,128,13056) #(Bools,Asserts,Nodes{logical,total})
(128,128{102},102.00) Chain length (Min,Max{#},Avg)
0 Warnings
0 Errors
# --- dioph1.toq --- 1 eq in 2 unknowns
#
# Find x and y given 4x - 3y = 11
# x in (2-7), y in (3,9)
#
#~~~
#~~~
end: #==========================================
Results
================
1) @x 5
2) @y 3
# --- dioph23.toq --- Regression Test
#
# 2 eqs in 3 unknowns - integer solutions in ranges given
#
# 3x - y + 2z = 14 x in (3-6), y in (7-10)
# x + 2y - z = 15 z in (2-5)
#
#~~~
#~~~
end: #==========================================
Results
================
1) @x 4
2) @y 8
3) @z 5
# --- erkel.toq --- Class exercise
#
# Your daughter has been kidnapped and held for ransom
# by Eldor, the Emperor of the Evil Empire of Exonia.
# If you do not pay the ransom within 24 hours, or if you
# pay less than the demand, your daughter will be hidden
# in a dungeon for life. If you pay more than the demand,
# your daughter will be sentenced to watch Gomer Pyle reruns
# 16 hours/day for life. The target is [Ransom] Erkels.
# You own 8 sealed bags of Erkels [e1,e2,...,e8], time enough
# for only one trip, and no time to open/reconfigure the bags.
#
# Given the data below, how many ways (if any) can you select
# a group of bags to satisfy the ransom demands?
#
#~~~
int: e1 = 5, e2 = 27, e3 = 32, e4 = 34
int: e5 = 36, e6 = 38, e7 = 44, e8 = 59
int: ransom = 143
#~~~
end: #==========================================
Results
======================
1) @b1 0
2) @b2 1
3) @b3 0
4) @b4 1
5) @b5 0
6) @b6 1
7) @b7 1
8) @b8 0
# --- factor42.toq --- Regression Test
#
# Find two unsigned 3-bit integers whose
# product is 42. (Use bool: variables)
#
#~~~
#~~~
end: #==========================================
2 Results
===============
1) @a0 0 1
2) @a1 1 1
3) @a2 1 1
4) @b0 1 0
5) @b1 1 1
6) @b2 1 1
# --- factor42p.toq --- Regression Test
#
# Find two unsigned integers (in 1-10) whose
# product is 42. (Use extBool variables)
#
#~~~
#~~~
end: #==========================================
2 Results
===============
1) @a 7 6
2) @b 6 7
# --- factor43.toq --- Regression Test
#
# Find two unsigned 4-bit integers whose
# product is 42. (Use bool: variables)
#
#~~~
#~~~
end: #==========================================
4 Results
=================
1) @a0 1 0 0 1
2) @a1 1 1 1 1
3) @a2 1 1 1 0
4) @a3 0 1 0 0
5) @b0 0 1 1 0
6) @b1 1 1 1 1
7) @b2 1 0 1 1
8) @b3 0 0 0 1
8 bool variables, 2 of which are constant
1) @a1 = 1
2) @b1 = 1
# --- factor43p.toq --- Regression Test
#
# Find two unsigned integers (in 1-15) whose
# product is 42. (Use extBool variables)
#
#~~~
#~~~
end: #==========================================
4 Solution Sets
========================
1) @a 7 14 3 6
2) @b 6 3 14 7
# --- factor5.toq ---
#
# Find two factors of 899
#
#~~~
#~~~
end: #==========================================
2 Solution Sets
========================
1) @a 31 29
2) @b 29 31
# --- factor6.toq ---
#
# Find two factors of 2,773 (both less than 65)
#
#~~~
#~~~
end: #==========================================
2 Solution Sets
========================
1) @a 47 59
2) @b 59 47
# --- factor7.toq ---
#
# Find a,b (both <= 128)
# such that a*b = 7,519
#
#~~~
#~~~
end: #==========================================
2 Solution Sets
========================
1) @a 797 709
2) @b 709 797
# --- factor8b.toq ---
#
# Find a,b (both < 150)
# such that a*b = 5,069
#
#~~~
#~~~
end: #==========================================
2 Results
=============
1) @a 37 137
2) @b 137 37
# --- factorafactora.toq ---
#
# Find two factors of 11,433
# (hint: both are less than 128)
#
#~~~
#~~~
end: #==========================================
2 Solution Sets
========================
1) @a 103 111
2) @b 111 103
# --- factorb.toq ---
#
# Find two factors of 13,081
# (hint: both less than 128)
#
#~~~
#~~~
end: #==========================================
2 Solution Sets
========================
1) @a 127 103
2) @b 103 127
# --- factorx.toq ---
#
# Find two integers (1 < (a,b) < 800)
# such that a*b = 565,073
#
#~~~
#~~~
end: #==========================================
2 Solution Sets
========================
1) @a 709 797
2) @b 797 709
# --- latin.toq --- Regression test
#
# A Latin Square is an n x n array of n different symbols, such
# that each symbol occurs once per row and once per column.
#
# Using ToQ -- construct a 3 x 3 Latin Square
#
#~~~
#~~~
end: #==========================================
12 Solution Sets
========================
1 V X
1) @a 2 1 1 3 1 2 2 3 1 3 3 2 | 1-3
2) @b 1 3 2 1 2 3 1 2 3 2 1 3 | 1-3
3) @c 3 2 3 2 3 1 3 1 2 1 2 1 | 1-3
4) @d 1 2 3 1 2 1 3 2 3 1 2 3 | 1-3
5) @e 3 1 1 2 3 2 2 1 2 3 3 1 | 1-3
6) @f 2 3 2 3 1 3 1 3 1 2 1 2 | 1-3
7) @g 3 3 2 2 3 3 1 1 2 2 1 1 | 1-3
8) @h 2 2 3 3 1 1 3 3 1 1 2 2 | 1-3
9) @i 1 1 1 1 2 2 2 2 3 3 3 3 | 1-3
# --- maha1.toq --- Regression test
#
# Problem from Mahaviracharya (9th century Indian Monk)
#
# In the forest, 37 numerically equal heaps of apples were seen
# by travelers. After 17 apples were removed, the remainder was
# divided evenly (no partial apples) among 79 travelers. Each
# heap has (50 < H < 100) apples. How many apples per traveler?
#
#~~~
#~~~
end: #==========================================
Results
======================
1) @heaps 88
2) @travs 41
# --- max1.toq --- Regression Test
#
# You have 5 packages to deliver (in one trip in a truck
# with finite capacity). You want to maximize the priorities
# of the packages you choose. The packages weigh
# { 813, 719, 120, 575, 235 } pounds, and their volumes are
# { 79, 78, 18, 72, 27 } cubic feet. The priorities are
# { 1, 2, 3, 2, 3 } where the higher the priority
# number, the more important the package. Your truck can
# carry 1550 pounds and has 179 cubic feet of space. Without
# concern for packing, which packages do you take?
#
#~~~
#~~~
end: #==========================================
Max Result = 8
(#19 of 22 cases)
0 @a
1 @b
1 @c
0 @d
1 @e
=== End Post Processing === (Max = 8)
# --- prime.toq --- regression test
#
# Find a prime number which is the
# sum of 4 consecutive primes
#
# Do not attempt this problem.
# Not for the faint of heart.
#~~~
#~~~
end: #==========================================
# --- prime2.toq --- regression test
#
# 0 and 10 are know as "prime decades" since they have exactly
# four prime numbers in the range [(10*x) - (10*x+9)], namely
# {2,3,5,7} and {11,13,17,19}. Can you find any other prime
# decades in the other 48 decades below 500?
#
#~~~
#~~~
end: #==========================================
2 Solution Sets
========================
1) @base 10 19
# --- ramanujan.toq --- Regression Test (heavy duty)
#
# I live on a street where the houses are numbered
# consecutively (1,2,3,...).
#
# The are more than 50 houses, and less than 500 houses.
#
# The sum of the house numbers lower than mine is the same
# as the sum of the house numbers greater than mine.
#
# What is my house number, and how many houses on my street?
#
#~~~
#~~~
end: #==========================================
Results
======================
1) @a 204
2) @b 288
# --- range1.toq --- Regression Test
#
# Find two 3-digit primes less than 125 (x,y)
# such that (11,000 <= x*y <= 11,300)
#
#~~~
#~~~
end: #==========================================
6 Solution Sets
========================
1) @x 109 107 109 103 101 103
2) @y 101 103 103 107 109 109
# --- sud3.toq --- Regression Test
# ___________________ ___________________
# | | | | | | | |
# | 1 | | | | 1 | A | B |
# |_____|_____|_____| |_____|_____|_____|
# | | | | | | | |
# | | | 2 | --> | C | D | 2 |
# |_____|_____|_____| |_____|_____|_____|
# | | | | | | | |
# | | 3 | | | E | 3 | F |
# |_____|_____|_____| |_____|_____|_____|
#
#~~~
#~~~
end: #==========================================
Results
=================
1) @A 2
2) @B 3
3) @C 3
4) @D 1
5) @E 2
6) @F 1
# --- sud4.toq --- Regression Test
# _________________________ _________________________
# | | | | | | | | | |
# | 1 | | | | | 1 | A | B | C |
# |_____|_____|_____|_____| |_____|_____|_____|_____|
# | | | | | | | | | |
# | | | 2 | | | D | E | 2 | F |
# |_____|_____|_____|_____| --> |_____|_____|_____|_____|
# | | | | | | | | | |
# | | | | 1 | | G | H | I | 1 |
# |_____|_____|_____|_____| |_____|_____|_____|_____|
# | | | | | | | | | |
# | | 4 | | | | J | 4 | K | L |
# |_____|_____|_____|_____| |_____|_____|_____|_____|
#
#~~~
#~~~
end: #==========================================
2 Solution Sets
========================
1) @A 2 3
2) @B 3 4
3) @C 4 2
4) @D 4 3
5) @E 1 1
6) @F 3 4
7) @G 2 4
8) @H 3 2
9) @I 4 3
10) @J 3 2
11) @K 1 1
12) @L 2 3
# --- teenagers.toq --- Regression test
#
# You have 3 teenagers (Scholar, Jock, Beauty)
# Using ToQ, find the age of each teen given:
#
# 2S - 3J + 2B = 0
#
# 3S + J - 4B = 1
#
#~~~
#~~~
end: #==========================================
Results
=================
1) @S 13
2) @J 18
3) @B 14
# --- tsp53.toq --- Regression Test
# Distances
# A ===========
# A B C D E
# ---------------------------
# B E A | - 500 200 185 205 |
# B | 500 - 305 360 340 |
# C | 200 305 - 320 165 |
# C D D | 185 360 320 - 302 |
# E | 205 340 165 302 - |
# Traveling Salesman ---------------------------
# Problem (Easy-Peasy)
# ~~~
int: ab=500, ac=200, ad=185, ae=205, bc=305
int: bd=360, be=340, cd=320, ce=165, de=302
#~~~
end: #==========================================
(#3 of 12 cases)
0 @ab
0 @ac
1 @ad
1 @ae
1 @bc
1 @bd
0 @be
0 @cd
1 @ce
0 @de
=== End Post Processing === (Min = 1220)
Reference
(Early) Draft
ToQ shares many attributes with other languages, but its
execution model is different. ToQ is an
interpreter (see the Compiling section below
for how the compiler/interpreter operates). ToQ
interprets each line as it is encountered (that is,
it does not compile code into some intermediate form and execute
it after all input is read). When no errors are detected,
ToQ
converts the user program into a call to the D-Wave quantum computing
system, executes the call, and upon return it displays the
results. ToQ has two modes of operation (Principal and
Post). Post processing is a superset of PrincipalMode, but with a
change from the Principal execution model. Post processing code
immediately follows the PrincipalMode code, and it is executed when the
Principal part has completed. (Click syntax
or Enter "toq -a" for an overview of ToQ syntax and semantics.)
Principal execution model
Principal-mode ToQ programs are comprised of directives, declarations
and executable statements. Most directives should appear before
the first executable statement, but some only make sense when in the
middle of the program (e.g., printvars:, printf:), but all variables
(bools, ints, reals) must be declared before the first executable
statement. There are two kinds of executable statements (regular
and assert). Regular statements are like other languages: (for
example in the sample below, alpha, beta, and
x are pre-declared
variables; PI is a recognized constant;
Cos and Sqrt are recognized
functions):
alpha = Cos(PI-x)
if: (alpha > 2.2433)
beta = 3.7*x*Sqrt(alpha)
else:
beta = (alpha^(1.22*x))
endif:
Only reals, ints, constants and functions may be used in regular
statements (bools are not allowed), and use of an uninitialized
variable is a fatal error. Regular statements are executed in
the expected order. Assert statements have different run-time
behavior. They operate on (at least two) bool variables, and are
used to represent a constraint problem. When an assert statement
with N bools is encountered, all 2N combinations of the bool variable
values are "tried" on the spot, and those sets for which the assert
evaluates to TRUE are saved in an internal data structure. Here
are some samples (all bools start with "@" and have been
pre-declared):
assert: @a + @b + @c + @d + @z >= 1
assert: Or(@x,And(@a,@y))
assert: And(TwoOf(@b,@d,@x,@y),Xor(@c,@z))
(Click boolfuncs or enter "toq -b" for a list of functions which operate on bools, or
"toq -B" for a list of the functions with definitions.) Each bool
should appear in more than one assert, and all the asserts should be
"related" - i.e., they should contain overlapping bools. The
Principal section is terminated when an "end:" or "post:" directive
is encountered.
When all assert statements have been processed (assuming there has
been at least one TRUE for each encountered assert), the combined
internal data structure is converted into a form which the D-Wave
can attack (known as a QUBO := Quadratic Unconstrained Binary
Optimization) and the problem is transmitted to the D-Wave for
resolution. Upon return, ToQ presents the array(s) of bool values
which make all the assert statements TRUE. Assert statement(s) may
be part of any IF-clause. To summarize:
- ToQ is a strongly-typed interpreter which uses the D-Wave
to solve constraint optimization problems.
- The assert capability differs from other languages - each
assert is evaluated 2^N times when encountered, and ToQ
saves its TRUE cases to be combined with the results from
all the other asserts encountered.
- This larger data structure is converted into a QUBO and
passed to the D-Wave for resolution. ToQ then automatically
displays the results for the user (or passes them to the
optional Post processing section).
Post processing execution model
Converting some data structures to QUBO form may be
computationally intensive, and the D-Wave system has finite
resources. Post processing is a ToQ-internal construct which
provides a mechanism to get around some of these limitations.
Post processing is controlled by the programmer via the "post:"
directive, which separates the Principal and Post sections of the
program. Post processing employs a different execution model,
uses some new variable types and a new statement type ("assertp:"),
which is like an "assert:" but less restricted. Post processing
supports two kinds of statements (regular and assertp). Regular
statements are similar to PrincipalMode statements, but with extended
capabilities, and assertp statements are like more powerful assert
statements. The new data types are "intp" and "realp" (analogous to
int and real from the PrincipalMode). They combine with the Post
processing execution model to provide a powerful way to complete
constraint optimization problems, as well as some other types of
problems (for example, some maximization/minimization problems) which
are not straightforward to address with the Principal execution
model. Post processing occurs after the Principal part of the
program has been completed, and uses the results from the Principal
execution. But the model of execution differs from the
PrincipalMode in these ways:
- All the int and real variables from the Principal part are
available, but they are read-only. That is, they may appear
in assertp statements and on the right-hand-side of
replacement statements, but not on the left-hand-side.
- Intp and realp variables (which are not available in the
Principal part of the code) are available for both read and
write. They may appear in assertp statements and on both
the left- and right-hand-side of replacement statements.
- All the bool variables which are used in the Post part must
have been in at least two executed assert statements in the
Principal part.
- All the bool variables from the Principal part are available,
but they are read-only. That is, they may appear in assertp
statements and on the right-hand-side of replacement
statements, but not on the left-hand-side. By contrast,
bool variables are available only in assert statements in
the Principal part, and their values cannot be read. All the
bools must have appeared in at least two Principal asserts.
- All the code in the Post part of the program is collected
into a single block
- All the surviving sets of bools from the Principal part are
saved. Surviving sets are the results from the Principal
part, each representing a set of bool values for which
all the assert statements evaluated to TRUE.
- When there are S sets of bools from the Principal part, the
above-mentioned block of Post code is executed S times.
(This differs from the execution model in Principal mode.)
Each statement in the block is executed. When an assertp
is encountered, it is evaluated - when the result is FALSE,
the block is terminated and control returns to the top of the
block for the next iteration. When all the assertp statements
in an iteration block are TRUE, that set of bools becomes part
of the final overall solution. That is, the final solution to
the original problem is the subset of the S Principal cases for
which all the Post assertp statements evaluate to TRUE.
- By default, all directives and I/O requests (e.g., "printf:")
in the Post section are silently ignored. Utilizing the
"postio:" directive enables Post processing I/O directives
to be executed for each iteration, but this is not recommended.
- The Post processing code block is terminated by either the
"end:" directive or the "epilogue:" directive. The epilogue
section re-enables I/O and other directives, and gives the
ToQ programmer an opportunity to summarize the results.
The epilogue section is terminated by an "end:" directive.
The Post processing execution model suggests two ways to complement
the capabilities of the PrincipalMode:
- Allow the D-Wave to attack larger problems than otherwise
available with PrincipalMode alone by partitioning the set of
assert statements with a "post:" directive (and replacing
the asserts with assertps). The Principal component of the
resulting program must be well-formed (i.e., all bools must
appear in at least two asserts, and all the asserts must have
overlapping bools). In particular, it may be most profitable
to place the asserts with the most bools in the Post section.
In some ways, this technique may make the D-Wave appear larger.
- Expand the exploitable problem domains which can be addressed
by combining bool variables into new variables, and using them
to solve problems not easily attacked in PrincipalMode.
ToQ is an interpreter which runs in concert with,
and acts as an intermediary for, a
host classical system and a D-Wave Quantum Computer System.
However, it does many operations (e.g., Sin, BitCount, Sqrt,
VectCompare, ...) at full compiled code speed. The interpreted
part of the program includes replacement
statements, control flow, and
assert evaluation. For replacement
statements,
ToQ reads expressions in the standard (infix) form, but
stores them in postfix ("Reverse Polish") form. Reverse Polish
is named for the Polish mathematician, Jan Lukasiewicz.
Infix Postfix
--------- -----------
1) X + Y X Y +
2) X * Y + Z X Y * Z +
3) X + Y * Z X Y Z * +
4) (X - Y) / Sin(R - T) X Y - R T - Sin /
5) Sqrt(A+R)*Max(R,R-A,A+1) A R + Sqrt R R A - A 1 + Max *
Postfix representation affords several advantages over infix for
computer evaluation: Postfix is expressed without parentheses,
postfix is easy to evaluate using stacks, and postfix does not have
precedence rules. The translation of infix to postfix notation
handles the parentheses and precedence rules once, so that multiple
evaluations of the expression with different values for the
variables can be more efficient. Note that by convention,
Expression 3 above, "X+Y*Z" is evaluated as "X+(Y*Z)" and not
"(X+Y)*Z." That is, multiplication has a higher precedence
than addition. Click here
to review the precedence rules.
Basic Operators |
+ |
− |
* |
/ |
^ |
** |
& |
| |
! |
~ |
% |
^^ |
---|
|
|
+ Add |
|
& Bitwise AND |
− Subtract |
|
| Bitwise OR |
* Multiply |
|
! Unary NOT |
/ Divide |
|
~ Bitwise NOT |
^ Raise to power |
|
% Remainder |
** Raise to power |
|
^^ Bitwise XOR |
|
Comparison |
and Logical |
Operators |
== |
!= |
> |
>= |
−> |
&& |
|| |
< |
<= |
<−> |
/\ |
\/ |
---|
|
|
== Equal |
|
!= Not equal |
&& And |
|
|| Or |
/\ And |
|
\/ Or |
> Greater than |
|
< Less than |
>= Greater than or equal |
|
<= Less than or equal |
---|
−> Implies |
|
<−> If-and-only-if |
|
The operator precedence rules are:
Operator |
Precedence |
|
Operator |
Precedence |
( |
1 |
|
> |
8 |
) |
1 |
|
< |
8 |
Verb |
2 |
|
>= |
8 |
+ (unary) |
3 |
|
<= |
8 |
− (unary) |
3 |
|
−> (implies) |
8 |
! (unaryNot) |
3 |
|
<−> (iff) |
8 |
** (exp) |
4 |
|
== |
9 |
^ (exp) |
4 |
|
!= |
9 |
* |
5 |
|
& |
10 |
/ |
5 |
|
| |
10 |
+ |
6 |
|
^^ (xor) |
10 |
− |
6 |
|
&& /\ |
11 |
<< |
7 |
|
|| \/ |
11 |
>> |
7 |
|
+= −= *= /= |
12 |
Operators of equal |
|
&= ^= |= %= |
12 |
precedence resolve |
|
>>= <<= = |
12 |
left to right |
|
, |
13 |
Lower precedence values imply dominance. For example, the
snippet X + Y * Z resolves to X + (Y * Z), not
(X + Y) * Z.
The most frequent use of ToQ will be as a library
call to provide faster optimization problem results. But,
since ToQ is (at least in part) an interpreter,
it is critically important that programs that call it do not fail
during the ToQ component of execution. That is,
if a program aborts in the middle of a ToQ section,
there is no debugger available to help diagnose the issue(s).
For that reason, ToQ
offers a few simple mechanisms to aid debugging:
- assert: --
An executable statement which operates on
constraint variables
(bool, bmask, mbool). Assert statements are used
to represent the components of the optimization problem.
An optimization problem is resolved when all the assert
statements in the execution path evaluate to TRUE. Essentially,
ToQ acts as if all the constraint variables took on all
their valid values, and selects only those sets for which all the
assert statements evaluate to TRUE. There are two important
rules with assert statements:
- Each must contain at least two booleans or
one extended boolean variable
- All the asserts must be connected
Here is a sample:
bool: @a, @b, @c
mbool: 1,5, @p1, @p2
assert: Or(@a, Xor(@b, @c))
assert: Nand(@a, @c)
assert: ((@p1 + @p2 + @b) == 7)
assert: ((2*@p1) >= (@p2+@a+@b))
In general, long assert: statements (12 or more bools) should be
avoided. See also quant which
is an advanced feature that
adds the potential to make assert statements more powerful and
easier to use.
- assert1: -- An "assert1:" statement is
treated the same as an "assert:" statement except when
autopartitioning (-QP option) is selected. "assert1:" forces the
assert to be in the first partition. See also
Autopartitioning
- assert2: -- An "assert2:" statement is
treated the same as an "assert:" statement except when
auto-partitioning (-QP option) is selected. "assert2:" forces the
assert to be in the second partition. See also
Autopartitioning
- assertp: -- An executable statement
which may be used only after the "post:" directive. It is
analogous to the regular assert: statement, except that when constraint variables are accessed, only the
actual value set which has resulted from the regular asserts are used
(as opposed to the full set of all possible constraint value
combinations). In the code snippet below, the user want to assure
that the bool: variables (@a1,@a2,...,@a7) are not identical to
(@b1,@b2,...,@b7). This computation could be performed with
regular assert: statements, but might require more complex embedding
layouts.
bool: @a1, @a2, @a3, @a4, @a5, @a6, @a7
bool: @b1, @b2, @b3, @b4, @b5, @b6, @b7
intp: aprofile, bprofile
# ... lots of assert: statements, etc
post:
aprofile = amalgam(@a1,@a2,@a3,@a4,@a5,@a6,@a7)
bprofile = amalgam(@b1,@b2,@b3,@b4,@b5,@b6,@b7)
assertp: (aProfile != bProfile)
end:
An optimization problem which employs "post:" processing is
resolved when all the assert: and assertp: statements in the
execution path evaluate to TRUE.
- clades: --
Enable the Clade Report (Off by default). This report shows
the "family-relationships" for the assert statements. This
directive should appear before the first executable statement.
See also clade.
- cladesoff: --
(Deprecated). This option is a no-op. Clade analysis is
off by default.
- conffile: -- The single argument is the configuration file name (with
no embedded blanks). Note that the configuration data is
usually included in the user's environment. This
directive should appear at the top of the program (before
the declarations). The configuration data read from this
file overrides data from the environment or from the
.dwaverc file in your home directory.
- dbprint: -- Debug aid: Print the line number and name/value of each
scalar item (real, int) in the list.
(Note - "dbpr:", "dbprint:" and "dbprintf:" are aliases).
For example, dbprintf: ijk, clank would yield:
DB(line 34):
Zork = 2.776219e-3
numb = 289
- dbprintb: -- Debug aid: Print the line number and name/value of each
item in the list in decimal, hex, octal, and binary.
The list items must be integers.
For example, dbprintb: abc, hitMask" would yield:
DB(line 119):
abc = 17 = 0x11 =0o21 = 0(2)10001
hitMask = 2078 = 0x81E = 0o4036 = 0(2)100000011110
- dbprintf: -- Debug aid: Print the line number and name/value of each
item in the list. (Note - "dbpr:" and "dbprint:" are
aliases for "dbprintf:")
For example, dbprintf: ijk, clank would yield:
DB(line 51):
ijk = 17
clank = 3.14159
- dbprintm: -- Debug aid: Print the line number and name/value of each
mtx: item in the list. Print by row (starting with 0).
Show each bitmask as hex, then in full binary
- dbprintt: -- Debug aid: Print the line number and name/value of each
tnsr: item in the list. A tensor has (d1,d2,d3) dimensions,
with d3 varying first. Show each (d1,d2) "line" in hex,
then in full binary.
Show each bitmask as hex, then in full binary
- dbprintv: -- Debug aid: Print the line number and name/value of each
vect: item in the list. Show each bitmask as hex, then
in full binary
- dbprintx: -- Debug aid: Print the line number and name/value of each
integer item in the list in hex.
- dbquit: -- Stop immediately.
- end: -- The last
line in an input program. Lines beyond this are ignored.
- endfunction: -- This directive terminates a function.
- endquant: -- This directive terminates a QUANT block of code
and initiates the multiple execution of the statements
in the block.
- epilogue: -- Signal the end of the POST processing section and permit
further I/O and processing before returning to the caller.
- errormgmt: -- Describe the error management philosophy.
- flipflop: -- Format: "flipflop: @x"
Force boolean variable "@x" to be 0, then run the problem
and record the results. Then force "@x" to be 1, run the
problem again, and record the results. Display both sets of
results for user review. (Not available yet.)
- force: -- Format: "force: @x, N" (where N is 0 or 1)
Force boolean variable "@x" to be 0 or 1, then run the problem
and display the results. This directive must appear after
the declaration of "@x" and before the first executable.
(Not available yet.)
- function: -- Define a ToQ subprogram.
(Not available yet.)
- functionio: -- Enable function I/O.
(Not available yet.)
- help: -- Make a help system request: format is "help: topic"
- include: -- Expand the named file in place.
(Not available yet.)
- initfile: -- The single argument is the initialization data file name (with
no embedded blanks). The format of the file is:
- Line 1: vars L N − where "vars" is the sentinel which
identifies the file type, non-zero L says to list the file
with the input listing, and N is the number of lines.
- Lines 2−(N+1): an initialized data item or a
prototype definition (enter: "toq −H prototype" for
details about prototypes).
Each data line contains a single variable and its value
in this format: "Type VarName = Value"
where Type is one of { "int:", "real:", "const:" }.
Note that varfile: is an alias
for "initfile:". This directive should appear at the top of
your program (before the declarations).
- LinearEq: --
LinearEq: is a special-case form of an assert statement.
When a ToQ program contains a LinearEq: statement, all the
executables must be LinearEq: statements. Here is the
general form, which must be followed exactly
C1*@a + C2*@b + C3*@c + ... == X
where @a, @b, ... must be different mbool variables, and the
C(i) must be non-zero integers. These statements comprise a
certain kind of problem (often described as "N equations
in M unknowns," with M > N). This form instructs ToQ to
attack this problem using a Direct-to-QUBO algorithm
instead of the more general (but more complex) algorithm.
This attack is often able to resolve larger problems than
the standard ToQ algorithm can manage. It will find
a single solution (if one exists) – even though there may
be multiple solutions. Here is a sample – two equations
with four unknowns:
mbool: 13,20, @a, @b
mbool: 35,50, @d, @f
# ~~~
lineareq: 5*@a + 6*@b - 2*@d - @f == 40
lineareq: @a + 2*@b - @d + 2*@f == 71
end:
Here are four solution sets to this problem:
@a: 15 13 16 19
@b: 14 17 15 13
@d: 42 46 47 48
@f: 35 35 36 37
- limits: -- The current limits on the values of various parameters.
- listall: -- List all the variables.
- listboolfuncs: -- List the functions which accept boolean arguments.
- listbools: -- List all the boolean variables {bool,bmask,mbool }
- listcode: --
List the input code at the end of the scan. This directive
should appear before the first executable statement, but
the code listing is always at the end.
- listconstdefs: -- List all the constants with their value and description.
- listconsts: -- List all the constants.
- listdirdefs: -- List all the directives with a description of each.
- listdirs: -- List all the directives.
- listfuncdefs: -- List all the functions, with a prototype
and description of each.
- listfuncs: -- List all the functions.
- listgen:
-- Show the internal (generated) representation of
{mbool:, bmask:} variables.
This directive should appear before the first executable
statement.
- listops: -- List all the operations with the precedence rules.
- listprotos: -- List all the prototypes (and associated data) in this program.
This directive should appear before the first
executable statement.
- listsatdefs: -- List all the Satisfiability functions with
a description of each.
- listsats: -- List all the Satisfiability functions.
- maximize: -- An executable statement which may be used only after the "post:"
directive. It is analogous to the regular assert: statement, except
that when bool: variables are accessed, only the actual value sets
which have resulted from the regular asserts are used. Only
one maximize or minimize statement may appear in a ToQ program.
It chooses the maximum value of the previously evaluated asserts
as the final answer of the problem. See also
MaxMin.
- minimize: -- An executable statement which may be used only after the "post:"
directive. It is analogous to the regular assert: statement, except
that when bool: variables are accessed, only the actual value sets
which have resulted from the regular asserts are used. Only
one maximize or minimize statement may appear in a ToQ program.
It chooses the minimum value of the previously evaluated asserts
as the final answer of the problem. See also
MaxMin.
- overview: -- List a brief description of the language features.
See also syntax:.
- post: -- Initiate POST-processing, which grants access to the values of
the computed constraint variable sets. This permits additional
conditions to be applied to the sets of constraint variables which
have survived the initial "assert:" statements. Special variables
(of types "intp:" and "realp:") are available only in the POST-
processing section - they may be used to hold computed combinations
of these formerly restricted variables. Both "intp:" and "realp:"
variables may be used on both the left- and right-hand sides of
replacement statements. All "intp;" and "realp:" variables which
are not set in their declaration statement are initialized to
zero. Normal "int:" and "real:" variables and constraint
variables may appear only on the right-hand side of replacement
statements in the POST section. "assert:" statements may
not be used in the POST section, but "assertp:" statements are
available in the POST section. They operate on any data
type. Only the constraint variable sets for which all the POST
section "assertp:" statements evaluate to TRUE are part of the final
solution. By default, all I/O (and other directives) are ignored in
the POST section (unless the "postio:" directive has been
encountered). See also
Autopartitioning.
- postio: -- Show the attributes for each POST-processing iteration, and
enable I/O (and other directives) during each iteration. In general,
the "postio:" directive should only be used during development
and debugging. It should appear before the first executable statement
- print: -- Print the value and attributes of the one or more variables
in the list. Use commas as separators. If the list is empty,
print the line number.
- printf: -- Print the concatenation of the (comma-separated) items listed.
Each item is either a valid variable name or a string (delimited
by ""s). The list extends to the end-of-line. Here is an example:
printf: "\tOmega = ", omega, " Delta = ", delta, "\n\n"
- printfn: -- Print the concatenation of the (comma-separated) items listed.
Each item is either a valid variable name or a string (delimited
by ""s). The list extends to the end-of-line. A newline character
is appended to the output line. Here is an example:
printfn: "\tiota = ", iota, " blork = ", blork
- printsummary: -- Print a summary at the end of
the scan. This directive
should appear before the first executable statement, but
the summary appears after the input has been read.
- printvars: -- Print the value and attributes of all the variables.
- printx: -- Print the concatenation of the (comma-separated) items
listed. Each item is either a valid variable name or a string
(delimited by ""s). Each variable must be an integer and will be
presented in hex. The list extends to the end-of-line.
A newline character is appended to the output line.
Here is an example:
printx: "mask = ", mask, " bitPattern = ", bitPattern
- prototype: -- The declaration of an external function reference, including
the name (case sensitive), return type and argument types.
See also ToQDispatch.
- quant: -- This directive initiates a block of statements which act
together to prepare a problem for resolution by the D-Wave.
A QUANT block is terminated by an endquant:
directive.
Each statement in the block is executed once for each
possible combination of the values of the constraint variables
(boolean and extended boolean) which appear in the QUANT block.
These results are combined with all the other QUANT block
results, then presented to the D-Wave, which finds the
sets of constraint variable values for which
all the assert statements are TRUE. Each QUANT block must
contain exactly one assert statement, and it must be the
last executable statement in the block. QUANT
blocks may not nest. A standalone assert statement
behaves as if it were in a QUANT block. Statements in a
QUANT block can read (but not write) constraint
variable values. Regular variables may be read and
written in a QUANT block, but changed regular variables
should not be read after a QUANT block (their values
may be unpredictable). A QUANT block must appear after
the last declaration statement and before a "post:"
statement (if any). QUANT blocks are syntactic constructs
which are typically used to simplify the text in an assert
statement by allowing boolean and other constraint variable
values to be combined. I/O is silently ignored in QUANT
blocks unless a quantio: directive has been encountered.
An assert statement in a QUANT block need not directly
reference constraint variables so long as
its expression contains variables which are derivatives
of constraint variables. QUANT blocks
may not be used with autopartitioning (-QP).
- quantio: -- Enable I/O during execution of a QUANT block (not recommended).
- return: -- Transfer control back to this function's caller.
- satisfiability: -- Treat SAT*() functions in special ways (see list below).
This directive must appear before the first executable statement.
A warning message is printed if a SAT*() function is encountered
but no satisfiability: directive is in effect. Here are the
special properties:
- No argument to an SAT*() function is a duplicate
- There are no orphan SAT*() function arguments. That is,
each argument to any SAT*() function must also appear in
at least one other SAT*() function.
- All arguments to SAT*() functions are simple bool:
variables. For example, "Or(@a,@b)" is not a
a valid SAT*() function argument.
- The "−" operator reverses the value of the argument.
That is, a 0 argument is treated as a 1, and a
non-zero argument is treated as a 0.
When the input file is a .cnf, satisfiability: is assumed.
Click here to get more information about
satisfiability problems and about more general cnf formats.
Click here for a list of the ToQ
satisfiability functions.
subjto: --
(subject to) is a special-case assert statement for processing
DTQ (Direct-to-QUBO) maximize/minimize problems (for example, the
"set-partitioning" problem). The rules are:
- Only bool and mbool constraint variables are allowed
- Only one maximize or minimize directive is allowed, it must
be the first executable statement, and it must be a linear
combination of the constraint variables
- The subjto: statements must contain only a simple linear
combination of the constraint variables, followed by
"== const"
Here is a simple example:
bool: @b1,@b2,@b3,@b4,@b5,@b6,@b7,@b8
# ~~~
minimize: (@b1+9*@b2+7*@b3+2*@b4+8*@b5+20*@b6+20*@b7+20*@b8)
subjto: @b2+@b3+@b4+@b6 == 1
subjto: @b1+@b3+@b5+@b7 == 1
subjto: @b1+@b2+@b5+@b8 == 1
# ~~~
end:
- sudoku: --
Sudoku: is a special-case form of an assert statement which
can be used to attack simple 9×9 Sudoku puzzles. When a ToQ
program contains a Sudoku: statement, all the executables
must be Sudoku: statements. Unlike normal asserts, these
statements are not activated until 9 statements are encountered
(each statement contains the input data for a single row
of the puzzle). Only the digits (0-9) may appear in a
sudoku statement (zeroes represent unknowns). No variables
are used with sudoku problems. These ToQ programs use
a Direct-to-QUBO solution. Here is a simple example:
sudoku: ( 7,5,8, 0,2,6, 0,9,0 )
sudoku: ( 0,0,0, 0,8,0, 5,0,0 )
sudoku: ( 3,2,6, 0,1,0, 0,0,7 )
sudoku: ( 0,3,9, 5,0,0, 7,0,0 )
sudoku: ( 5,7,0, 2,9,8, 0,3,4 )
sudoku: ( 0,0,2, 0,0,4, 9,5,0 )
sudoku: ( 9,0,0, 0,4,0, 2,6,5 )
sudoku: ( 0,0,5, 0,3,0, 0,0,0 )
sudoku: ( 0,4,0, 6,5,0, 3,1,9 )
end:
Alternately, ToQ also accepts a special
.sud input file, which allows
simpler formats for sudoku puzzles.
- syntax: -- List the syntax/semantic rules (includes the "overview:").
Alternately, the −a commandline option will do
the same thing.
- timing: -- List the wallclock and CP time for various steps of the ToQ
computation on the Summary page. This directive should
appear before the first executable statement. Alternately,
the −T commandline option can used to initiate
timing.
- varfile: -- "varfile" is an alias for initfile:
− which carries external variable declarations and
values into ToQ.
- viewvectors: -- List the detailed input to the HUBO --> QUBO converter.
This directive should appear before the first executable statement.
- warningsoff: -- Disable the warning messages
(not recommended). This
directive should appear before the first executable statement.
- whereami: -- Print the current line number (and any included text).
- xref: -- Enable the ConstraintVariable/AssertId cross reference map.
This directive should appear before the first executable statement.
- xrefoff: --
(Deprecated). This option is a no-op. Xref is off by default.
Abs(x) |
MtxInsertM(mOut,indx1...) |
Sat24(b1,b2,b3,b4) |
Acos(x) |
MtxInsertV(mOut,indx1...) |
Sat25(b1,b2,b3,b4,b5) |
Acosh(x) |
MtxNot(mOut,mIn) |
Sat3(b1,b2,b3) |
All(b1,b2,...) |
MtxOp(mOut,mtx1,op,...) |
Sat34(b1,b2,b3,b4) |
Amalgam(b1,b2,...) |
MtxOp3(mOut,op1,mtx1,...) |
Sat35(b1,b2,b3,b4,b5) |
And(b1,b2) |
MtxPaint(mOut,word,...) |
Sat4(b1,b2,b3,b4) |
Antilog(x) |
MtxProc(mOut,mIn,...) |
Sat45(b1,b2,b3,b4,b5) |
Any(b1,b2,...) |
MtxPut(mOut,nBits,...) |
Sat5(b1,b2,b3,b4,b5) |
Asin(x) |
MtxReady(mIn) |
SatN(N,b1,b2,...) |
Asinh(x) |
MtxReverse(mOut,mIn) |
Sin(r) |
Atan(x) |
MtxShift(mOut,mIn,n...) |
Sinh(x) |
Atan2(x,y) |
MtxSwap(mOut,mIn,...) |
Sqrt(x) |
Atanh(x) |
MtxVect(m,v,dir) |
SqrtAbs(x) |
Bitcount(n) |
MtxVect(m,v,dir,n1,n2,fill)) |
Sum(n) |
Bitmask(b1,m,n1,n2,...) |
MtxVectInit(mOut,vIn,fill) |
SumDelta(a,d,n) |
Ceiling(x) |
MtxVectOp(mOut,opFlag,...) |
Tan(r) |
Combinations(m,n) |
MtxVectOp3(mOut,opFlag,...) |
Tanh(r) |
Cos(r) |
NAE3Sat(b1,b2,b3) |
TnsrBit(tIn,op,d1,d2,d3,v) |
Cosh(x) |
NAE4Sat(b1,b2,b3,b4) |
TnsrBitCount(tIn) |
Cubert(x) |
NAE5Sat(b1,b2,b3,b4,b5) |
TnsrCompare(t1,c,t2) |
Diff(m1,m2,...) |
NAESat(b1,b2,...) |
TnsrCopy(tOut,tIn) |
Diff1(m1,n1,n2,...) |
NAESat3(b1,b2,b3) |
TnsrGet(tIn,d1,d2,d3,...) |
Even(n) |
NAESat4(b1,b2,b3,b4) |
TnsrGetStk(tIn,d1,d2,j,f) |
Exp(x) |
NAESat5(b1,b2,b3,b4,b5) |
TnsrInit(tOut,word) |
Expm1(x) |
NAESatN(N,b1,b2,...) |
TnsrMtx(t,t1,m,m1,n,d,j,f) |
Factorial(n) |
Nand(b1,b2) |
TnsrNot(tOut,tIn) |
Fibonacci(n) |
NBitHit(b1,m,n1,n2,...) |
TnsrOp(tOut,t1,op,t2) |
Floor(x) |
NDiff(x1,x2,...) |
TnsrOp3(tOut,...) |
FormalMod(a,b) |
NDiff1(x1,x2,...) |
TnsrPut(tOut,d1,d2,d3,...) |
GCD(m1,m2,...) |
NearInt(x,eps) |
TnsrPutStk(tOut,d1,d2,w,f) |
GSeries(m1,m2,n) |
NOf(N,b1,b2,...) |
TnsrReady(tIn) |
IFF(b1,b2) |
None(b1,b2,...) |
TnsrVect(t,v,d,f) |
Implies(b1,b2) |
Nor(b1,b2) |
Trunc(x) |
InRangeEq(x,min,max) |
NOrLess(N,b1,b2,...) |
TwoOf(b1,b2,...) |
InRangeNEq(x,min,max) |
NOrMore(N,b1,b2,...) |
TwoToN(n) |
InSet(val,x1,x2,...) |
Not(b1) |
UpperBd(v) |
Inv(x) |
NSame1(x1,x2,...) |
VectBit(vect,action,index,val) |
InvMod(j,k) |
NumbVals(v) |
VectBitCount(vect,nIgnore) |
IRand(j,k) |
NXor(b1,b2) |
VectCompare(v1,c,v2,...) |
IsInt(x) |
Odd(n) |
VectConcat(vOut,...) |
LCM(m1,m2,...) |
OneOf(b1,b2,...) |
VectCopy(vOut,vIn) |
Ln(x) |
Or(b1,b2) |
VectGet(vIn,i,n,j,f) |
Ln1P(x) |
OutRangeEq(x,min,max) |
VectInit(vOut,mask) |
Log(x) |
OutRangeNEq(x,min,max) |
VectInsert(vOut,...) |
Log2(x) |
OutSet(val,x1,x2,...) |
VectMtx(vOut,mIn) |
LowerBd(v) |
Permutations(m,n) |
VectMtxLns(vOut,mIn,r1,r2) |
Lucas(n) |
PopCount(n) |
VectNot(vOut,vIn) |
MaskN(N) |
Pow(x,y) |
VectOp(vOut,v1,op,v2) |
Max(x1,x2,...) |
Pow2(n) |
VectOp2(vOut,...) |
MaxAbs(x1,x2,...) |
Prime(n) |
VectOp3(vOut,op1,v1,...) |
Min(x1,x2,...) |
Rand(a,b) |
VectPaint(vOut,p,n) |
MinAbs(x1,x2,...) |
RandSeed(n) |
VectProc(vOut,...) |
Mod(j,k) |
Round(x) |
VectPut(vOut,i,w,n) |
MtxBit(mtx,action,r,c,v) |
Same(m1,m2,...) |
VectReady(vInt) |
MtxBitCount(mIn,nIgnore) |
Sat(b1,...) |
VectReverse(vOut,vIn) |
MtxCompare(m1,comp,m2,...) |
Sat12(b1,b2) |
VectShift(vOut,vIn,n,d,f) |
MtxConcat(mOut,mtx1,mtx2) |
Sat13(b1,b2,b3) |
XNor(b1,b2) |
MtxCopy(mOut,mIn) |
Sat14(b1,b2,b3,b4) |
Xor(b1,b2) |
MtxFlip(mOut,mIn) |
Sat15(b1,b2,b3,b4,b5) |
Xor2Sat(b1,b2) |
MtxGet(m,indx,n,...) |
Sat2(b1,b2) |
Xor3Sat(b1,b2,b3) |
MtxInit(mOut,word) |
Sat23(b1,b2,b3) |
- Abs( x ): Absolute value of x
- Acos( x ): Arc Cosine of x (−1 ≤ x < 1)
- Acosh( x ): Arc Hyperbolic Cosine of x
- All( b1, b2, ... ): Return 1 if all of the (2−10)
arguments are non-zero, otherwise return 0.
May be used with bool arguments (but not with
{bmask, mbool} arguments)
- Amalgam( m1, m2, ... ): Return a (32-bit) bitmask where each bit is specified
by the logical value of the (2−16) arguments.
Logical value := (0 for 0, 1 for non-0). The first
argument is the low-order bit, the second argument is
next bit, ... Each argument may be either an int or
or bool, but bool may be used only during POST
processing. Most useful in POST processing to
create a bitmask of bool values for comparison, etc.
For example, when all the arguments are bool variables,
amalgam(@q1,@q2,@q3,@q4) = @q1 + 2*@q2 + 4*@q3 + 8*@q4.
Or, given (@b1,@b2,@b3,@b4,@b5) = (0,1,1,0,1),
Amalgam(@b1,@b2,@b3,@b4,@b5)
would return 22 = 0x16 = 0o26 = 0(2)10110.
See also BitCount(),
BitMask(), and MaskN().
- And( b1, b2 ): Return 1 if both of the
arguments are non-zero, otherwise return 0.
May be used with bool arguments (but not with
{bmask, mbool} arguments)
- Antilog( x ): Inverse logarithm - the number whose
logarithm is x
- Any( b1, b2, ... ): Return 1 if any of the (2−10)
arguments is non-zero, otherwise return 0.
May be used with bool arguments (but not with
{bmask, mbool} arguments)
- Asin( x ): Arc Sine of x (−1 ≤ x < 1)
- Asinh( x ): Arc Hyperbolic Sine of x
- Atan( x ): Arc Tangent of x
- Atan2( x, y ): Arc Tangent of x/y -- Atan2() overcomes a limitation
with Atan(). Specifically, with two arguments, Atan2() can return
the angle in the correct quadrant
- Atanh( x ): Arc Hyperbolic Tangent of x
- BitCount( n ): The number of 1-bits in the 32-bit integer n.
Same as PopCount().
- BitMask( bit1, m1, m2, ... ): Return a 32-bit integer mask with a 1 for each bit location
designated by arguments (2,3,...). bit1 represents the
low order bit in the result mask, thus each of the subsequent
(1−16) arguments must be in the range {bit1 − (bit1+31)}.
bit1 must be in the range (0−1023). Any overlap generates
a run-time warning, not an error. Here are some samples:
BitMask(1,4,6,1) evaluates to 41 = 0o51 = 0x29 = 0(2)101001
BitMask(0,8,0,3) evaluates to 265 = 0o411 = 0x109 = 0(2)100001001
BitMask(64,70,66,71) evaluates to 196 = 0o304 = 0xC4 = 0(2)11000100
BitMask(511,512,498,511,527) generates a range error (498)
Often used with its companion function NBitHit()
(take care to use the same value for bit1), particularly as a filter
for constraint variables, as in
int: maskp
mbool: 0,31, xyz
maskp = BitMask(0,2,5,12,15,17,23)
# TRUE only when xyz is one of (2,5,12,15,17,23)
assert: NBitHit(0,maskp,xyz) == 1
- Ceiling( x
): The smallest integer ≥ x
(i.e., RoundUp).
Not to be confused with Trunc().
- Combinations( total, n ): The number of combinations of total things taken n
at a time. Both arguments are integers in (1-51), and
n < total. See also Permutations().
- Cos( r ): Cosine of the angle r (radians)
- Cosh( x ): Hyperbolic Cosine of the angle x (radians)
- Cubert( x ): The cube root of x
- Diff( m1, m2, ...): Return T/F to: Are all the (2−13) integer argument values
different? Accepts expressions, constraintVars and regularVars
as arguments. (ConstraintVar types are {bool,mbool,bmask}).
See also Same(),
NDiff(),
Diff1().
- Diff1( m1, n1, n2, ...): Return T/F to: Is the first argument different than all the
other (1−12) arguments?
See also Same(),
NDiff(),
Diff().
- Even( n ): Return 1 if the integer argument n is even, else return 0
- Exp( x ): Exponential of x. Exp(x) = ex
- Expm1( x ): Exponential of (x−1). Expm1(x) = ex−1, accurate
even for small values of x
- Factorial( n ): The product of all the integers from 1 to n
- Fibonacci( n ): The nth element in the Fibonacci series.
- Floor( x ): The greatest integer ≤ x (i.e., RoundDown).
Not to be confused with Trunc().
- FormalMod( a, b ): The amount by which a exceeds the largest integer
multiple of b which is not greater than a. Thus,
FormalMod(17,4) = 1; FormalMod(−17,4) = 3. The standard definition is
extended to allow real arguments, and to handle (b < 0)
by convention such that FormalMod(a,-b) = FormalMod(-a,b).
See also
Mod(),
InvMod().
- GCD( m1, m2, ... ): Return the greatest common divisor (aka, greatest common factor (gcf)).
The largest positive integer that divides the (2−10) 32-bit positive
integer args evenly (no remainder). Special case: GCD(0,0) = 0
- GSeries( m1, m2, n ): The nth element in the Generalized Fibonacci series.
- GSeries(0) = m1
- GSeries(1) = m2
- GSeries(n) = GSeries(n−2) +
GSeries(n−1).
- IFF( b1, b2 ): The logical (or material) biconditional operator (also known as
"if and only if"). Return TRUE when b1 and b2 are logically the same,
FALSE otherwise. IFF(b1,b2) is equivalent to
(b1 <−> b2).
IFF() is an alias for XNor() and NXor()). May be used with bool
arguments (but not with {bmask, mbool} arguments).
- Implies( b1, b2 ): The material conditional operator (also known as the material
implication). Return TRUE except when b1 is TRUE and b2 is
FALSE. Implies(b1,b2) is equivalent to (b1 −> b2)."
May be used with bool arguments (but not with {bmask, mbool}
arguments).
- InRangeEq( val, min, max ): Return 1 when (min ≤ val ≤ max),
0 otherwise. May be used with constraint arguments.
- InRangeNEq( val, min, max ): Return 1 when (min < val < max),
0 otherwise. May be used with constraint arguments.
- InSet( val, x1, x2, ... ): Return 1 when val is the same value as one of the (1-8) other
arguments, else return 0. May be used with constraint arguments.
See also OutSet().
- Inv( x ):
Inverse. Inv(x) = 1/x (x ≠ 0)
- InvMod( j, k ): The modular multiplicative inverse of j mod k
(both 32-bit integers > 1), or zero if the two arguments are not
coprime. See also
Mod(),
FormalMod().
- IRand( j, k ): Return a random integer between j and k (both
are positive 32-bit integers)
Notes:
- Not reproducible
- IRand(0,1) is like a coin flip
- See also Rand(),
RandSeed().
- IsInt( x
): Return TRUE when the argument x is an
integer. See also NearInt().
- LCM( m1, m2, ... ): Return the least common multiple (aka, lowest common factor (lcf)).
The smallest positive integer that is a multiple of the integer
arguments. Special case: if any argument is zero, the LCM is
defined to be zero.
- Ln( x ): Natural logarithm of x (x > 0) - the power to which
e (2.718281828459...) must be raised to yield x
- Ln1P( x ): Natural logarithm of (x+1), (x > −1)
- Log( x ): Logarithm (base 10) of x (x > 0) - the power to which 10
must be raised to yield x
- Log2( x ): Logarithm (base 2) of x (x > 0) - the power to which 2
must be raised to yield x
- LowerBd( v ): Return the smallest value that the constraint variable v can take on. This special function behaves like a compile-time
constant rather than a regular function, and thus can appear
anywhere after the declarations, but not in an assert statement
nor in a QUANT block. Its argument must be of type bool, mbool
or bmask. The argument may not be an expression.
For example:
bool: @pair
mbool: 5,20,2, @batch
bmask: 2,4, @mask
int: firstP, firstB, firstM
firstP = LowerBd(@pair)
firstB = LowerBd(@batch)
firstM = LowerBd(@mask)
would set firstP to 0, firstB to 5 and firstM to 3 = 0(2)0011.
See also
UpperBd(),
NumbVals().
- Lucas( n
): The nth element in the Lucas series. Lucas(0) = 2,
Lucas(1) = 1, and Lucas(n) = Lucas(n−2) + Lucas(n−1).
- MaskN( N )
: Return a 32-bit mask with the low-order N bits set.
The argument N must be an integer in (0-31).
Sample: MaskN( 5 ) = 31 = 0x1F = 0o37 = 0(2)11111
- Max( x1, x2, ... ): Maximum of the (2−10) arguments)
- MaxAbs( x1, x2, ... ): Maximum of the absolute values of the
(2−10) arguments
- Min( x1, x2, ... ): Minimum of the (2−10) arguments
- MinAbs( x1, x2, ... ): Minimum of the absolute values of the
(2−10) arguments
- Mod( j, k ): The remainder from dividing integer k into
integer j.
Non-integer values for j and k are silently truncated
to integers. This definition is used for the % operator.
See also
FormalMod(),
InvMod().
- MtxBit( mtx, op, row,
col, val ): Return the number of 1 bits in
matrix mtx.
Operate on matrix mtx in the following way:
- Check that mtx exists and is initialized,
row,col is in range (count
from 0), op is 1 of
{SETBIT,
GETBIT}.
If these conditions are not met, RETURN -1.
- If op is SETBIT, set the
bit at row,col
to 0 if val is zero, 1 otherwise, and RETURN 1
- If op is GETBIT,
RETURN the value of the bit
at row,col. In this case, val is not used.
- SETBIT and
GETBIT
are ToQ internal constants.
- MtxBitCount( mIn, nIgnore ):
Return the number of 1 bits in matrix mIn. Ignore the
nIgnore (-31 → 31) end bits in each row of mIn.
When nIgnore is negative, ignore the leading bits in
each row, else ignore the rightmost bits of each row.
Typically, nIgnore = 0. May be used in an assert
statement. If an error is encountered, return -1.
- MtxCompare( m1, comp, m2, ... ):
Return TRUE(1) or FALSE(0) to the comparison of two conforming
matrices (m1 and m2). Ignore the nIgnore (-31 --> 31)
end bits in each row of the matrices. When nIgnore is
negative, ignore the leading bits in each row, else ignore
the rightmost bits of each row. Typically, nIgnore = 0.
The comparison operator (comp) must be one of the these
extended internal ToQ comparison constants:
{XTEQ,
XTNEQ,
XTLT,
XTLE,
XTGE,
XTGE}.
The comparisons scan left to right. May be used in an
assert statement. If an error is encountered, return -1.
- MtxConcat( mOut, m1, m2 ):
Build matrix mOut by concatenating matrices m1
and m2.
All three matrices must have the same number of columns,
and the number of rows in mOut must be the sum of the input
matrices' rows. Return 0 if successful, -1 if any errors
encountered.
- MtxCopy( mOut, mIn ):
Copy matrix mIn to mOut. mIn and
mOut must be conforming matrices (same size).
Return 0 if successful, -1 if any errors encountered.
See also MtxInsert(),
MtxInsertM(),
MtxInsertV().
- MtxFlip( mOut, mIn ):
Create mOut from mIn by flipping rows/columns.
MOut and
mIn must be different and anti-conformant. MIn must be
initialized. The number of rows and columns in mIn must be
multiples of 32. MOut must be pre-declared (like any other
matrix). Return 0 if successful, -1 if any errors encountered.
- MtxGet( m, indx, nBits, loc, indx, just, fill, wrap ):
Return a 32-bit integer copy of the nBits bits starting
at row(col) loc and index indx of matrix mIn.
Dir must be one of
{MTXROW,
MTXCOL}.
Loc and
indx both start at 0, and indx is a bitcount.
NBits is in (1-32), and indx counts left to right.
Wrap is one of
{WRAP,
WRAPOFF}.
If wrap = WRAPOFF,
a request beyond the end of a row is an error. In either
case, an error occurs if the request extends beyond the size
of mIn. When nBits is not 32, the just
and fill
arguments determine the justification and the fill
for the returned 32-bit integer. These internal ToQ
constants constitute the valid values for the justification
and fill arguments:
just fill
---------- ----------
LEFTS Left side FILLZERO Fill with 0s
RIGHTS Right side FILLLONE Fill with 1s
See also
{VectGet(),
MtxPut(),
MtxInsertM(),
MtxInsertV()}.
- MtxInit( mOut, word ):
Initialize matrix mOut with copies of 32-bit word word.
Typical values for word could include 0, MASK32 (all
ones), 7, -15, MASK3202, ... Return 0 if successful,
-1 if any errors encountered. See also
{MtxVectInit(),
MtxPaint()}.
- MtxInsertM( mOut, nBits, row1, indx1, mIn, row2, indx2, fill, wrap ):
Insert nBits from matrix mIn starting at row row2,
bit "indx2" into matrix mOut starting at row row1,
bit indx1 The row and indx arguments both start at 0;
indx is a bitcount and counts left to right. Wrap is
one of
{WRAP,
WRAPOFF}.
If wrap = WRAPOFF, a request
beyond the end of a row is an error. In either case, an
error occurs if the request extends beyond the size of
either matrix. Return 0 if successful, -1 if any errors
encountered. Note - if mOut is uninitialized on
input to MtxInsertM(), it is initialized via fill
before the data move. Fill is one of
{ FILLZERO,
FILLONE }.
When mOut has already been initialized, fill is ignored.
See also
{MtxInsert(),
{MtxInsertV(),
MtxPut()}.
- MtxInsertV( mOut, nBits, row, indx1, vIn, indx2, fill, wrap )
Insert nBits from vector vIn starting at bit indx2 into
matrix mOut starting at row row, bit indx1. The
row and indx arguments both start at 0. Indx is a
bitcount and counts left to right. Wrap is one of
{WRAP,
WRAPOFF}.
If wrap = WRAPOFF, a request
beyond the end of a row is an error. In either case, an
error occurs if the request extends beyond the size of
the vector or matrix. Return 0 if successful, -1 if any
errors encountered. Note: if mOut is uninitialized on
input to MtxInsertV(), it is initialized via fill
before the data move. Fill is one of
{ FILLZERO,
FILLONE }.
When mOut has already been initialized, fill is
ignored. See also MtxInsertM(), MtxPut().
- MtxNot( mOut, mIn ):
Flip each bit of mIn to create mOut. mIn and mOut
must be conforming matrices (same size), but they need
not be different. MIn must be initialized.
Return 0 if successful, -1 if any errors encountered.
- MtxOp( mOut, m, op, m2 ):
Set matrix mOut to m1 op m2 - where all three matrices
are conforming, and
op is one of the extended bit-by-bit binary operators: {
XTAND,
XTANDNOT,
XTOR,
XTORNOT,
XTXOR,
XTNOR,
XTXNOR,
XTIFF,
XTIMPLIES }.
These terms are
internal ToQ constants.
(Note -
{XTANDNOT,
XTORNOT,
XTIMPLIES }
are not commutative.)
These terms are internal ToQ constants; they perform
bit-by-bit operations. M1 and m2 must be different,
but mOut is not restricted. Return 0 if successful,
-1 if any errors encountered. See also MtxOp3().
- MtxOp3( mOut, op1, mtx1, op, op2, op3, m2 ):
Set matrix mOut to ((op1 m1) op2 (op3 m2)) -
where all three matrices are conforming, and op1 and
op3 are one of
{XTNOT,
XTNOOP},
and op2 is one of the extended bit-by-bit binary operators: {
XTAND,
XTANDNOT,
XTOR,
XTORNOT,
XTXOR,
XTNOR,
XTXNOR,
XTIFF,
XTIMPLIES }.
These terms are
internal ToQ constants.
(Note -
{XTANDNOT,
XTORNOT,
XTIMPLIES }
are not commutative.)
M1 and m2 must be different,
but mOut is not restricted. Return 0 if successful, or
-1 if any errors encountered. See also MtxOp(), VectOp3().
- MtxPaint( mOut, word, nBits ):
Fill matrix mOut (left to right) with copies of the lower
nBits bits of the 32-bit word word. NBits
is in (3-32).
The last (rightmost) bits of each row of mOut may contain
only the expected subset of word. See also MtxInit().
Return 0 if successful, -1 if any errors encountered.
(not yet available)
- MtxProc( mOut, mIn, action, w1, w2, nBits, delta ):
Process matrix mIn via action action which operates on the
low order nBits of 32-bit word w1. Actions are
- XTCOUNT - return the number of occurrences of w1.
- XTFIND - return the location of the first occurrence
of w1 in vIn (or -1 if not found).
- XTLAST - return the location of the last occurrence
of w1 in vIn (or -1 if not found).
- XTREPL - copy mIn to mOut and replace all
occurrences of w1 with w2.
Only XTREPL uses mOut and w2. 
Delta (range: 1-nBits)
tells how many bits to skip on a miss (a hit always skips
nBits bits). Return -1 if unsuccessful.
(not yet available)
- MtxPut( mOut, nBits, word, row, indx, fill, wrap ):
Place the low-order nBits bits of the 32-bit word word
into matrix mOut starting at row row, index indx.
NBits is in (1-32) and indx starts at 0 and counts
left to right.
Wrap is one of
{WRAP,
WRAPOFF}.
If wrap is WRAPOFF, an error occurs if the request
extends beyond an mOut row. In either case, an error
occurs if the request extends beyond last bit of mOut.
Return 0 if successful, -1 if any errors encountered.
Note - if mOut is uninitialized on input to MtxPut(),
it is initialized via fill before the data move.
Fill is one of
{ FILLZERO,
FILLONE }.
When mOut has
already been initialized, fill is ignored.
See also MtxGet(), MtxInsertM(), MtxInsertV().
- MtxReady( mIn ):
Return 1 if matrix mIn has been initialized, 0 if not, or
-1 if mIn is not a matrix.
- MtxReverse( mOut, mIn ):
Set mOut to a bit-by-bit reverse of mIn. The input
matrices must be conforming, but they need not be different.
The reversals are done by rows. Return 0 if successful,
-1 if any errors encountered.
- MtxShift( mOut, mIn, nBits, dir, fill ):
Set mOut to a copy of mIn shifted nBits bits in
direction dir with fill set by fill. mOut
and mIn must be
conforming vectors, but they need not be different.
The shifts are done by row (i.e., no cross-row
shifts). To do a full matrix shift (cross-row), use
MtxVect()
to create a vector, then
VectShift(), then
MtxVect() again to create a matrix.
These internal ToQ constants constitute the
valid values for the direction and fill arguments:
dir fill
----------- ------------
LEFTS Left shift FILLZERO Fill with 0s
RIGHTS Right shift FILLLONE Fill with 1s
LEFTC Left circular shift
RIGHTC Right circular shift
The fill argument is required for all cases, but it is
ignored for circular shifts. Return 0 if successful,
-1 if any errors encountered.
- MtxSwap( mOut, mIn, swFlag, n1, n2 ):
Set mOut to a copy of mIn, then swap mOut's rows(cols)
n1 and n2, with (n1 < n2),
and counting starts at zero. Matrices
mOut and mIn
must be conforming but need not be different. MIn must be
initialized. SwFlag must be one of
{MTXROW,
MTXCOL}.
- MtxVect( m, v, dir ):
Copy all data between matrix m and vector v.
Dir is one of
{MTXTOVECT,
{VECTTOMTX}.
After the copy, both
will contain the same data. The source must be initialized.
V(nBits) must be 32*m(nRows)*m(nCols).
See also MtxVectInit(),
See also MtxVectLns().
- MtxVectInit( mOut, vIn, fill ):
Build matrix mOut by concatenating copies of vector
vIn The size of vIn must match the number of
columns in mOut. VIn must be initialized.
Return 0 if successful, otherwise -1. See also
MtxInit,
MtxPaint.
- MtxVectLns( m, v, dir, n1, n2, fill ):
Copy selected data between matrix m and vector v.
Dir is one of
{MTXTOVECT,
{VECTTOMTX}.
The source must be
be initialized. The copy uses row(col) n1 to n2,
where the row(col) numbers are zero-based and n1 ≤
n2. The full
contents of v are accessed. When the destination is
an uninitialized m, it is set to fill before the
copy (fill is otherwise ignored). Fill is one of
{FILLZERO,
FILLONE}.
The size of vector v(nBits) must
be 32*(n2-n1+1).
See also MtxVect(),
MtxVectInit().
- MtxVectOp( mOut, opFlag, mIn, op, vIn ):
MIn and mOut
are conforming matrices, and vIn is a vector.
Set matrix mOut to either
(mIn op vIn) - or -
(vIn op mIn),
where the order is controlled by opFlag which is one of
{COLVECTMTX,
ROWVECTMTX,
MTXCOLVECT,
MTXROWVECT},
and op is one of the extended bit-by-bit binary operators: {
XTAND,
XTANDNOT,
XTOR,
XTORNOT,
XTXOR,
XTNOR,
XTXNOR,
XTIFF,
XTIMPLIES }.
These terms are
internal ToQ constants.
(Note -
{XTANDNOT,
XTORNOT,
XTIMPLIES }
are not commutative.)
When a ROWVECT opFlag is chosen, the length of vector vIn
must match the number of columns in mIn. That is,
each bit in each row of min is operated on (via op)
by each bit of vIn to create each bit in each row
in mOut.
When a COLVECT opFlag is chosen, the length of vin
is not restricted, but rather it is used to cover the size
(number of rows) of mIn. That is, each bit in each column
of mIn is operated on (via op) by each bit of vin
to create each bit in each column in mOut.
Return 0 if successful, -1 if not.
See also MtxVectOp3().
- MtxVectOp3( mOut, opFlag, op1, mIn, op2, op3, vIn ):
MIn and mOut
are conforming matrices, and vIn is a vector.
Set matrix mOut to either
((op1 mIn) op2 (op3 vIn)) - or -
((op1 vIn) op2 (op3 mIn)),
where the order is controlled by opFlag which is one of
{COLVECTMTX,
ROWVECTMTX,
MTXCOLVECT,
MTXROWVECT},
op1 and op3 are one of
{XTNOT,
XTNOOP},
and op2 is one of the extended bit-by-bit binary operators: {
XTAND,
XTANDNOT,
XTOR,
XTORNOT,
XTXOR,
XTNOR,
XTXNOR,
XTIFF,
XTIMPLIES }.
These terms are
internal ToQ constants.
(Note -
{XTANDNOT,
XTORNOT,
XTIMPLIES }
are not commutative.)
When a ROWVECT opFlag is chosen, the length of vector vIn
must match the number of columns in mIn. That is,
each bit in each row of min is operated on (via op)
by each bit of vIn to create each bit in each row
in mOut.
When a COLVECT opFlag is chosen, the length of vin
is not restricted, but rather it is used to cover the size
(number of rows) of mIn. That is, each bit in each column
of mIn is operated on (via op) by each bit of vin
to create each bit in each column in mOut.
Return 0 if successful, -1 if not.
See also MtxVectOp().
- NAE3Sat( b1, b2, b3 ): A satisfiability function which returns TRUE
if any of its 3 arguments is different than any other (that is,
the arguments are not all equal), otherwise return 0.
Any argument may be preceded by "−", which reverses
the value of the argument. That is, a zero argument is treated
as a 1, and a non-zero argument is treated as a 0. The "−" operator
reverses the value of its argument only in the context of
a satisfiability function, not in general.
These three sample asserts are equivalent:
bool: @w, @x, @y
assert: nae3sat( @w, NOT(@x), @y )
assert: nae3sat( @w, !@x, @y )
assert: nae3sat( @w, -@x, @y )
NAE3Sat() and NAESat3() are aliases. NAE3Sat(@a,@b,@c) and
NAESat(@a,@b,@c) produce the same results. NAE3SAT() checks
its argument count, but NAESat() doesn't. NAE3Sat() may be used
with bool arguments (but not with {bmask, mbool} arguments)
- NAE4Sat( b1, b2, b3, b4 ): A satisfiability function which returns TRUE
if any of its 4 arguments is different than any other (that is,
the arguments are not all equal), otherwise return 0.
Any argument may be preceded by "−", which reverses
the value of the argument. That is, a zero argument is treated
as a 1, and a non-zero argument is treated as a 0. The "−" operator
reverses the value of its argument only in the context of
a satisfiability function, not in general.
These three sample asserts are equivalent:
bool: @w, @x, @y, @glorp
assert: nae4sat( @w, NOT(@x), @y, @glorp )
assert: nae4sat( @w, !@x, @y, @glorp )
assert: nae4sat( @w, -@x, @y, @glorp )
NAE4Sat() and NAESat4() are aliases. NAE4Sat(@a,@b,@c,@d) and
NAESat(@a,@b,@c,@d) produce the same results. NAE4SAT() checks
its argument count, but NAESat() doesn't. NAE4Sat() may be used
with bool arguments (but not with {bmask, mbool} arguments)
- NAE5Sat( b1, b2, b3, b4, b5 ): A satisfiability function which returns TRUE
if any of its 5 arguments is different than any other (that is,
the arguments are not all equal), otherwise return 0.
Any argument may be preceded by "−", which reverses
the value of the argument. That is, a zero argument is treated
as a 1, and a non-zero argument is treated as a 0. The "−" operator
reverses the value of its argument only in the context of
a satisfiability function, not in general.
These three sample asserts are equivalent:
bool: @w, @x, @y, @bingo, @zorro
assert: nae5sat( @w, NOT(@x), @y, @bingo, @zorro )
assert: nae5sat( @w, !@x, @y, @bingo, @zorro )
assert: nae5sat( @w, -@x, @y, @bingo, @zorro )
NAE5Sat() and NAESat5() are aliases. NAE5Sat(@a,@b,@c,@d,@e) and
NAESat(@a,@b,@c,@d,@e) produce the same results. NAE5SAT() checks
its argument count, but NAESat() doesn't. NAE5Sat() may be used
with bool arguments (but not with {bmask, mbool} arguments)
- NAESat( b1, b2, ... ): A satisfiability function which returns TRUE
if any of its 2-6 arguments is different than any other (that is,
the arguments are not all equal), otherwise return 0.
Any argument may be preceded by "−", which reverses
the value of the argument. That is, a zero argument is treated
as a 1, and a non-zero argument is treated as a 0. The "−" operator
reverses the value of its argument only in the context of
a satisfiability function, not in general.
These three sample asserts are equivalent:
bool: @a, @b, @c, @d
assert: naesat( @a, NOT(@b), @c, @d )
assert: naesat( @a, !@b, @c, @d )
assert: naesat( @a, -@b, @c, @d )
NAESat() may be used with bool arguments (but not with
{bmask, mbool} arguments)
- NAESat3( b1, b2, b3 ): A satisfiability function which returns TRUE
if any of its 3 arguments is different than any other (that is,
the arguments are not all equal), otherwise return 0.
Any argument may be preceded by "−", which reverses
the value of the argument. That is, a zero argument is treated
as a 1, and a non-zero argument is treated as a 0. The "−" operator
reverses the value of its argument only in the context of
a satisfiability function, not in general.
These three sample asserts are equivalent:
bool: @r, @s, @t
assert: naesat3( @r, NOT(@s), @t )
assert: naesat3( @r, !@s, @t )
assert: naesat3( @r, -@s, @t )
NAESat3() and NAESat3() are aliases. NAESat3(@x,@y,@z) and
NAESat(@a,@b,@c) produce the same results. NAESat3() checks
its argument count, but NAESat() doesn't. NAESat3() may be used
with bool arguments (but not with {bmask, mbool} arguments)
- NAESat4( b1, b2, b3, b4 ): A satisfiability function which returns TRUE
if any of its 4 arguments is different than any other (that is,
the arguments are not all equal), otherwise return 0.
Any argument may be preceded by "−", which reverses
the value of the argument. That is, a zero argument is treated
as a 1, and a non-zero argument is treated as a 0. The "−" operator
reverses the value of its argument only in the context of
a satisfiability function, not in general.
These three sample asserts are equivalent:
bool: @w, @x, @y, @glorp
assert: naesat4( @w, NOT(@x), @y, @glorp )
assert: naesat4( @w, !@x, @y, @glorp )
assert: naesat4( @w, -@x, @y, @glorp )
NAESat4() and NAE4Sat() are aliases. NAESat4(@a,@b,@c,@d) and
NAESat(@a,@b,@c,@d) produce the same results. NAESat4() checks
its argument count, but NAESat() doesn't. NAESat4() may be used
with bool arguments (but not with {bmask, mbool} arguments)
- NAESat5( b1, b2, b3, b4, b5 ): A satisfiability function which returns TRUE
if any of its 5 arguments is different than any other (that is,
the arguments are not all equal), otherwise return 0.
Any argument may be preceded by "−", which reverses
the value of the argument. That is, a zero argument is treated
as a 1, and a non-zero argument is treated as a 0. The "−" operator
reverses the value of its argument only in the context of
a satisfiability function, not in general.
These three sample asserts are equivalent:
bool: @w, @x, @y, @bingo, @zorro
assert: naesat5( @w, NOT(@x), @y, @bingo, @zorro )
assert: naesat5( @w, !@x, @y, @bingo, @zorro )
assert: naesat5( @w, -@x, @y, @bingo, @zorro )
NAESat5() and NAE5Sat() are aliases. NAESat5(@a,@b,@c,@d,@e) and
NAESat(@a,@b,@c,@d,@e) produce the same results. NAESat5() checks
its argument count, but NAESat() doesn't. NAESat5() may be used
with bool arguments (but not with {bmask, mbool} arguments)
- NAESatN( N, b1, b2, ... ): A satisfiability function which returns TRUE
if any of its N (2-6) arguments is different than any other (that is,
the arguments are not all equal), otherwise return 0.
Any argument may be preceded by "−", which reverses
the value of the argument. That is, a zero argument is treated
as a 1, and a non-zero argument is treated as a 0. The "−" operator
reverses the value of its argument only in the context of
a satisfiability function, not in general.
These three sample asserts are equivalent:
bool: @a, @b, @pluto, @d
assert: naesatn( 4, @a, NOT(@b), @pluto, @d )
assert: naesatn( 4, @a, !@b, @pluto, @d )
assert: naesatn( 4, @a, -@b, @pluto, @d )
NAESatN() may be used with bool arguments (but not with
{bmask, mbool} arguments)
- Nand( b1, b2 ): Return 0 if both b1 and b2 are non-zero.
Otherwise return 1. (Note that any other logical gate
can be created out of NAND gates.)
May be used with bool arguments (but not with
{bmask, mbool} arguments)
- NBitHit( bit1, mask,
x1, x2, ...): Mask is a 32-bit mask (possibly
built with BitMask()), bit1
is the value which the low-order bit of mask represents, and
x1,x2,..." are (1−16) integers in the range {bit1 − (bit1+31)}.
Return a count of the bit hits. A hit occurs when mask has
a 1 bit in location (x1-bit1) or (x2-bit1) or
... Argument x(n) == bit1
implies the low order (rightmost) bit. Here are some samples:
Using:
a = 6; d = 41 = 0o51 = 0x29 = 0(2)101001
b = 0; e = 265 = 0o411 = 0x109 = 0(2)100001001
c = 10; f = 196 = 0o304 = 0xC4 = 0(2)11000100
NBitHit(1,d,a) returns 1 (6)
NBitHit(0,e,3,b,6,9) returns 2 (0, 3)
NBitHit(64,f,65,66,67,68) returns 1 (66)
NBitHit(0,e,4,14,5,15,6,16) returns 0 (no hits)
NBitHit(32,c,48,49,50,51) generates a range error (10)
Often used with its companion function BitMask() (take care
to use the correct value for bit1), particularly as a
filter for constraint variables, as in
int: maskq
mbool: 0,15, omega
maskq = BitMask(0,0,3,5,13)
# TRUE only when omega is one of (0,3,5,13)
assert: NBitHit(0,maskq,omega) == 1
- NDiff( m1, m2, ...): Return the number of different values among the (2−13) integer
arguments. Accepts expressions, constraintVars and regularVars
as arguments. (ConstraintVar types are {bool,mbool,bmask}).
See also Same(),
Diff1(),
NDiff1(),
Diff().
- NDiff1( m1, n1, n2, ...):
Return the number of arguments which are not equal to the first
argument among the other (1-12) integer arguments. Accepts
expressions, constraintVars and regularVars as arguments.
(ConstraintVar types are {bool,mbool,bmask}).
See also Same(),
NDiff(),
Diff1(),
NSame1(),
Diff().
- NearInt( x, eps ): If x is within eps of an integer, return that integer,
else return 0.5. 10-9 is a typical value for eps
(0 < eps < 0.01). See also IsInt().
- NOf( N, b1, b2, ... ): Return 1 if exactly N of the (2−10)
other arguments are non-zero, otherwise return 0. (N > 0).
May be used with bool: arguments (but not with
{bmask, mbool} arguments)
- None( b1, b2, ... ): Return 1 if all of the (2−10)
arguments are zero, otherwise return 0.
May be used with bool arguments (but not with
{bmask, mbool} arguments)
- NOr( b1, b2 ): Return 1 if b1 and b2 are both zero, otherwise return 0.
Same as Not(Or(b1,b2)). May be used with bool
arguments (but not with {bmask, mbool} arguments)
- NOrLess( N, b1, b2, ... ): Return 1 if N or less of the (2−10)
other arguments are non-zero, otherwise return 0.
(N > 0).
May be used with bool arguments (but not with
{bmask, mbool} arguments)
- NOrMore( N, b1, b2, ... ): Return 1 if N or more of the (2−10)
other arguments are non-zero, otherwise return 0.
(N > 0).
May be used with bool arguments (but not with
{bmask, mbool} arguments)
- Not( b1 ): Return 1 if b1 is 0, and 0 if b1 is non-zero.
May be used with bool arguments (but not with
{bmask, mbool} arguments)
- NSame1( m1, n1, n2, ...):
Return the number of arguments which are equal to the first
argument among the other (1-12) integer arguments. Accepts
expressions, constraintVars and regularVars as arguments.
(ConstraintVar types are {bool,mbool,bmask}).
See also Same(),
NDiff(),
Diff1(),
NDiff1(),
Diff().
- NearInt( x, eps ): If x is within eps of an integer, return that integer,
- NumbVals( v ): Return the number of values that the constraint variable v can take on. This special function behaves like a compile-time
constant rather than a regular function, and thus can appear
anywhere after the declarations, but not in an assert statement
nor in a QUANT block. Its argument must be of type bool, mbool
or bmask. The argument may not be an expression.
For example:
bool: @tf
mbool: 5,20,2, @batch
bmask: 2,4, @mask
int: numbTF, numbB, numbM
numbTF = NumbVals(@pair)
numbB = NumbVals(@batch)
numbM = NumbVals(@mask)
would set numbP to 2, numbB to 8 and numbM to 6.
See also
UpperBd(),
LowerBd().
- Nxor( b1, b2 ): Return 1 if b1 and b2 are both zero or both non-zero,
otherwise return 0. Same as Not(Xor(b1,b2)), Xnor(b1,b2),
and IFF(b1,b2). May be used with bool arguments
(but not with {bmask, mbool} arguments)
- Odd( n ): Return 1 if the integer argument n is odd, else return 0
- OneOf( b1, b2, ... ): Return 1 if exactly one of the (2−10) arguments
is non-zero, and 0 otherwise.
May be used with bool arguments (but not with
{bmask, mbool} arguments)
- Or( b1, b2 ): Return 1 if either b1 or b2 is non-zero,
and return 0 otherwise.
May be used with bool arguments (but not with
{bmask, mbool} arguments)
- OutRangeEq( val, min, max ): Return 0 when (min ≤ val ≤ max),
1 otherwise. May be used with "bool" and constraint arguments.
- OutRangeNEq( val, min, max ): Return 0 when (min < val < max),
1 otherwise. May be used with "bool" and constraint arguments.
- OutSet( val, x1, x2, ... ): Return 1 when val is not the same value as any of the (1-8) other
arguments, else return 0. May be used with constraint arguments.
See also InSet().
- Permutations( total, n ): The number of different ways that n things may be selected
from total things. Both arguments are integers in (1-51),
and n < total.
See also Combinations().
- PopCount( n ): The number of 1-bits in the 32-bit integer n.
Same as BitCount().
- Pow( x, y ): Return the value of x raised to the y power.
The arguments may be integers or reals, but if x is negative,
y must be an integer. By definition Pow(0,0) = 1.
Pow(x,y) is the same as x^y and x**y.
- Pow2( n ): Return a floating point representation of 2n,
where n is an integer
in (0-300). Same as TwoToN(n). When n > 31,
do not set an int: variable to the return value.
- Prime( n ): Return TRUE if n (a positive 32-bit integer) is prime,
0 otherwise. May be used with a constraint argument expression.
- Rand( a, b ): Return a random floating point value between a
and b.
- Not reproducible
- See also IRand(),
RandSeed().
- RandSeed( n ):
Initialize the random generator seed for use with functions
Rand() and
IRand(). This function should be called before
calling Rand(), IRand(). Using the same seed for multiple runs should
produce the same sequence of random values provided there are no other
intervening random number calls. The value n is an unsigned integer
in [0−100,000] (silently enforced). N = 0 tells the system to pick a
random seed. A random seed is chosen if Rand() or IRand() is called
before RandSeed(). Multiple calls to RandSeed() are ignored. The
return value is the n actually used, or −1 if RandSeed() had
already been called. Here is a valid usage:
int: seed
seed = RandSeed(4913)
- Round( x ): The integer nearest to x. Values halfway between two
integers select the nearest even integer.
See also Ceiling(),
Floor().
Not to be confused with Trunc().
- Same( m1, m2, ...): Return T/F to: Are all the (2−13) integer argument values the
same? Accepts expresssions, constraintVars and regularVars as
arguments. (ConstraintVar types are {bool, mbool, bmask}).
See also Diff(),
NDiff(),
Diff().
- Sat( b1, ... ): A satisfiability function which returns TRUE
if any of its 1-6 arguments is non-zero (TRUE), otherwise
return 0. Any argument may be preceded by "−", which reverses
the value of the argument. That is, a zero argument is treated
as a 1, and a non-zero argument is treated as a 0. The "−" operator
reverses the value of its argument only in the context of
a satisfiability function, not in general.
These three sample asserts are equivalent:
bool: @j, @k, @m, @p
assert: sat( @j, NOT(@k), @m, @p )
assert: sat( @j, !@k, @m, @p )
assert: sat( @j, -@k, @m, @p )
Sat(@r,@s,@t) and Sat3(@r,@s,@t) produce identical results.
Sat() may be used with bool arguments (but not with
{bmask, mbool} arguments)
- Sat12( b1, b2 ): A disjunctive clause in a 2SAT problem.
Return 1 if exactly one of the 2 arguments is non-zero (TRUE),
otherwise return 0. Any argument may be preceded by "−", which
reverses the value of the argument. That is, a zero argument is
treated as a 1, and a non-zero argument is treated as a 0. The
"−" operator reverses the value of its argument only in the
context of a satisfiability function, not in general.
These three sample asserts are equivalent:
bool: @a, @b
assert: sat12( @a, NOT(@b) )
assert: sat12( @a, !@b )
assert: sat12( @a, -@b )
Sat12() is an alias for Xor2Sat(). Sat12() may be used with
bool arguments (but not with {bmask, mbool} arguments)
- Sat13( b1, b2, b3 ): A disjunctive clause in a 3SAT problem.
Return 1 if exactly one of the 3 arguments is non-zero (TRUE),
otherwise return 0. Any argument may be preceded by "−", which
reverses the value of the argument. That is, a zero argument is
treated as a 1, and a non-zero argument is treated as a 0. The
"−" operator reverses the value of its argument only in the
context of a satisfiability function, not in general.
These three sample asserts are equivalent:
bool: @a, @b, @c
assert: sat13( @a, NOT(@b), @c )
assert: sat13( @a, !@b, @c )
assert: sat13( @a, -@b, @c )
Sat13() may be used with bool arguments (but not with
{bmask:, mbool:} arguments)
- Sat14( b1, b2, b3, b4 ): A disjunctive clause in a satisfiability problem.
Return 1 if exactly one of the four arguments is non-zero
(TRUE), otherwise return 0. Any argument may be preceded by "−", which
reverses the value of the argument. That is, a zero argument is treated
as a 1, and a non-zero argument is treated as a 0. The "−" operator
reverses the value of its argument only in the context of
a satisfiability function, not in general.
These three sample asserts are equivalent:
bool: @a, @b, @c, @omega
assert: sat14( @a, NOT(@b), @c, @omega )
assert: sat14( @a, !@b, @c, @omega )
assert: sat14( @a, -@b, @c, @omega )
Sat14() may be used with bool arguments (but not with
{bmask, mbool} arguments)
- Sat15( b1, b2, b3, b4, b5 ): A disjunctive clause in a satisfiability problem.
Return 1 if exactly one of the five arguments is non-zero
(TRUE), otherwise return 0. Any argument may be preceded by "−", which
reverses the value of the argument. That is, a zero argument is treated
as a 1, and a non-zero argument is treated as a 0. The "−" operator
reverses the value of its argument only in the context of
a satisfiability function, not in general.
These three sample asserts are equivalent:
bool: @a, @b, @c, @d, @e
assert: sat15( @a, NOT(@b), @c, @d, @e )
assert: sat15( @a, !@b, @c, @d, @e )
assert: sat15( @a, -@b, @c, @d, @e )
Sat15() may be used with bool arguments (but not with
{bmask, mbool} arguments)
- Sat2( b1, b2 ): A disjunctive clause in a 2SAT problem.
Return 1 if either of the arguments is non-zero (TRUE), otherwise
return 0. Any argument may be preceded by "−", which reverses
the value of the argument. That is, a zero argument is treated
as a 1, and a non-zero argument is treated as a 0. The "−" operator
reverses the value of its argument only in the context of
a satisfiability function, not in general.
These three sample asserts are equivalent:
bool: @a, @b
assert: sat2( @a, NOT(@b) )
assert: sat2( @a, !@b )
assert: sat2( @a, -@b )
Sat2(@a,@b) and Sat(@a,@b) produce identical results.
Sat2() checks its the argument count, but Sat() doesn't.
Sat2() may be used with bool arguments (but not with
{bmask, mbool} arguments). Sat2() is similar to Or().
- Sat23( b1, b2, b3 ): A disjunctive clause in a 3SAT problem.
Return 1 if exactly two of the 3 arguments is non-zero (TRUE),
otherwise return 0. Any argument may be preceded by "−", which
reverses the value of the argument. That is, a zero argument is
treated as a 1, and a non-zero argument is treated as a 0. The
"−" operator reverses the value of its argument only in the
context of a satisfiability function, not in general.
These three sample asserts are equivalent:
bool: @a, @b, @c
assert: sat23( @a, NOT(@b), @c )
assert: sat23( @a, !@b, @c )
assert: sat23( @a, -@b, @c )
Sat13() may be used with bool arguments (but not with
{bmask, mbool} arguments)
- Sat24( b1, b2, b3, b4 ): A disjunctive clause in a satisfiability problem.
Return 1 if exactly two of the four arguments are non-zero
(TRUE), otherwise return 0. Any argument may be preceded by "−", which
reverses the value of the argument. That is, a zero argument is treated
as a 1, and a non-zero argument is treated as a 0. The "−" operator
reverses the value of its argument only in the context of
a satisfiability function, not in general.
These three sample asserts are equivalent:
bool: @a, @b, @c, @zip
assert: sat24( @a, NOT(@b), @c, @zip )
assert: sat24( @a, !@b, @c, @zip )
assert: sat24( @a, -@b, @c, @zip )
Sat24() may be used with bool arguments (but not with
{bmask, mbool} arguments)
- Sat25( b1, b2, b3, b4, b5 ): A disjunctive clause in a satisfiability problem.
Return 1 if exactly two of the five arguments are non-zero
(TRUE), otherwise return 0. Any argument may be preceded by "−", which
reverses the value of the argument. That is, a zero argument is treated
as a 1, and a non-zero argument is treated as a 0. The "−" operator
reverses the value of its argument only in the context of
a satisfiability function, not in general.
These three sample asserts are equivalent:
bool: @a, @b, @c, @d, @x3
assert: sat25( @a, NOT(@b), @c, @d, @x3 )
assert: sat25( @a, !@b, @c, @d, @x3 )
assert: sat25( @a, -@b, @c, @d, @x3 )
Sat25() may be used with bool arguments (but not with
{bmask, mbool} arguments)
- Sat3( b1, b2, b3 ): A disjunctive clause in a 3SAT problem.
Return 1 if any of the 3 arguments is non-zero (TRUE), otherwise
return 0. Any argument may be preceded by "−", which reverses
the value of the argument. That is, a zero argument is treated
as a 1, and a non-zero argument is treated as a 0. The "−" operator
reverses the value of its argument only in the context of
a satisfiability function, not in general.
These three sample asserts are equivalent:
bool: @a, @b, @c
assert: sat3( @a, NOT(@b), @c )
assert: sat3( @a, !@b, @c )
assert: sat3( @a, -@b, @c )
Sat3(@a,@b,@c) and Sat(@a,@b,@c) produce identical results.
Sat3() checks its the argument count, but Sat() doesn't.
Sat3() may be used with bool arguments (but not with
{bmask, mbool} arguments)
- Sat34( b1, b2, b3, b4 ): A disjunctive clause in a satisfiability problem.
Return 1 if exactly three of the four arguments are non-zero
(TRUE), otherwise return 0. Any argument may be preceded by "−", which
reverses the value of the argument. That is, a zero argument is treated
as a 1, and a non-zero argument is treated as a 0. The "−" operator
reverses the value of its argument only in the context of
a satisfiability function, not in general.
These three sample asserts are equivalent:
bool: @a, @b, @c, @zip
assert: sat34( @a, NOT(@b), @c, @zip )
assert: sat34( @a, !@b, @c, @zip )
assert: sat34( @a, -@b, @c, @zip )
Sat34() may be used with bool arguments (but not with
{bmask, mbool} arguments)
- Sat35( b1, b2, b3, b4, b5 ): A disjunctive clause in a satisfiability problem.
Return 1 if exactly three of the five arguments are non-zero
(TRUE), otherwise return 0. Any argument may be preceded by "−", which
reverses the value of the argument. That is, a zero argument is treated
as a 1, and a non-zero argument is treated as a 0. The "−" operator
reverses the value of its argument only in the context of
a satisfiability function, not in general.
These three sample asserts are equivalent:
bool: @a, @b, @c, @zip
assert: sat35( @a, NOT(@b), @c, @d, @x3 )
assert: sat35( @a, !@b, @c, @d, @x3 )
assert: sat35( @a, -@b, @c, @d, @x3 )
Sat35() may be used with bool arguments (but not with
{bmask, mbool} arguments)
- Sat4( b1, b2, b3, b4 ): A disjunctive clause in a 4SAT problem.
Return 1 if any of the 4 arguments is non-zero (TRUE), otherwise
return 0. Any argument may be preceded by "−", which reverses
the value of the argument. That is, a zero argument is treated
as a 1, and a non-zero argument is treated as a 0. The "−" operator
reverses the value of its argument only in the context of
a satisfiability function, not in general.
These three sample asserts are equivalent:
bool: @a, @b, @c, @d
assert: sat4( @a, NOT(@b), @c, @d )
assert: sat4( @a, !@b, @c, @d )
assert: sat4( @a, -@b, @c, @d )
Sat4(@a,@b,@c,@d) and Sat(@a,@b,@c,@d) produce identical results.
Sat4() checks its the argument count, but Sat() doesn't.
Sat4() may be used with bool arguments (but not with
{bmask:, mbool:} arguments)
- Sat45( b1, b2, b3, b4, b5 ): A disjunctive clause in a satisfiability problem.
Return 1 if exactly four of the five arguments are non-zero
(TRUE), otherwise return 0. Any argument may be preceded by "−", which
reverses the value of the argument. That is, a zero argument is treated
as a 1, and a non-zero argument is treated as a 0. The "−" operator
reverses the value of its argument only in the context of
a satisfiability function, not in general.
These three sample asserts are equivalent:
bool: @a, @b, @c, @zip
assert: sat45( @a, NOT(@b), @c, @d, @x3 )
assert: sat45( @a, !@b, @c, @d, @x3 )
assert: sat45( @a, -@b, @c, @d, @x3 )
Sat25() may be used with bool arguments (but not with
{bmask, mbool} arguments)
- Sat5( b1, b2, b3, b4, b5): A disjunctive clause in a 5SAT problem.
Return 1 if any of the 5 arguments is non-zero (TRUE), otherwise
return 0. Any argument may be preceded by "−", which reverses
the value of the argument. That is, a zero argument is treated
as a 1, and a non-zero argument is treated as a 0. The "−" operator
reverses the value of its argument only in the context of
a satisfiability function, not in general.
These three sample asserts are equivalent:
bool: @a, @b, @c, @d, @e
assert: sat5( @a, NOT(@b), @c, @d, @z )
assert: sat5( @a, !@b, @c, @d, @z )
assert: sat5( @a, -@b, @c, @d, @z )
Sat5(@a,@b,@c,@d,@e) and Sat(@a,@b,@c,@d,@e) produce identical results.
Sat5() checks its argument count, but Sat() doesn't.
Sat5() may be used with bool arguments (but not with
{bmask, mbool} arguments)
- SatN( N, b1, b2, ...): A disjunctive clause in a satisfiability problem.
Return 1 if exactly N of the remaining arguments are non-zero (TRUE),
otherwise return 0. Any argument may be preceded by "−", which reverses
the value of the argument. That is, a zero argument is treated
as a 1, and a non-zero argument is treated as a 0. The "−" operator
reverses the value of its argument only in the context of
a satisfiability function, not in general.
These three sample asserts are equivalent:
bool: @a, @b, @c, @glorp, @gold
assert: satN( 3, @a, NOT(@b), @c, @glorp, @gold )
assert: satN( 3, @a, !@b, @c, @glorp, @gold )
assert: satN( 3, @a, -@b, @c, @glorp, @gold )
Sat24() may be used with bool arguments (but not with
{bmask, mbool} arguments)
- Sin( r ): Sine of the angle r (radians)
- Sinh( x ): Hyperbolic Sine of r
- Sqrt( x ): The positive square root of x (x ≥ 0)
- SqrtAbs( x ): The positive square root of the absolute value of x
- Sum( n ): Sum of the integers from 1 to n := 1+2+3+...+n, (n > 0)
- SumDelta( a, d, n ): Sum of the arithmetic progression defined by its first term (a),
delta (d) and number of elements (n), with (d > 0) and
n is an integer > 0.
- Tan( r ): Tangent of the angle r (radians)
- Tanh( r ): Hyberbolic tangent of the angle r (radians)
- TnsrBit( tIn, op, d1, d2, d3, val ):
Operate on tensor tIn in the following way:
- Check that tIn exists and is initialized,
the indices d1,d2,d3 are in range (all 3 count
from 0), op is 1 of
{SETBIT,
GETBIT}.
IF these conditions are not met, RETURN -1.
- If op is SETBIT, set the
bit at d1,d2,d3
to 0 if val is zero, 1 otherwise, and RETURN 1
- If op is GETBIT,
RETURN the value of the bit
at d1,d2,d3. In this case, val is not used.
- SETBIT and
GETBIT
are ToQ internal constants.
- TnsrBitCount( tIn ):
Return the number of 1 bits in tensor tIn. May be used in
an assert statement. If an error is encountered, return -1.
- TnsrCompare( t1, c, t2 ):
Return TRUE(1) or FALSE(0) to the comparison of two conforming
tensors (t1 and t2).
The comparison operator (comp) must be one of the these
extended internal ToQ comparison constants:
{XTEQ,
XTNEQ,
XTLT,
XTLE,
XTGE,
XTGE}.
The comparisons scan left to right. May be used in an
assert statement. If an error is encountered, return -1.
- TnsrCopy( tOut, tIn ):
Copy tensor tIn to tOut. tIn and tOut must be
conforming tensors (all dimensions match). Return 0 if
successful, -1 if any errors encountered.
- TnsrGet( tIn, d1, d2, d3, nBits, just, fill ):
Return a 32-bit integer copy of the nBits bits starting at
index d1,d2,d3 of tensor tIn. NBits is in (1-32),
the indices start at 0, and d3 varies first. An error
occurs if the request extends beyond the size of tIn.
When nBits is not 32, the just and fill arguments
determine the justification and fill for the returned 32-bit
integer. These internal ToQ constants constitute the valid
values for the justification and fill arguments:
just fill
------------ ------------
LEFTS Left side FILLZERO Fill with 0s
RIGHTS Right side FILLLONE Fill with 1s
See also
TnsrGetStk(),
TnsrPut(),
TnsrPutStk().
- TnsrGetStk( tIn, d1, d2, just, fill ):
Return a 32-bit integer copy of the stack starting at index
d1,d2 of tensor tIn. The stack size is given by
the d3 dimension of tIn. and must be in (1-32), and
the indices start at 0 and d3 varies first. An error
occurs if the request extends beyond the size of tIn.
When the size is not 32, the just and fill arguments
determine the justification and fill for the returned 32-bit
integer. These internal ToQ constants constitute the valid
values for the justification and fill arguments:
just fill
------------ ------------
LEFTS Left side FILLZERO Fill with 0s
RIGHTS Right side FILLLONE Fill with 1s
Return 0 if successful, -1 if any errors encountered.
See also
PutStk(),
TnsrGet(),
TnsrPut().
- TnsrInit( tOut, word ):
Initialize tensor tOut with copies of 32-bit word word.
TnsrInit() initialization does not honor tensor boundaries,
rather it just populates the tensor with contiguous 32-bit
entities. Most frequent values for word are 0 and
MASK32. Return 0 if successful, -1 if any errorsencountered.
- TnsrMtx( t, m, dir, fill ):
Copy data between tensor t and matrix m.
Dir is one of {TNSRTOMTX,MTXTTOTNSR}. After the copy, both
will contain the same data, but m may contain extra row(s).
Tensor dimensions are (nX,nY,nZ), and matrix dimensions are
(row,col). Col must be an integer multiple of nZ.
The source must be initialized. M(nBits) must be at
least as big as the tensor. When m is larger than t
- TNSRTOMTX: fill is used to fill the extra rows.
- MTXTOTNSR: a warning message will be issued.
Fill is one of (FILLZERO,FILLONE}.
- TnsrNot( tOut, tIn ):
Flip each bit of tIn to create tOut. tIn and tOut
must be conforming tensors (d1,d2,d3 match)), but they need
not be different. Return 0 if successful, -1 if any
errors encountered.
- TnsrOp( tOut, t1, op, t2 ):
Set tensor tOut to t1 op t2 - where all three vectors are
conforming,
and op is one of the extended bit-by-bit binary operators: {
XTAND,
XTANDNOT,
XTOR,
XTORNOT,
XTXOR,
XTNOR,
XTXNOR,
XTIFF,
XTIMPLIES }.
These terms are
internal ToQ constants.
(Note -
{XTANDNOT,
XTORNOT,
XTIMPLIES }
are not commutative.)
These terms are internal ToQ constants; they perform
bit-by-bit operations. V1 and v2 must be different,
but vOut is not restricted. Return 0 if successful,
-1 if any errors encountered. See also TnsrOp3(),
- TnsrOp3( tOut, op1, t1, op2, op3, t2 ):
Set tensor tOut to ((op1 t1) op2 (op3 t2)) -
where all three tensors are conforming, and op1 and
op3 are one of
{XTNOT,
XTNOOP},
and op2 is one of the extended bit-by-bit binary operators: {
XTAND,
XTANDNOT,
XTOR,
XTORNOT,
XTXOR,
XTNOR,
XTXNOR,
XTIFF,
XTIMPLIES }.
These terms are
internal ToQ constants.
(Note -
{XTANDNOT,
XTORNOT,
XTIMPLIES }
are not commutative.)
These terms are internal ToQ constants; they perform
bit-by-bit operations. V1 and v2 must be different,
but vOut is not restricted. Return 0 if successful, or
-1 if any errors encountered. See also VectOp(), TnsrOp2().
- TnsrPut( tOut, d1, d2, d3, word, nBits, fill ):
Place the low-order nBits bits of the 32-bit word word
into tensor tOut starting at index d1,d2,d3. NBits
is in (1-32) and d1,d2,d3 start at 0 and d3 varies
first. An error occurs if the request extends beyond
the size of tOut. Return 0 if successful,
-1 if any errors encountered. Note - if tOut is
uninitialized on input to TnsrPut(), it is initialized
via fill before the data move. Fill is 1 of
{FILLZERO,FILLONE}. When tOut has already been
initialized, fill is ignored.
See also
TnsrGet(),
TnsrGetStk(),
TnsrPutStk().
- TnsrPutStk( tOut, d1, d2, word, fill ):
Place d3 bits of the 32-bit word word into
tensor tOut starting at index d1,d2. D3 is
the 3rd dimension of tensor tOut. and must be in
(1-32), d1,d2,d3 start at zero, and d3 varies
first. An error occurs if the request extends beyond
the size of tOut. When d3 is not 32, just determines
whether to use the left- or right-most bits of word.
If tOut is uninitialized on input to TnsrPutStk(),
it is initialized via fill before the data move.
When tOut has already been initialized, fill is ignored.
These internal ToQ constants constitute the valid
values for the justification and fill arguments:
just fill
------------ ------------
LEFTS Left side FILLZERO Fill with 0s
RIGHTS Right side FILLLONE Fill with 1s
Return 0 if successful, -1 if any errors encountered.
See also
TnsrPut(),
TnsrGet(),
TnsrGetStk().
- TnsrReady( tIn ):
Return 1 if tensor tIn has been initialized, 0 if not, or -1
if tIn is not a tensor.
- TnsrVect( t, v, dir, fill ):
Copy all data between tensor t and vector v.
dir is one of
{TNSRTOVECT,
VECTTOTNSR}.
After the copy,
both will contain the same data, but v may contain extra
bits on the end. The source must be initialized.
v(nBits) must be at least as big as the tensor. When
v is larger than t, fill is used to determine
how to fill the excess for TNSRTOVECT. For VECTTOTNSR, a
warining is issued when v is larger than t.
fill
must be one of
{FILLZERO,
FILLONE}.
Return 0 if successful, -1 if any errors encountered.
- Trunc( x ): The integer component of x − not to be confused
with Floor() or Ceiling().
x Trunc(x) Floor(x) Ceiling(x)
--- -------- -------- ----------
PI 3 3 4
-PI -3 -4 -3
- TwoOf( b1, b2, ... ): Return 1 if exactly two of the (2−10)
arguments are non-zero, and 0 otherwise.
May be used with bool arguments (but not with
{bmask, mbool} arguments)
- TwoToN( n ): Return a floating point representation of 2n,
where n is an integer
in (0-300). Same as Pow2(n). When n > 31,
do not set an int: variable to the return value.
- UpperBd( v ): Return the largest value that the constraint variable v can take on. This special function behaves like a compile-time
constant rather than a regular function, and thus can appear
anywhere after the declarations, but not in an assert statement
nor in a QUANT block. Its argument must be of type bool, mbool
or bmask. The argument may not be an expression.
For example:
bool: @pair
mbool: 5,20,2, @batch
bmask: 2,4, @mask
int: lastP, lastB, lastM
lastP = UpperBd(@pair)
lastB = UpperBd(@batch)
lastM = UpperBd(@mask)
would set lastP to 1, lastB to 19 and lastM to 12 = 0(2)1100.
See also
LowerBd(),
NumbVals().
- VectBit( v, op, index, val ): Return the number of 1 bits in vector v.
Operate on vector v in the following way:
- Check that v exists and is initialized,
index is in range (count
from 0), op is 1 of
{SETBIT,
GETBIT}.
If these conditions are not met, RETURN -1.
- If op is SETBIT, set the
bit at index
to 0 if val is zero, 1 otherwise, and RETURN 1
- If op is GETBIT,
RETURN the value of the bit
at index. In this case, val is not used.
- SETBIT and
GETBIT
are ToQ internal constants.
- VectBitCount( v ): Return the number of 1 bits in vector v.
May be used in an assert statement. If an error is encountered,
return −1.
- VectCompare( v1, comp, v2 ): Return TRUE(1) or FALSE(0) to the comparison of two conforming
vectors (v1 and v2). V1 and v2 must be different.
The comparison operator (comp) must be one of the following
internal ToQ constants { VECTEQ,
VECTNEQ, VECTLT,
VECTLE, VECTGT,
VECTGE }. The comparisons scan left to right. May be used
in an assert statement. If an error is encountered, return −1.
- VectConcat( vOut, v1, indx1, n1, v2, indx2, n2, fill ): Build vector vOut by concatenating vectors v1 and v2.
Pick up n1 bits from v1 starting at bit indx1
(counting starts at zero), then add n2 bits from v2
starting at bit indx2. N1 + n2 must not exceed the
constant size of vOut. If the sum is less than the size
of vOut - the fill argument determines how to fill
in the remaining bits:
fill
------------
FILLZERO Fill with 0s
FILLLONE Fill with 1s
Return 0 if successful, −1 if any errors encountered.
- VectCopy( vOut, vIn
): Copy vector vIn to vOut. vIn and vOut must be
conforming vectors (same size).
See also VectInsert().
Return 0 if successful, −1 if any errors encountered.
- VectGet( v, indx, n, just, fill ): Return a 32-bit integer copy of the n bits starting at
index indx of vector v. N is in (1-32),
and indx
starts at 0 and counts left to right. An error occurs if
the request extends beyond the size of v. When n is not
32, the just and fill arguments determine the justification
and the fill for the returned 32-bit integer. These internal
ToQ constants constitute the valid values for
the justification and fill arguments:
just fill
------------ ------------
LEFTS Left side FILLZERO Fill with 0s
RIGHTS Right side FILLLONE Fill with 1s
See also VectInsert().
Return 0 if successful, −1 if any
errors encountered.
- VectInit( vOut, mask
): Initialize vector vOut with
all masks. Typical values
for the 32-bit entity mask include 0, −1 (all ones),
MASK3201, MASK3240, ... Return 0 if successful, −1 if
any errors encountered.
- VectInsert( vOut, indx1, vIn, indx2, nBits, fill ): Insert nBits from vector vIn starting at indx2 into
vector vOut starting at bit indx1.
See also VectPut().
Return 0 if successful, −1 if any errors encountered.
Note - if vOut is uninitialized on input to VectInsert(),
it is initialized via fill before the data move.
Fill is 1 of
{ FILLZERO,
FILLONE }.
When vOut has
already been initialized, fill is ignored.
- VectNot( vOut, vIn ): Flip each bit of vIn to create vOut.
vIn and vOut
must be conforming vectors (same size), but they need
not be different. Return 0 if successful, −1 if any
errors encountered.
- VectOp( vOut, v1, op, v2 ): Set vector vOut to v1 op v2 - where all three vectors are
conforming,
and op is one of extended bit-by-bit binary operators: {
XTAND,
XTANDNOT,
XTOR,
XTORNOT,
XTXOR,
XTNOR,
XTXNOR,
XTIFF,
XTIMPLIES }.
These terms are
internal ToQ constants; they perform bit-by-bit operations.
V1 and v2 must be different, but vOut is not restricted.
Return 0 if successful, −1 if any errors encountered.
See also VectOp2(),
VectOp3().
- VectOp2( vOut, fill, nBits, indxV, v1, indx1, op, v2, indx2): Set vector vOut to fill, then replace the nBits bits
starting at indxV with the result of v1[indx1] op v2[indx2].
The vectors must be big enough to accommodate the requests.
The vectors need not be conforming or different. Fill is one
of { FILLZERO, FILLONE },
and op is one of {
XTAND,
XTANDNOT,
XTOR,
XTORNOT,
XTXOR,
XTNOR,
XTXNOR,
XTIFF,
XTIMPLIES }.
These terms are internal
ToQ constants; they perform bit-by-bit operations. Return 0
if successful, −1 if any errors encountered.
See also VectOp(),
VectOp3().
- VectOp3( vOut, op1, v1, op2, op3, v2 ): Set vector vOut to
((op1 v1) op2 (op3 v2) -
where all three vectors are conforming, and op1 and
op3 are one of
{XTNOT,
XTNOOP},
(unary operators),
and op2 is one of the extended bit-by-bit binary
operators:
XTAND,
XTANDNOT,
XTOR,
XTORNOT,
XTXOR,
XTNOR,
XTXNOR,
XTIFF,
XTIMPLIES }.
(Note -
{XTANDNOT,
XTORNOT,
XTIMPLIES }
are not commutative.)
These terms are internal ToQ constants; they perform
bit-by-bit operations. V1 and v2 must be different,
but vOut is not restricted. Return 0 if successful, or
-1 if any errors encountered.
See also VectOp(),
VectOp2().
- VectPaint( vOut, word, nBits ): Fill vector vOut (left to right) with copies of the lower
nBits bits of the 32-bit word word. NBits is in (3-32).
The last (rightmost) bits of Vout may contain only the
expected subset of word.
See also VectInit(). Return 0
if successful, −1 if any errors encountered.
(not yet available)
- VectProc( vOut, vIn,
action, w1, w2, nBits, delta ): Process vector
vIn via action action which operates on the
low order nBits of 32-bit word w1. Actions
are
VECTCOUNT - return the number of occurrences of w1.
VECTFIND - return the location of the first occurrence
of w1 in vIn (or −1 if not found).
VECTLAST - return the location of the last occurrence
of w1 in vIn (or −1 if not found).
VECTREPL - copy vIn to vOut, and replace all
occurrences of w1 with w2.
Only VECTREPL uses vOut and w2. Delta
(range: 1−nBits)
tells how many bits to skip on a miss (a hit always skips
nBits bits). Return −1 if unsuccessful.
(not yet available)
- VectPut( vOut, indx, word, nBits, fill ): Place the low-order nBits bits of the 32-bit word word
into vector vOut starting at index indx. NBits is
in (1-32) and indx starts at 0 and counts left to right.
An error occurs if the request extends beyond the size of
vOut. See also VectInsert().
Return 0 if successful,
−1 if any errors encountered. Note - if vOut is
uninitialized on input to VectPut(), it is initialized
via fill before the data move. Fill is one of
{FILLZERO,FILLONE}. When vOut has already been
initialized, fill is ignored.
- VectReady( vIn
): Return 1 if vector vIn has been initialized, 0 if not, or -1
if vIn is not a vector.
- VectReverse( vOut, vIn ): Set vOut to a bit-by-bit reverse of
vIn. The input
vectors must be conforming, but they need not be different.
Return 0 if successful, −1 if any errors encountered.
- VectShift( vOut, vIn, n, dir, fill ): Set vOut to a copy of vIn shifted n bits in direction
dir with fill set by fill. vOut and vIn must be
conforming vectors, but they need not be different. These
internal ToQ constants constitute the valid values for
the direction and fill arguments:
dir fill
----------- ------------
LEFTS Left shift FILLZERO Fill with 0s
RIGHTS Right shift FILLLONE Fill with 1s
LEFTC Left circular shift
RIGHTC Right circular shift
The fill argument is required for all cases, but it is
ignored for circular shifts. Return 0 if successful,
−1 if any errors encountered.
- Xnor( b1, b2
): Return 1 if b1 and b2 are both
zero or both non-zero, otherwise return 0. Same as
Not(Xor(b1,b2)), NXor(b1,b2), and IFF(b1,b2). May be used with
bool arguments (but not with {bmask, mbool} arguments)
- Xor( b1, b2
): Return 1 if b1 is non-zero and b2
is 0, or if b2 is non-zero and b1 is 0. When both
expressions are zero or both are non-zero, return 0. May be used
with bool arguments (but not with {bmask, mbool} arguments)
- Xor2Sat( b1, b2
): A satisfiability function which returns TRUE if
its two arguments are different (that is, one is zero and one is
non-zero), otherwise return 0. Any argument may be preceded by
"−", which reverses the value of the argument. That is, a
zero argument is treated as a 1, and a non-zero argument is treated as
a 0. The "−" operator reverses the value of its argument
only in the context of a satisfiability function, not in general.
These three sample asserts are equivalent:
bool: @x, @y
assert: xor2sat( NOT(@x), @y )
assert: xor2sat( !@x, @y )
assert: xor2sat( −@x, @y )
Xor2Sat() checks its argument count. Xor2Sat() is an alias for
Sat12(). Xor2Sat() may be used with bool arguments (but
not with {bmask, mbool} arguments)
- Xor3Sat( b1, b2, b3 ): A satisfiability function which returns TRUE if exactly one
or all of its 3 arguments is non-zero, otherwise return 0.
Any argument may be preceded by "−", which reverses
the value of the argument. That is, a zero argument is treated
as a 1, and a non-zero argument is treated as a 0. The "−" operator
reverses the value of its argument only in the context of
a satisfiability function, not in general.
These three sample asserts are equivalent:
bool: @w, @x, @y
assert: xor3sat( @w, NOT(@x), @y )
assert: xor3sat( @w, !@x, @y )
assert: xor3sat( @w, −@x, @y )
Xor3Sat() checks its argument count. Xor3Sat() may be used with
bool arguments (but not with {bmask, mbool} arguments)
NAE3Sat( b1, b2, b3 ) |
Sat2( b1, b2 ) |
NAE4Sat( b1, b2, b3, b4 ) |
Sat23( b1, b2, b3 ) |
NAE5Sat( b1, b2, b3, b4, b5 ) |
Sat24( b1, b2, b3, b4 ) |
NAESat( b1, b2, ... ) |
Sat25( b1, b2, b3, b4, b5 ) |
NAESat3( b1, b2, b3 ) |
Sat3( b1, b2, b3 ) |
NAESat4( b1, b2, b3, b4 ) |
Sat34( b1, b2, b3, b4 ) |
NAESat5( b1, b2, b3, b4, b5 ) |
Sat35( b1, b2, b3, b4, b5 ) |
NAESatN( N, b1, b2, ... ) |
Sat4( b1, b2, b3, b4 ) |
Sat( b1, ... ) |
Sat45( b1, b2, b3, b4, b5 ) |
Sat12( b1, b2 ) |
Sat5( b1, b2, b3, b4, b5) |
Sat13( b1, b2, b3 ) |
SatN( N, b1, b2, ...) |
Sat14( b1, b2, b3, b4 ) |
Xor2Sat( b1, b2 ) |
Sat15( b1, b2, b3, b4, b5 ) |
Xor3Sat( b1, b2, b3 ) |
See also the satisfiability directive.
Click here for a discussion of satisfiability
problems.
The vect: (and vectp:) data typea define
1-D bit arrays of arbitrary length for use in a
ToQ program (a .toq file) or in a
variable-value file (-z option or
initfile: directive). Size is set on the declaration, must be a
multiple of 32, and cannot be changed.
Vectors are actually packed bit arrays, which can be set,
interrogated, and interact with other vectors, as well as matrices
and tensors. Direct access to vect
variables is restricted, but there are a variety of functions available
for data manipulation (enter: "toq -H vect"
or click here for details).
When using vectors in the functions listed below, they are
treated atomically, that is, operations interact with the entire
vector, so there is no need to be aware of word boundaries.
Some access is limited to (1-32) bits, and access may be over 32-bit
boundaries. Vect variables are uninitialized (using an
uninitialzed variable is a fatal error).
When initialized, the entire vector must be covered.
Use the > symbol to fill out vectors (as in sample 3).
Format is
vect: nBits, v1, v2, ...
where nBits is an integer (>0) multiple of 32.
Here are some samples:
vect: 96, v1, v2, xmask = 0xAAAAAAAA,0xFFFFFFFF,37
vect: 64, ymask = 2*0xAFAFAFAF, tbar=2*0
vect: 96, vv = 0x1234CDEF,>0, wv = >MASK32, rr = >0
Each initiation value is 32 bits.
MtxVect(M,V,dir) |
VectInit(Vout,word) |
MtxVectFrag(M,V,dir,...) |
VectInsert(Vout,...) |
MtxVectInit(mOut,Vin,...) |
VectNot(Vout,Vin) |
MtxVectOp(Mout,opFlag,...) |
VectOp(Vout,V1,op,V2) |
MtxVectOp3(Mout,op1,...) |
VectOp2(Vout,...) |
TnsrVect(T,V,dir,j,f) |
VectOp3(Vout,...) |
VectBit(Vin,op,indx,val) |
VectPaint(Vout,p,n) |
VectBitcount(Vin,nIgnore) |
VectProc(Vout,...) |
VectCompare(V1,c,V2) |
VectPut(Vout,i,w,n) |
VectConcat(Vout,...) |
VectReady(Vin) |
VectCopy(Vout,Vin) |
VectReverse(Vout,Vin) |
VectGet(Vin,i,n,j,f) |
VectShift(Vout,Vin,n,d,f) |
- GETBIT --
op argument to VectBit().
- FILLONE
-- Argument (fill with 1s) to
VectShift(),
VectGet(),
VectPut()
- FILLZERO
-- Argument (fill with 0s) to
VectShift(),
VectGet(),
VectPut()
- LEFTC --
Direction argument to VectShift() for circular left shift
- LEFTS --
Direction argument to VectShift() for
left shift, and VectGet()
for left side justification
- MTXTOVECT --
Direction indicator for MtxVect()
- TNSRTOVECT --
Direction indicator for TnsrVect()
- RIGHTC --
Direction argument to VectShift() for circular right shift
- RIGHTS --
Direction argument to VectShift() for right
shift, and
VectGet() for right side justification
- SETBIT --
op argument to VectBit().
- VECTTOMTX --
Direction indicator for MtxVect()
- VECTTOTNSR --
Direction indicator for TnsrVect()
- XTAND --
Vector operator (AND) for
VectOp(),
VectOp2(),
VectOp3
- XTANDNOT --
Vector operator (AND-NOT) for
VectOp(),
VectOp2()
- XTEQ --
Argument (Equal) to VectCompare()
- XTGE --
Argument (Greater than or Equal) to VectCompare()
- XTGT --
Argument (Greater than) to VectCompare()
- XTIFF --
Vector operator (IFF) for
VectOp(),
VectOp2(),
VectOp3
- XTIMPLIES --
Vector operator (IMPLIES) for
VectOp(),
VectOp2(),
VectOp3
- XTLE --
Argument (Less than or Equal) to VectCompare()
- XTLT --
Argument (Less than) to VectCompare()
- XTNEQ --
Argument (Not Equal) to VectCompare()
- XTNOOP --
Vector operator (No-op) for
VectOp3
- XTNOR --
Vector operator (NOR) for
VectOp(),
VectOp2(),
VectOp3
- XTNOT --
Unary vector operator (NOT) for
VectOp3
- XTOR --
Vector operator (OR) for
VectOp(),
VectOp2(),
VectOp3
- XTORNOT --
Vector operator (OR-NOT) for
VectOp(),
VectOp2
- XTXNOR --
Vector operator (XNOR) for
VectOp(),
VectOp2(),
VectOp3
- XTXOR --
Vector operator (XOR) for
VectOp(),
VectOp2(),
VectOp3
The mtx: (and mtxp:) data types define
2-D bit arrays of arbitrary length for use in a ToQ
program (a .toq file) or in a variable-value file (-z option or
initfile: directive). Size is set on the declaration
as nRows and nCols.
Matrices are actually packed bit arrays, which can be set,
interrogated, and interact with other matrices, as well as
vectors and tensors.
The dimensions cannot be changed.
When using matrices in the functions listed below, they are
treated atomically, that is, operations interact with the
entire matrix, so there is no need to be aware of word/row/column
boundaries. Direct access
to mtx variables is restricted, but there are a variety
of functions available for data manipulation
(see the list below
or click on any entry in the list for details).
Mtx variables are uninitialized
(using an uninitialzed variable is a fatal error).
When initialized, the entire matrix must be covered.
Use the > symbol to fill out vectors (as in sample 3 below).
Format is
mtx: nRows,nCols, m1, m2, ...
where "nRows" is an integer (>0) and "nCols" is
an integer multiple of 32. Here are some samples:
mtx: 16,96, m1, m2, mMask = 0xAAAAAAAA,47*0
mtx: 30,64, ymask = 60*0xAFAFAFAF, zbar = 60*0
mtx: 12,128, tPush = >MASK3202, tPull = >MASK32
Each initiation value is 32 bits. In the examples
above, "47*0" means 47 32-bit zeroes, and the >
indicates initialization of the remaining bits, and
"MASK32" represents 32 bits of 1s (MASK32 and MASK3202
are ToQ internal 32-bit constants).
MtxBit(Min,op,r,c,val) |
MtxPaint(Mout,word,...) |
MtxBitCount(Min,nIgnore) |
MtxProc(Mout,Min,...) |
MtxCompare(M1,comp,M2,...) |
MtxPut(Mout,nBits,...) |
MtxConcat(Mout,M1,M2) |
MtxReady(Min) |
MtxCopy(Mout,Min) |
MtxReverse(Mout,Min) |
MtxFlip(Mout,Min) |
MtxShift(Mout,Min,n,...) |
MtxGet(Min,indx,n,...) |
MtxSwap(Mout,Min,...) |
MtxInit(Mout,word) |
MtxVect(M,V,dir) |
MtxInsertM(Mout,indx1,...) |
MtxVectInit(Mout,Vin,fill) |
MtxInsertV(Mout,indx1,...) |
MtxVectLns(M,V,dir,...) |
MtxNot(Mout,Min) |
MtxVectOp(Mout,opFlag,...) |
MtxOp(Mout,M1,op,M2) |
MtxVectOp3(Mout,opFlag,...) |
MtxOp3(Mout,op1,M1,...) |
TnsrMtx(T,M,dir,fill) |
- GETBIT --
op argument to MtxBit().
- FILLONE
-- Argument (fill with 1s) to
MtxShift(),
MtxGet(),
MtxPut()
- FILLZERO
-- Argument (fill with 0s) to
MtxShift(),
MtxGet(),
MtxPut()
- LEFTC --
Direction argument to MtxShift() for circular left shift
- LEFTS --
Direction argument to MtxShift() for
left shift, and MtxGet()
for left side justification
- MTXCOL --
"SwFlag" argument to
MtxVectOp()
signifying column swap, and dir argument to
MtxGet() and
MtxPut().
- MTXROW --
"SwFlag" argument to
MtxVectOp()
signifying row swap, and dir argument to
MtxGet() and
MtxPut().
- MTXTOVECT --
Direction indicator for MtxVect()
- RIGHTC --
Direction argument to MtxShift() for circular right shift
- RIGHTS --
Direction argument to MtxShift() for right
shift, and
MtxGet() for right side justification
- SETBIT --
op argument to MtxBit().
- TNSRTOVECT --
Direction indicator for TnsrVect()
- VECTTOMTX --
Direction indicator for MtxVect()
- VECTTOTNSR --
Direction indicator for TnsrVect()
- XTAND --
Matrix operator (AND) for
MtxOp(),
MtxOp3
- XTANDNOT --
Matrix operator (AND-NOT) for
MtxOp(),
MtxOp3()
- XTEQ --
Argument (Equal) to MtxCompare()
- XTGE --
Argument (Greater than or Equal) to MtxCompare()
- XTGT --
Argument (Greater than) to MtxCompare()
- XTIFF --
Matrix operator (IFF) for
MtxOp(),
MtxOp3
- XTIMPLIES --
Matrix operator (IMPLIES) for
MtxOp()
- XTLE --
Argument (Less than or Equal) to MtxCompare()
- XTLT --
Argument (Less than) to MtxCompare()
- XTNEQ --
Argument (Not Equal) to MtxCompare()
- XTNOOP --
Matrix operator (No-op) for
MtxOp3
- XTNOR --
Matrix operator (NOR) for
MtxOp(),
MtxOp3
- XTNOT --
Unary matrix operator (NOT) for
VectOp3
- XTORNOT --
Matrix operator (OR-NOT) for
MtxOp(),
- XTOR --
Matrix operator (OR) for
MtxOp(),
MtxOp3
- XTXNOR --
Matrix operator (XNOR) for
MtxOp(),
MtxOp3
- XTXOR --
Matrix operator (XOR) for
MtxOp(),
MtxOp3
The tnsr: (and tnsrp:) data types define
3-D bit arrays of arbitrary length for use in a ToQ
program (a .toq file) or in a variable-value file (-z option or
initfile: directive). Size is set on the declaration
as (nx,ny,nz),
internally called rows, columns, stacks.
(nx,ny,nz) are
set at compile-time and cannot be changed.
Tensors are actually packed bit arrays, which can be
set, interrogated, and interact with other tensors,
as well as vectors and matrices.
Direct access to tensor variables is restricted, but
there are a variety of functions available for data
manipulation (see the list below or click on any entry
in the list for details).
When using tensors in the functions listed below, they are
treated atomically, that is, operations interact with the
entire tensor, so there is no need to be aware of
word/row/column/stack boundaries.
Tensor variables are uninitialized (using an uninitialzed
variable is a fatal error). When a tensor is inititialized,
the entire tensor must be covered. Use the >
symbol to fill out tensors (as in sample 2).
The format is
tnsr: nx,ny,nz, t1, t2, ...
where nx, ny, nz are integers (>0). Here are some samples:
tnsr: 8,8,10, t1, t2 = 0x6789FFFF, -1, 0, >0x55555555
tnsr 4,5,6, tBox = >MASK32
Each initiation value is 32 bits. In the examples
above, the > indicates initialization of the remaining
bits, and both "-1" and "MASK32" represent 32 bits
of 1s. Keep in mind that tensors are packed, so the
initialization values are spread over the variable range.
Initialization values beyond the variable's range are
ignored.
TnsrBit(Tin,op,d1,d2,d3,val) |
TnsrNot(Tout,Tin) |
TnsrBitcount(Tin) |
TnsrOp(Tout,T1,op,T2) |
TnsrCompare(T1,c,T2) |
TnsrOp3(Tout,...) |
TnsrCopy(Tout,tIn) |
TnsrPut(Tout,d2,d2,d3,w,n) |
TnsrGet(Tin,d2,d2,d3,n,j,f) |
TnsrPutStk(Tout,d2,d2,w,f) |
TnsrGetStk(Tin,d2,d2,j,f) |
TnsrReady(Tin) |
TnsrInit(Tout,word) |
TnsrVect(T,V,dir,fill) |
TnsrMtx(T,M,dir,fill) |
- GETBIT --
op argument to TnsrBit().
- FILLONE
-- Argument (fill with 1s) to
TnsrGet(),
TnsrGetStk(),
TnsrPut(),
TnsrPutStk()
- FILLZERO
-- Argument (fill with 0s) to
TnsrGet(),
TnsrGetStk(),
TnsrPut(),
TnsrPutStk()
- LEFTS --
Direction argument to
TnsrGet(),
TnsrGetStk(),
TnsrPut(),
TnsrPutStk()
for left side justification
- MTXTOTNSR --
Direction indicator for
TnsrMtx()
- RIGHTS --
Direction argument to
TnsrGet(),
TnsrGetStk(),
TnsrPut(),
TnsrPutStk()
for right side justification
- SETBIT --
op argument to TnsrBit().
- TNSRTOMTX --
Direction indicator for
TnsrMtx()
- TNSRTOVECT --
Direction indicator for
TnsrVect()
- VECTTOTNSR --
Direction indicator for
TnsrVect()
- XTAND --
Tensor operator (AND) for
TnsrOp(),
TnsrOp3
- XTANDNOT --
Tensor operator (AND-NOT) for
TnsrOp()
- XTEQ --
Argument (Equal) to TnsrCompare()
- XTGE --
Argument (Greater than or Equal) to TnsrCompare()
- XTGT --
Argument (Greater than) to TnsrCompare()
- XTIFF --
Tensor operator (IFF) for
TnsrOp()
TnsrOp3
- XTIMPLIES --
Tensor operator (IMPLIES) for
TnsrOp(),
TnsrOp3
- XTLE --
Argument (Less than or Equal) to TnsrCompare()
- XTLT --
Argument (Less than) to TnsrCompare()
- XTNEQ --
Argument (Not Equal) to TnsrCompare()
- XTNOOP --
Tensor operator (No-op) for
TnsrOp3
- XTNOR --
Tensor operator (NOR) for
TnsrOp(),
TnsrOp3
- XTNOT --
Unary tensor operator (NOT) for
VectOp3
- XTOR --
Tensor operator (OR) for
TnsrOp(),
TnsrOp3
- XTORNOT --
Tensor operator (OR-NOOR-NT
TnsrOp()
TnsrOp3
- XTXNOR --
Tensor operator (XNOR) for
TnsrOp(),
TnsrOp3
- XTXOR --
Tensor operator (XOR) for
TnsrOp(),
TnsrOp3
- COLVECTMTX --
"OpFlag" argument to
MtxVectOp() and
MtxVectOp3
signifying bit-by-bit Column Vector op Matrix.
- CUBERT2 --
3√2 = 1.259921049894873
- CUBERT3 --
3√3 = 1.442249570307408
- D2RADIANS -- 2π/360
= 0.0174532925199433 rad/deg = Angle conversion factor.
D2RADIANS * degrees = radians
- ELECTRIC
-- Electric constant = 8.854187817×10−12 F/m:
permittivity of vacuum
- ENAT --
e = 2.718281828459045 = base of the natural logarithms
- FILLONE
-- Argument (fill with 1s) to
VectShift() and
VectGet()
- FILLZERO
-- Argument (fill with 0s) to
VectShift() and
VectGet()
- FOURTHPI
-- (¼)π = 0.785398163397448
- GETBIT --
op argument to
MtxBit(),
TnsrBit(),
VectBit().
- HALFPI --
(½)π = 1.5707963267949
- JOSEPHSON -- Josephson constant
- LEFTC --
Direction argument to VectShift() for circular left shift
- LEFTS --
Direction argument to VectShift() for
left shift, and VectGet()
for left side justification
- LN10 --
ln(10) = loge(10) = natural logarithm of 10
= 2.302585092994046
- LN2 -- ln(2)
= loge(2) = natural logarithm of 2
= 0.693147180559945
- LN3 -- ln(3)
= loge(3) = natural logarithm of 3
= 1.098612288668109691395
- LOG102 --
log10(2) = 0.301029995663981
- LOG103 --
log10(3) = 0.477121254719662
- LOG10E --
log10(e) = 0.44429448190325182765
- MASK02 -- Low order 2 bits = 0x00000003 = 0o00000000003
- MASK03 -- Low order 3 bits = 0x00000007 = 0o00000000007
- MASK04 -- Low order 4 bits = 0x0000000F = 0o00000000017
- MASK05 -- Low order 5 bits = 0x0000001F = 0o00000000037
- MASK06 -- Low order 6 bits = 0x0000003F = 0o00000000077
- MASK07 -- Low order 7 bits = 0x0000007F = 0o00000000177
- MASK08 -- Low order 8 bits = 0x000000FF = 0o00000000377
- MASK09 -- Low order 9 bits = 0x000001FF = 0o00000000777
- MASK10 -- Low order 10 bits = 0x000003FF = 0o00000001777
- MASK11 -- Low order 11 bits = 0x000007FF = 0o00000003777
- MASK12 -- Low order 12 bits = 0x00000FFF = 0o00000007777
- MASK13 -- Low order 13 bits = 0x00001FFF = 0o00000017777
- MASK14 -- Low order 14 bits = 0x00003FFF = 0o00000037777
- MASK15 -- Low order 15 bits = 0x00007FFF = 0o00000077777
- MASK16 -- Low order 16 bits = 0x0000FFFF = 0o00000177777
- MASK17 -- Low order 17 bits = 0x0001FFFF = 0o00000377777
- MASK18 -- Low order 18 bits = 0x0003FFFF = 0o00000777777
- MASK19 -- Low order 19 bits = 0x0007FFFF = 0o00001777777
- MASK20 -- Low order 20 bits = 0x000FFFFF = 0o00003777777
- MASK21 -- Low order 21 bits= 0x001FFFFF = 0o00007777777
- MASK22 -- Low order 22 bits = 0x003FFFFF = 0o00017777777
- MASK23 -- Low order 23 bits = 0x007FFFFF = 0o00037777777
- MASK24 -- Low order 24 bits = 0x00FFFFFF = 0o00077777777
- MASK25 -- Low order 25 bits = 0x01FFFFFF = 0o00177777777
- MASK26 -- Low order 26 bits = 0x03FFFFFF = 0o00377777777
- MASK27 -- Low order 27 bits = 0x07FFFFFF = 0o00777777777
- MASK28 -- Low order 28 bits = 0x0FFFFFFF = 0o01777777777
- MASK29 -- Low order 29 bits = 0x1FFFFFFF = 0o03777777777
- MASK30 -- Low order 30 bits = 0x3FFFFFFF = 0o07777777777
- MASK31 -- Low order 31 bits = 0x7FFFFFFF = 0o17777777777
- MASK32 -- 32 bits = all ones = 0xFFFFFFFF = 0o37777777777
- MASK3201
-- Alternating bits: 32 bits of 0101... = 0o12525252525 = 0x55555555
- MASK3202
-- Alternating 2-bits: 32 bits of 00110011... = 0o06314631463 = 0x33333333
- MASK3204
-- Alternating 4-bits: 32 bits of 0000111100001111... = 0o01703607417 = 0x0F0F0F0F
- MASK3208
-- Alternating 8-bits: 32 bits of 0000000011111111... = 0o00077600377 = 0x00FF00FF
- MASK3210
-- Alternating bits: 32 bits of 101010... = 0o25252525252 = 0xAAAAAAAA
- MASK3220
-- Alternating 2-bits: 32 bits of 11001100... = 0o31463146314 =
0xCCCCCCCC
- MASK3240
-- Alternating 4-bits: 32 bits of 1111000011110000... =
0o36074170360 = 0xF0F0F0F0
- MASK3280
-- Alternating 8-bits: 32 bits of 1111111100000000... =
0o37700177400 = 0xFF00FF00
- MTXCOL --
"SwFlag" argument to
MtxVectOp()
signifying column swap, and dir argument to
MtxGet() and
MtxPut().
- MTXCOLVECT --
"OpFlag" argument to
MtxVectOp() and
MtxVectOp3
signifying bit-by-bit Matrix op Column Vector.
- MTXROW --
"SwFlag" argument to
MtxVectOp()
signifying row swap, and dir argument to
MtxGet() and
MtxPut().
- MTXROWVECT --
"OpFlag" argument to
MtxVectOp() and
MtxVectOp3
signifying bit-by-bit Matrix op Row Vector.
- NUCLMAGN
-- Nuclear magneton = 5.05078343×10-27 J/T
- PHI -- Golden
ratio: Φ = (1+√5 )/2 =
1.618033988749895. Note: (1/Φ) = (Φ−1)
- PHIINV --
1/Φ = 0.618033988749895.
Note: PHIINV = (1/Φ) = (Φ−1)
- PI -- π
= 3.141592653589793 = circumference/diameter for a circle
- PI43 --
(4/3)π = 4.18879020478639
- PLANCK
-- h = 6.62606957×10-34 Js = Planck's constant
- PLANCK2PI -- h-bar = 1.05457168×10-34 Js
= Planck's constant(h)/(2*π)
- RADIANS2D -- 360/(2π)
= 57.295779513082 rad/deg = Angle conversion factor: RADIANS2D * radians = degrees
- RIGHTC --
Direction argument to VectShift() for circular right shift
- RIGHTS --
Direction argument to VectShift() for right
shift, and
VectGet() for right side justification
- ROWVECTMTX --
"OpFlag" argument to
MtxVectOp() and
MtxVectOp3
signifying bit-by-bit Row Vector op Matrix.
- SETBIT --
op argument to
MtxBit(),
TnsrBit(),
VectBit().
- SQRT10 --
√10
= 3.162277660168379
- SQRT2 --
√2
= 1.414213562373095
- SQRT3 --
√3
= 1.732050807568877
- SQRT5 --
√5
= 2.236067977499790
- SQRT6 --
√6
= 2.449489742783178
- SQRT7 --
√7
= 2.645751311064591
- SQRT8 --
√8
= 2.82842712474619
- SQRTE --
√e
= 1.64872127070013
- SQRTPI --
√π
= 1.77245385090552
- THIRDPI --
π/3 = 1.0471975511965977
- WRAP --
wrap argument (allow wrapping) to
MtxGet(),
MtxPut().
- WRAPOFF --
wrap argument (do not allow wrapping) to
MtxGet(),
MtxPut().
- XTAND --
Binary operator (AND) for Vector, Matrix and Tensor functions.
- XTANDNOT --
Compound binary operator (And, Not) for
VectOp3(),
MtxOp3(),
TnsrOp3().
- XTEQ --
Comparison operator (Equal) for Vector, Matrix and Tensor functions.
- XTGE --
Comparison operator (Greater than or equal) for Vector, Matrix and Tensor functions.
- XTGT --
Comparison operator (Greater than) for Vector, Matrix and Tensor functions.
- XTIFF --
Binary operator (IFF) for Vector, Matrix and Tensor functions.
- XTIMPLIES --
Binary operator (IMPLIES) for Vector, Matrix and Tensor functions.
- XTLE --
Comparison operator (Less than or equal) for Vector, Matrix and Tensor functions.
- XTLT --
Comparison operator (Less than) for Vector, Matrix and Tensor functions.
- XTNEQ --
Comparison operator (Not equal) for Vector, Matrix and Tensor functions.
- XTNOOP --
Unary operator (No-op) for op1 argument to
VectOp3(),
MtxOp3(),
TnsrOp3().
- XTNOR --
Binary operator (NOR) for Vector, Matrix and Tensor functions.
- XTNOT --
Unary operator (NOT) for op1 argument to
VectOp3(),
MtxOp3(),
TnsrOp3().
- XTOR --
Binary operator (OR) for Vector, Matrix and Tensor functions.
- XTORNOT --
Compound binary operator (Or, Not) for
VectOp3(),
MtxOp3(),
TnsrOp3().
- XTXOR --
Binary operator (XOR) for Vector, Matrix and Tensor functions.
- XTXNOR --
Binary operator (XNOR) for Vector, Matrix and Tensor functions.
In some cases, the problem described by the input .toq file
may not fit onto the D-Wave hardware system. One option is to
try post processing, which requires
programmer intervention. ToQ also provides
a new mechanism to automatically break up the problem into pieces, then
reassemble the results for presentation back to the caller.
Use the −QP option to initiate autopartitioning.
When the programmer knows that certain asserts should be in
either the original partition (sent to the D-Wave) or the final
partition (post processed automatically in classical mode), she
may replace the assert key word with assert1:
or assert2: to force that component
of the partitioning. To enable, use
toq -QP -i xyz.toq
Although there are a great many options to do special things, the
vast majority of usage is:
Typical Usage: toq -i xyz.toq
Here is a list of all the options.
Usage: toq [-abBcCdDeEfFg] [-G fmt] [-h] [-H topic] [-i inFile]
[-n N] [-o outFile] [-O opt(s)] [-Lpq] [-Q opt] [-rRsS]
[-t satType] [-TuvxXZ] [-z varFile|configFile] [-Z]
-a Syntax/semantics overview (no execution)
-b List the bool- and constraint-eligible functions
(no execution)
-B List the bool- and constraint-eligible functions
w/ descriptions (no execution)
-c List the constants (no execution)
-C List the constants w/ values, descrs (no execution)
-d List the directives (no execution)
-D List the directives w/ descrs (no execution)
-e List the error handling attributes (no execution)
-E Do not show constraint variable declaration error hints
-f List all the functions (no execution)
-F List all the functions w/ descriptions (no execution)
-g List the generated boolVariables and assertStmts
-G Group result display format for .qubo input files.
Followed by a string (e.g., toq -i zz.qubo -G 3,ABCDEFGH
-or- toq -i ww.qubo -G 4). Defines various output display
formats (enter "toq -QG" for details and examples)
-h Help - print this message (no execution)
-H Help topic - print help message about "topic" (no exec)
-i The input file name (default is stdin)
Typical case: toq -i xyz.toq
Special Sat(DIMACS) case: toq -i abc.cnf
Special Qubo case: toq -i def.qubo
Special Adjacency case: toq -i ghi.adj
-L List the input program (after scan)
-n Number of results requested (overrides env, startup files)
Default: 500, Range: (1-2,000) is silently enforced
-o The output file name (default is stdout)
-O Options(s)Print: Show detailed help for one or more options.
E.g., "toq -Ox" describes the -x option (no execution)
-p Print all variable values at completion
-q Use the direct qubo method to solve problem (via qbsolv).
For input = xyz.toq, 2 files will be generated:
xyzTOQ.qubo and xyzTOQ.qbout
-Q Special options (defined by next argument)
-Q afile - "file" is Quantum Apprentice file, nolist
-Q Afile - "file" is Quantum Apprentice file, list
-Q c - Collect all (cnf) single var msgs --> 1 warning
(Default behavior is an error msg)
-Q C - Disable all (cnf) single var msgs
(This option is not recommended)
-Q Dn - Debug level (n)
-Q f - Don't show Post/Partition first pass cases
-Q F - Enable the Clade (assert/family) Report
-Q G - Show details/examples for -G option (no exec)
-Q I - Use the ToQ Internal Solver
-Q M - Disable ToQ bool/assert msg (not recommended)
-Q P - Enable Partitioning
-Q Q - Use the Quantum Simulator Solver
-Q r - Seed (integer in 1-100,000) to force
reproducible embedding (e.g., -Qr12461)
-Q R - Regression testing mode
-Q Se - Synopsis - Embedded ToQ (no execution)
-Q Sm - Synopsis - Programming Model (no execution)
-Q Sp - Synopsis - Partitioning (no execution)
-Q Sq - Synopsis - Full QUBO processing (no execution)
-Q V - View generated vectors
-Q W - Disable Warning messages (not recommended)
-Q x - Enable extended constraint variable report
-Q Y - Disable FYI messages
-R Run the FrontEnd only - no solution
-s List the Satisfiability functions (no execution)
-S List the Satisfiability functions w/ descriptions
(no execution)
-t Type of satisfiability clauses (for "cnf" only,
(not "cnf+")). Valid strings for "satType" are in
{ 1in3, 2in3, 2in4, 2in5, 3in4, 3in5, 4in5, nae, nae3,
nae4, nae5, naen, sat2, sat3, sat4, sat5, xor2, xor3 }
Simple example: toq -i xyz.cnf -t nae3
-T Show detailed timing data
-u User manual (list options combined - no execution)
-v Print Version information (no execution)
-x Enable the ConstraintVar/AssertId Xref
-X Suppress all output but errors, warnings, Summary
(Not for new (programs, programmers))
-z AuxFileName - read/process this file. The auxiliary
files are VariablesIn and Configuration (see -Z)
-Z Format (layout) of the VariablesIn, Configuration,
and .cnf files (no execution)
-1 Stop at 1st error detected (default: OFF)
-a Syntax/semantics overview' -o Output file name
-b List bool/constraint funcs' -O Option(s)Print'
-B List bool/constr funcs,descr' -p Print var values at end
-c List constants' -q Use Qbsolv to solve problem
-C List constants w/ descr' -Q Special options
-d List directives' -R Run the FrontEnd only
-D List directives w/ descr' -s List Sat functions'
-e List error handling attrs' -S List Sat funcs w/ descr'
-E Don't show constr hints -t Type Sat clauses'
-f List functions' -T Show detailed timing
-F List functions w/ descr' -u List user manual'
-g List gen'd bools/asserts -v Version info'
-G Group result display format' -V List vector funcs, descr'
-h Help (show cmdline options)' -x Enable bool/assert Xref
-H Help topic (help: "topic")' -X Suppress non-error,-warnings
-i Input file name -z AuxFileNm (vals,config)
-L List input program -Z Format (layout) of files'
-n Number of results -1 Stop at 1st error
' no execution
You may read variable values into your program from an external
file – see the Reading External Variables
chapter. During the execution of the program, using any of
the following directives will allow you to write information to the
output file. A future version will support writing information
out to a file.
- dbprintf: print the line number and name/value of each item
on the the list
- dbprintb: same as "dbprintf:" except list display items
in decimal, hex, octal, and binary
- dbprintv: list vector display items in hex and binary
- dbprintx: similar to "dbprintb:" (list
display items (including vectors) in hex and binary)
- print: var1 [,var2...] prints the current
value of the variables in the list with the current line number
- printvars: prints the current value of all the variables
with the current line number
- printf: print the comma-separated items listed
e.g., printf: "Alpha = ", alpha, "Beta = ", beta, "\n"
- printfn: same as printf: with an automatic "\n" tacked on
Click here for a list of the input and output
files for ToQ.
Qbsolv is a powerful program in the qOp toolset. It resolves QUBO
problems, even when they are larger than the target D-Wave system.
It automatically partitions the problem into D-Wave-size chunks,
runs them, and passes the results back to ToQ for
presentation back to the user.
ToQ uses Qbsolv via the −q
commandline argument (as below):
toq -q -i xyz.toq
When ToQ is called with the -q option, a special file "xyzTOQ.qubo" is
created (its format is described below), and its contents are processed
by the Qbsolv utility. A new output file containing
the results (in an internal format) are saved in a new file named
"xyzTOQ.qbout" – ToQ processes this file and
prints the results in a more reader-friendly manner. Both new
files are saved and available for later reuse. The .qbout file is
ASCII and contains the results as a bit-string.
.qubo File Format – A .qubo file contains data which
describes an unconstrained quadratic binary optimization problem.
It is an ASCII file comprised of four types of lines:
- Comments - defined by a "c" in column 1. They may appear
anywhere in the file, and are otherwise ignored.
- One program line, which starts with "p" in the first column.
The program line must be the first non-comment line in the file.
The program line has six required fields (separated by space(s)),
as in this example:
p qubo target maxNodes nNodes nCouplers
where:
- p – the problem line sentinel
- qubo – identifies the file type
- target – a string which identifies the topology of
the problem and the specific problem type. For an unconstrained
problem, target may be "0" or "unconstrained." For constrained
problems, valid strings could include "chimera128" or "chimera512"
(among others).
- maxNodes – number of nodes in the topology.
- nNodes – number of nodes in the problem
(nNodes ≤ maxNodes). Each node has a unique number
and must take a value in the the range {0 −
(maxNodes-1)}. A duplicate node number is an
error. The node numbers need not be in order, and they need
not be contiguous.
- nCouplers – number of couplers in the
problem. Each coupler is a unique connection between two
different nodes. The maximum number of couplers is
(nNodes)2. A duplicate coupler is an error.
- nNodes clauses. Each clause is made up of three
numbers. The numbers are separated by one or more blanks.
The first two numbers must be integers and are the number for this
node (repeated). The node number must be in {0 −
(maxNodes-1)}. The third value is the weight associated
with the node, may be an integer or float, and can take on any positive
or negative value, or zero.
- nCouplers clauses. Each clause is made up of three
numbers (i, j, str). The numbers are separated by one or more blanks.
The first two numbers must be different integers and are the node
numbers for this coupler. The two values (i and j) must have (i <
j). Each number must be one of the nNodes valid node
numbers (and thus in {0 − (maxNodes-1)}).
The third value (str) is
the strength associated with the coupler, may be an integer or float,
and can take on any positive or negative value, but not zero.
Every node must connect with at least one other node (thus must have at
least one coupler connected to it).
Here is a simple QUBO file example for a problem with 4 nodes and
6 couplers. This example is provided to illustrate the elements
of a QUBO benchmark file, not to represent a real problem.
c
c This is a sample .qubo file
c with 4 nodes and 6 couplers
c
p qubo 0 4 4 6
c ------------------
0 0 3.4
1 1 4.5
2 2 2.1
3 3 -2.4
c ------------------
0 1 2.2
0 2 3.4
1 2 4.5
0 3 -2
1 3 4.5678
2 3 -3.22
When running ToQ in LibraryMode, users can make calls to
other parts of the (calling) program.
Some special preliminary work is necessary. Each function
to be called must be declared via a prototype: directive (see
format below), and the user must supply a version of
ToQDispatch() in
the calling program to help complete the external reference.
See below for a sample ToQDispatch() function.
All prototype: directives must appear before the first executable
statement or be part of an input variable file (-z file).
Prototype external functions are only available during LibraryMode, not
when running ToQ as a stand-alone program. Here is
the format of a prototype: directive -
prototype: id, pType, FuncName(type1,type2,...)
where id is a unique integer (in 1-32)
pType is the return type of external function FuncName()
(and must be either "int" or "real")
FuncName is the external function to call, and
type1,type2,... are its argument types (max=8), which
are scalar ("int" or "real") and call-by-value only
Upon return, you will have access only to the return value.
Here is a skeleton of a ToQDispatch() function.
The arguments in each prototype: must agree in type and number
with its corresponding function in ToQDispatch().
The IDs supplied in the prototype:
directive must correspond to the case labels in ToQDispatch().
Note that the name ToQDispatch is case-sensitive. If you have
these three prototype statements in your .toq file,
prototype: 1, real, FtRate(int,real,int)
prototype: 5, int, Jussive(int)
prototype: 2, real, Omega(real,real)
and the calling program contains the above functions,
and your .toq file contains something like:
int: numb, mode = 4, intensity = 17
real: rate, freq = 0.37
# ~~~
numb = Jussive(intensity)
rate = FtRate(mode,freq,intensity)
Here is a snippet of the calling program with the corresponding
required ToQDispatch() function. Note that the ToQDispatch()
function must agree exactly with the form below (i.e., the id,
3 integer arguments and 3 double arguments). The calling
program supplies the FtRate(), Omega() and Jussive() functions.
double ToQDispatch( int id, int n1, int n2, int n3,
double x1, double x2, double x3);
double FtRate( int a, double x, int b);
double Omega( double x, double y);
int Jussive( int a);
. . .
double ToQDispatch(int id, int n1, int n2, int n3,
double x1, double x2, double x3)
{
double retValue;
// ~~~
switch (id) {
case 1: retValue = FtRate(n1,x1,n2);
break;
case 2: retValue = Omega(x1,x2);
break;
case 5: retValue = Jussive(n1);
break;
default: printf("\nError - prototype %d not found\n", id);
retValue = -999.999;
break;
}
return(retValue);
}
Note that the ToQ runtime system manages the type
of the ToQDispatch() return value. In the snippet
of the .toq program above, the return value for Jussive() is
automatically converted to an integer.
(Early) Draft
This section is not meant for serial review. Rather it is
a repository (or miscellaneous collection) of various topics which one
would click in the above text. Some of the material in this
section is very detailed. After reading the particular topic,
clicking the [Back] button will return you to the previous spot.
assert: -
An executable statement which operates on constraint variables
(bool, bmask, mbool). Assert statements are used
to represent the components of an optimization problem.
An optimization problem is resolved when all the assert
statements in the execution path evaluate to TRUE. Essentially,
ToQ acts as if all the constraint variables took on all
their valid values, and selects only those sets for which all the
assert statements evaluate to TRUE. There are two important
rules with assert statements:
Here are some samples:
bool: @a, @b, @c
mbool: 1,5, @p1, @p2
mbool: 3,12,3, @p3
assert: Or(@a, Xor(@b, @c))
assert: Nand(@a, @c)
assert: ((@p1 + @p2 + @p3 - @b) == 13)
assert: ((2*@p1) >= (@p2+@a+@b))
In general, long assert statements (14 or more bools) should be
avoided. See also quant: which is an
advanced feature that adds the potential to make assert statements more
powerful and easier to use.
There are several special-purpose flavors of assert.
assert1
-- An "assert1:" statement is treated the
same as an "assert:" statement except when autopartitioning (-QP
option) is selected. "assert1:" forces the assert to be in the first
partition.
assert2
-- An "assert2:" statement is treated the same as an
"assert:" statement except when autopartitioning (-QP option) is
selected. "assert2:" forces the assert to be in the second
partition.
assertp
-- An executable statement which may be used only after the
"post:" directive. It is analogous to the regular assert:
statement, except that when bool: variables are accessed, only the
actual value set which has resulted from the regular asserts are used
(as opposed to the full set of all possible bool: value
combinations). In the code snippet below, the user want to assure
that the bool: variables (@a1,@a2,...,@a7) are not identical to
(@b1,@b2,...,@b7). This computation could be performed with
regular assert: statements, but might require more complex embedding
layouts. This example uses the
Amalgam() function, which provides a convenient
way to compare two set of booleans.
bool: @a1, @a2, @a3, @a4, @a5, @a6, @a7
bool: @b1, @b2, @b3, @b4, @b5, @b6, @b7
intp: aProfile, bProfile
# ... lots of assert: statements, etc
post:
aProfile = amalgam(@a1,@a2,@a3,@a4,@a5,@a6,@a7)
bProfile = amalgam(@b1,@b2,@b3,@b4,@b5,@b6,@b7
assertp: (aProfile != bProfile)
end
An optimization problem which employs "post:" processing is
resolved when all the
assert and
assertp statements in the
execution path evaluate to TRUE.
lineareq --
is a special-case form of an assert statement.
When a ToQ program contains a LinearEq: statement, all the
executables must be LinearEq: statements. Here is the
general form, which must be followed exactly
C1*@a + C2*@b + C3*@c + ... == X
where @a, @b, ... must be different mbool variables, and the
Ci must be non-zero integers. These statements comprise a
certain kind of problem (often described as "N equations
in M unknowns," with M > N). This form instructs ToQ to
attack this problem using a "Direct-to-QUBO" algorithm
instead of the more general (but more complex) algorithm.
This attack is often able to resolve larger problems than
the standard ToQ algorithm can manage. It will find a
single solution (if there is one) - even though there may
be multiple solutions. Here is a sample - two equations
with four unknowns:
mbool: 13,20, @a, @b
mbool: 35,50, @d, @f
# ~~~
lineareq: 5*@a + 6*@b - 2*@d - @f == 40
lineareq: @a + 2*@b - @d + 2*@f == 71
# ~~~
end:
And here are four solution sets to this problem:
@a: 15 13 16 19
@b: 14 17 15 13
@d: 42 46 47 48
@f: 35 35 36 37
maximize
-- An executable statement which may be used only after the "post:"
directive. It is analogous to the regular assert: statement,
except that when bool: variables are accessed, only the actual value
sets which have resulted from the regular asserts are used.
(Note that if a post: directive is present, the post: section follows
it). Only one maximize or minimize statement may appear in a
ToQ program. It chooses the maximum value of the previously evaluated
asserts (or assertps) as the final answer of the problem.
minimize --
An executable statement which may be used only after the "post:"
directive. It is analogous to the regular assert: statement,
except that when bool: variables are accessed, only the actual value
sets which have resulted from the regular asserts are used.
(Note that if a post: directive is present, the post: section follows
it). Only one maximize or minimize statement may appear in a
ToQ program. It chooses the minimum value of the
previously evaluated asserts (or assertps) as the final answer of the
problem.
subjto: --
(subject to) is a special-case assert statement for processing
DTQ (Direct-to-QUBO) maximize/minimize problems (for example, the
"set-partitioning" problem). The rules are:
- Only bool and mbool constraint variables are allowed
- Only one maximize or minimize directive is allowed, it must
be the first executable statement, and it must be a linear
combination of the constraint variables
- The subjto: statements must contain only a simple linear
combination of the constraint variables, followed by
"== const"
Here is a simple example:
bool: @b1,@b2,@b3,@b4,@b5,@b6,@b7,@b8
# ~~~
minimize: (@b1+9*@b2+7*@b3+2*@b4+8*@b5+20*@b6+20*@b7+20*@b8)
subjto: @b2+@b3+@b4+@b6 == 1
subjto: @b1+@b3+@b5+@b7 == 1
subjto: @b1+@b2+@b5+@b8 == 1
# ~~~
end:
ToQ provides three data types for acting on arrays of
bits as atomic operations: vectors (1-D), matrices (2-D), and tensors
(3-D). For example, if Mtx1, Mtx2 and Mtx3 are
conforming (e.g., 80x32)
matrices, setting Mtx3 to (Mtx1 XOR Mtx2) can be done with a single
function call. The data is packed, individual bits can be
accessed, the full complement of logical operations are available, I/O
is available, and data can be operated on and moved between bit arrays
(i.e., one can move data and compute with vectors,matrices,tensors).
The data types are vect:, mtx:, tnsr:. Data items may be
initialized on the declaration statement (all elements must
be initialized before use). Enter:
toq -H vect
toq -H mtx
toq -H tnsr
for details, functions, et cetera. Here is some sample code:
# --- bitex.toq --- Regression: bit array sample
vect: 128, v1, v3, v2 = mask3240, mask3210, 0x2468FEDC, mask32
vect: 96, v4
# Note - the > means fill out the array
mtx: 4,128, m1, m2 = 0, mask32, >mask3220
mtx: 2,64, m3, m4
tnsr: 2,4,8, t1, t2 = 0x1234CDEF, 0xFFAA0022
int: bitsV1, bitsV2, bitsV3, bitsM4, bitsT1, bitsT2
# ~~~
VectInit(v1,0x13579246)
VectOp(v3,v1,XTAND,v2)
MtxVect(m3,v2,VECTTOMTX)
MtxReverse(m4,m3)
TnsrNot(t1,t2)
TnsrVect(t1,v4,TNSRTOVECT,FILLONE)
dbprintx: v1, v2, v3, v4, m2, m3, m4, t2, t1
bitsV1 = VectBitCount(v1,0)
bitsV2 = VectBitCount(v2,0)
bitsV3 = VectBitCount(v3,0)
bitsM4 = MtxBitCount(m4,0)
bitsT1 = TnsrBitCount(t1)
bitsT2 = TnsrBitCount(t2)
dbprintf: bitsV1, bitsV2, bitsV3, bitsM4, bitsT1, bitsT2
# ~~~
end:
And here are the results:
DB(line 15)
(vect: 128) v1 = 0x13579246, (3 repeats)
(vect: 128) v2 = 0xF0F0F0F0, AAAAAAAA, 2468FEDC, FFFFFFFF
(vect: 128) v3 = 0x10509040, 02028202, 00409244, 13579246
(vect: 96) v4 = 0xEDCB3210, 0055FFDD, FFFFFFFF
m2 (mtx: 4,128) - hex
Row 0) = 0x00000000, FFFFFFFF, CCCCCCCC, (1 repeat)
Row 1) = 0xCCCCCCCC, (3 repeats)
Row 2) = ... -<3 128-bit duplicate rows (1-3)>-
m3 (mtx: 2,64) - hex
Row 0) = 0xF0F0F0F0, AAAAAAAA
Row 1) = 0x2468FEDC, FFFFFFFF
m4 (mtx: 2,64) - hex
Row 0) = 0xFFFFFFFF, 3B7F1624
Row 1) = 0x55555555, 0F0F0F0F
t2 (tnsr: 2,4,8) - hex
(0,0) = 0x12
(0,1) = 0x34
(0,2) = 0xCD
(0,3) = 0xEF
(1,0) = 0xFF
(1,1) = 0xAA
(1,2) = 0x00
(1,3) = 0x22
t1 (tnsr: 2,4,8) - hex
(0,0) = 0xED
(0,1) = 0xCB
(0,2) = 0x32
(0,3) = 0x10
(1,0) = 0x00
(1,1) = 0x55
(1,2) = 0xFF
(1,3) = 0xDD
DB(line 22)
bitsV1 = 56
bitsV2 = 81
bitsV3 = 31
bitsM4 = 81
bitsT1 = 33
bitsT2 = 31
bmask: is a constraint variable type: multi-bit
logical entities for use in assert statements. Format is:
bmask: J, K, @m1, @m2, ...
where J and K are integers, (0 < J < K ≤ 8), and each of
the one or more variables in the list is a K-bit word which
has exactly J 1-bits.
Here is a table of values for a bmask: J, K, @var1,
@var2 declaration:
J,K Values
----- ----------------
1,2 1,2
1,3 1,2,4
1,4 1,2,4,8
1,5 1,2,4,8,16
1,6 1,2,4,8,16,32
1,7 1,2,4,8,16,32,64
1,8 1,2,4,8,16,32,64,128
2,3 3,5,6
2,4 3,5,6,9,10,12
2,5 3,5,6,9,10,12,17,18,20,24
2,6 3,5,6,9,10,12,17,18,20,24,33,34,36,40,48
2,7 3,5,6,9,10,12,17,18,20,24,33,34,36,40,48,65,66,68,72,80,96
2,8 3,5,6,9,10,12,17,18,20,24,33,34,36,40,48,65,66,68,72,80,96,
129,130,132,136,144,160
3,4 7,11,13,14
3,5 7,11,13,14,19,21,22,25,26,28
3,6 7,11,13,14,19,21,22,25,26,28,35,37,38,41,42,44,49,50,52,56
3,7 7,11,13,14,19,21,22,25,26,28,35,37,38,41,42,44,49,50,52,56,
67,69,70,73,74,76,81,82,84,88,97,98,100,104,112
3,8 7,11,13,14,19,21,22,25,26,28,35,37,38,41,42,44,49,50,52,56,
67,69,70,73,74,76,81,82,84,88,97,98,100,104,112,131,133,134,
137,138,140,145,146,148,152,161,162,164,168,176,193,194,196,
200,208,224
4,5 15,23,27,29,30
4,6 15,23,27,29,30,39,43,45,46,51,53,54,57,58,60
4,7 15,23,27,29,30,39,43,45,46,51,53,54,57,58,60,71,75,77,78,83,
85,86,89,90,92,99,101,102,105,106,108,113,114,116,120
4,8 15,23,27,29,30,39,43,45,46,51,53,54,57,58,60,71,75,77,78,83,
5,86,89,90,92,99,101,102,105,106,108,113,114,116,120,135,139,
41,142,147,149,150,153,154,156,163,165,166,169,170,172,177,
78,180,184,195,197,198,201,202,204,209,210,212,216,225,226,
28,232,240
5,6 31,47,55,59,61,62
5,7 31,47,55,59,61,62,79,87,91,93,94,103,107,109,110,115,117,
118,121,122,124
5,8 31,47,55,59,61,62,79,87,91,93,94,103,107,109,110,115,117,
18,121,122,124,143,151,155,157,158,167,171,173,174,179,181,
82,185,186,188,199,203,205,206,211,213,214,217,218,220,227,
29,230,233,234,236,241,242,244,248
6,7 63,95,111,119,123,125,126
6,8 63,95,111,119,123,125,126,159,175,183,187,189,190,207,215,
219,221,222,231,235,237,238,243,245,246,249,250,252
7,8 127,191,223,239,247,251,253,254
A Clade is a group of related assert statements. Related means
that each member of the group has at least one boolean variable
in common with another member of the clade. A program with
multiple clades means that each clade (family of asserts) shares
no booleans with the other clades.
Often, a ToQ
program with mulitple clades is actually unintentional.
Here is a simple example:
# --- clade2.toq --- Regression Test
#
# 2 Clades (lines 8,9,11 and lines 10,12)
#
bool: @a,@b,@c,@d,@e,@f,@g
mbool: 1,4, @x,@y,@z
# ~~~
assert: Or(@g,And(@a,@b))
assert: @b+@c+@d+@e+@f == 3
assert: @x+@y <= 6
assert: And(@g,@e)
assert: @x-@z < 2
# ~~~
end:
If the Clade Report is off, ToQ will issue a warning
and request that you rerun with the -QF option, which would lead
to this message:
ToQ: ::::> Warning
--> Disconnected asserts. The 5 input assert statements
fall into 2 clades which do not overlap. See the
Clade Report below -
Clade Report
================
Clade 1
---------
1 (line 8): assert: Or(@g,And(@a,@b))
2 (line 9): assert: @b+@c+@d+@e+@f == 3
3 (line 11): assert: And(@g,@e)
Clade 2
---------
1 (line 10): assert: @x+@y <= 6
2 (line 12): assert: @x-@z < 2
CNF (Conjunctive Normal Form) is the DIMACS file format for
satisfiability problems. ToQ accepts ".cnf" files
as input for satisfiability problems. Here is the format of this file
type:
- The file is ASCII
- Comments have a "c" in the first character, and the
line is otherwise ignored
- After zero or more comments, the ProblemLine appears:
The format is "p cnf nVars   nClauses" where:
- cnf is a required token
- nVars is the number of unique variables.
The variables are used in the clauses. The variables are
designated by positive integers, typically (1−nVars)
- nClauses is the number of clauses
- The rest of the file is made up of the clauses (one
clause per line)
- Each clause is comprised of the variables (separated by
a blank and terminated by a 0)
- A minus sign ("−") designates the logical negation of
the variable in a clause
A problem solution occurs when a set of variable values (each is either
TRUE or FALSE) can be found that makes each clause TRUE. Each clause
is TRUE when at least one term in the clause is TRUE. That is, the
terms in each clause are ORed together, and the clauses are ANDed.
Here is a simple example:
c Sample file (5 variables, 4 clauses)
p cnf 5 4
1 2 -3 0
4 1 3 0
5 -4 2 0
3 4 5 0
When a .cnf file is used as input (-i option), ToQ
internally takes care of declarations, bool: variable naming, etc.
and returns the solution as a set of values for the
nVarsintegers in the input file clauses.
There are two mechanisms for extending the representation of
satisfiability problems:
- Use "cnf+" on the ProblemLine rather than "cnf" --
this directs ToQ to treat each line separately as
a satisfiability clause. Click
Cnf+ for details.
- Use the "-t satType" commandline option (works only
with "cnf" on the ProblemLine). "SatType" tells
ToQ how to interpret the .cnf file lines.
By default, each line is treated as a simple Sat() function,
but when "satType" is one of the strings below,
each input line is treated as the corresponding
function from this list:
String Function String Function
------ -------- ------ --------
1in2 Sat12() nae3 NAESat3()
1in3 Sat13() nae4 NAESat4()
1in4 Sat14() nae5 NAESat5()
1in5 Sat15() naen NAESatN()
2in3 Sat23() sat2 Sat2()
2in4 Sat24() sat3 Sat3()
2in5 Sat25() sat4 Sat4()
3in4 Sat34() sat5 Sat5()
3in5 Sat35() satn SatN()
4in5 Sat45() xor2 Xor2Sat()
nae NAESat() xor3 Xor3Sat()
Using the "-t satType" option may be particularly helpful (along
with the "satisfiability:" directive) for error-checking.
Click here for a list of all the satisfiability
functions. Click here for a
description of the satisfiability: directive.
CNF+ (see also CNF
above). Using "cnf+" on the ProblemLine rather than "cnf"
directs ToQ to treat each line separately as a
satisfiability clause. The last item on each line
is a zero. The following examples illustrate this
cardinality capability:
1 3 43 47 >= 2 0
31 32 86 0
12 14 16 18 20 == 3 0
2 3 4 5 0
21 23 31 33 41 43 0
which translate internally to:
assert: ((@01 + @03 + @43 + @47) >= 2)
assert: sat3(@31,@32,@86)
assert: ((@12 + @14 + @16 + @18 + @20) == 3)
assert: sat4(@02,@03,@04,@05)
assert: ((@21+@23+@31+@33+@41+@43) > 0)
only these compare operators are allowed with cnf+:
> =
>= == "==" and "=" are treated the same
< !=
<=
Click here for a list of all the satisfiability
functions. Click here for a
description of the satisfiability: directive.
A ToQ program consists of a collection of
assert
statements which operate on Constraint Variables.
ToQ works by finding sets of values for the Constraint
Variables for which all the asserts are TRUE. All Constraint
Variable names start with the @ character. There are two
types of Constraint Variables - Booleans (bool:) and Extended Booleans
(mbool:, bmask:). Boolean variables take on the values {0,1}, and
Extended Booleans are really combinations of Booleans -
- mbool: N,M,[i,] @var1, @var2, ...
- The variables in the list take on the values N to M
(optionally incremented by i), with (0 ≤ N
< M ≤ 65,535)
- bmask: J,K, @var7, @var8, ....
- The variables in the list take on all K-bit values which
have exactly J ones, with (0 < J < K ≤ 8).
Click here for a list of values for
bmask variables.
Constraint Variables are set by the run-time system and may not be
read or written by the ToQ program.
Click here for more details about variable
types.
The lines in a ToQ program file (e.g., xyz.toq) are
delimited by the end-of-line. Although the maximum line length is
large, it is often convenient to break up lines for easier
reading. For ToQ program files only, long lines may
be partitioned by using the Continuation Character ('_').
Here are the simple rules:
- The last character on a line to be continued must be '_'.
- The next line must have '_' as its first character.
Note that whitespace may not precede the '_'.
- Comment lines may not be nested in continued lines.
- A "continued-line" may have as many member lines as needed
provided the total line length is not exceeded.
- A multi-line "continued line" still has the same maximum allowable
length as any other line.
- The Continuation Character ('_') may not appear elsewhere
in a ToQ program (except in comments).
Here is a simple example:
Before: minimize: (@ab*ab+@ac*ac+@ad*ad+@ae*ae + @bc*bc+@bd*bd+@be*be + @cd*cd+@ce*ce + @de*de)
After: minimize: (@ab*ab + @ac*ac + @ad*ad + @ae*ae + _
_ @bc*bc + @bd*bd + @be*be + @cd*cd + _
_ @ce*ce + @de*de)
ToQ can generate a ConstraintVariable/AssertId cross
reference map after the last executable statement (Off by
default). To enable, use the "-x" option or the "xref:"
directive. Here is a simple sample:
1 # --- satprob.toq --- Regr #61
2 #
3 # 10 variables
4 # 15 assertions
5 #
6 bool: @A,@B,@C,@D,@E,@F,@G,@H,@I,@J
7 #~~~
8 assert: @B + @D + @A > 0
9 assert: @J + @I + @F > 0
10 assert: not(@J) + not(@A) + @C > 0
11 assert: not(@I) + @D + @C > 0
12 assert: @B + not(@F) + @C > 0
13 assert: @C + not(@H) + @J > 0
14 assert: @C + @A + @E > 0
15 assert: @F + not(@J) + @B > 0
16 assert: not(@B) + @G + not(@I) > 0
17 assert: @C + @H + not(@B) > 0
18 assert: not(@I) + @A + not(@D) > 0
19 assert: not(@E) + @D + not(@F) > 0
20 assert: not(@E) + not(@D) + not(@F) > 0
21 assert: not(@G) + not(@E) + @J > 0
22 assert: not(@J) + @H + not(@A) > 0
23 #~~~
24 end:
|
|
|
15 Asserts
==============
Id Line # Text
-- ---- --- ----------------
1) 1 8 3 @B + @D + @A > 0
2) 2 9 3 @J + @I + @F > 0
3) 3 10 3 not(@J) + not(@A) + @C > 0
4) 4 11 3 not(@I) + @D + @C > 0
5) 5 12 3 @B + not(@F) + @C > 0
6) 6 13 3 @C + not(@H) + @J > 0
7) 7 14 3 @C + @A + @E > 0
8) 8 15 3 @F + not(@J) + @B > 0
9) 9 16 3 not(@B) + @G + not(@I) > 0
10) A 17 3 @C + @H + not(@B) > 0
11) B 18 3 not(@I) + @A + not(@D) > 0
12) C 19 3 not(@E) + @D + not(@F) > 0
13) D 20 3 not(@E) + not(@D) + not(@F) > 0
14) E 21 3 not(@G) + not(@E) + @J > 0
15) F 22 3 not(@J) + @H + not(@A) > 0
Constraint/AssertId Xref
============================
Nm\Id 1 2 3 4 5 6 7 8 9 A B C D E F #
----------------------------------------------
1) @A * * * * * 5
2) @B * * * * * 5
3) @C * * * * * * 6^
---------
4) @D * * * * * 5
5) @E * * * * 4
6) @F * * * * * 5
---------
7) @G * * 2_
8) @H * * * 3
9) @I * * * * 4
---------
10) @J * * * * * * 6^
----------------------------------------------
#v 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3
----------------------------------------------
Id 1 2 3 4 5 6 7 8 9 A B C D E F
----------------------------------------------
Asserts/Constraint: min = 2(1), max = 6(2), avg = 4.50
|
|
In some cases, no combination of boolean variable values will have an
effect on the evaluation of an assert statement. When the assert
will always be FALSE, the problem has no solution; when it will always
be TRUE, the assert does not contribute to the solution. Here are
two simple examples:
bool: @a, @b
assert: ((@a+@b) == 3) # always FALSE
assert: ((@a+@b) < 7) # always TRUE
Both these cases are error conditions.
- Boolean Variables (BoolVars)
- Constraint variables which implement booleans (data type
bool). They
take on only the values {0,1} representing {False,True} or
{Out,In} etc. BoolVars are not available to the
programmer for reading and writing. Rather they are set
by the system and upon program completion, they contain
the solutions. All BoolVar names start with @.
Boolean variables may be used only in
assert statements.
- Constraint Variables (ConstrVars)
- Variables of type
bool, mbool, and
bmask.
These variables are not available to the programmer for
reading and writing. Rather they are set by the system
and upon program completion, they contain the solutions.
All ConstrVar names start with @.
Constraint variables may be used only in
assert statements.
- Extended Boolean Variables (ExtBoolVars)
- Variables of type
mbool, and bmask. These
variables provide a programmer shortcut, and they represent
combinations of bool variables. All
ExtBoolVar names start with @.
Extended boolean variables may be used only in
assert statements.
- Satisfiability Problems (SatProbs)
- A satisfiability problem is a collection of similar
clauses. Each clause is composed of a group of boolean
variables. A clause is TRUE if at least one of the
boolean variables is TRUE (i.e., all the booleans are ORed
together). A problem is satisfied if
there are one or more sets of the booleans for which all the
clauses are TRUE (i.e., all the clauses are ANDed together).
Click here for
a list of the satisfiability functions. Click
here for a more detailed discussion
of CNF problems (including cnf+ clauses).
ToQ is part of the qOp package of
prototype quantum tools. dw (another qOp tool)
provides a variety of services, including setting up an environment on
your system to make it easier to use the other tools. The
recommended way to set up your environment for ToQ is via
dw. Beyond meeting ToQ's needs,
dw performs a variety of other actions, including:
- Provides a general purpose interface for interacting
with the D-Wave System
- Manages connections, solvers and workspaces
- Displays geometry data
- Builds and executes quantum machine instructions (QMIs)
- Embeds qubos to create parameterized quantum machine
instructions (PQMIs)
- Binds and validates PQMIs
Many dw subcommands set and display environment variables which
are used to manage access to the D-Wave System.
ToQ finds the sets of values of all the Constraint
Variables for which all the program's assert statements are TRUE.
It builds an internal data structure of the relationships between the
Constraint Variables and the asserts,
then transforms them into a QUBO
format. A QUBO is like an upper triangular matrix with all the
booleans represented on the diagonal, and all the other terms represent
the relationships between the nodes. Embedding is the
transformation which maps this QUBO onto the target D-Wave hardware,
which does not have complete connectivity, and may have some inactive
nodes. The D-Wave hardware uses a "chimera" interconnect, and it
utilizes chaining (mapping multiple physical nodes to represent a
single logical node) to map the original QUBO onto the hardware.
In general, this is an NP-hard problem. The more {asserts,
booleans, booleans/assert}, the more difficult the embedding
becomes. The embedding algorithm depends on a random number
generator, so each run may produce a different embedding. You can
force reproducibility in the embedder by repeatedly using the "-Qr123"
flag, where the "123" represents an integer in [1-100,000]. For
details, click reproducibility.
ToQ is part of the qOp package of quantum tools.
"dw" (another qOp tool) provides a variety of services, including
setting up an environment on your system to make it easier to use the
other tools. The recommended way to set up your environment for
ToQ is via "dw," but of course other standard methods
are also available. ToQ searches first in your
environment for some key parameters. Values in a .toqrc file in
your local working directory will override environment values.
Values in a configuration file (use the -z option) will override
.toqrc values. Some parameters may be entered via the
commandline. Enter "toq -H dw" or "toq -H qOp" or "toq -H toqrc"
for more details.
ToQ manages three levels of error conditions:
- Warnings - messages are issued and execution continues
- Syntax/Semantic Errors - messages are issued, and an error-scan
of the input continues, but execution is terminated
- Run-time Errors - a message is issued, and an error-scan of the
input may continue, but execution is terminated. A dump
of the current values of all variables at the point of
failure is generated.
It is important to note that when a (non-Warning) error condition is
encountered, actual execution is stopped, and thus further
error-checking may be compromised. When reviewing output, one
should always address the first error first, since that error may be
masking or inducing errors further down. You may use the "-1"
commandline option to force ToQ to stop at the first error.
In all cases, ToQ
returns the status to the calling program. When no errors are
detected, ToQ returns the optimal solution to the input problem.
A ToQ input file with an .adj suffix
(e.g., xyz.adj) describes an adjacency problem (frequently
referred to as a special case of graph labeling known as "graph
coloring"). Graph coloring algorithms are used in a variety of
applications, including a wide range of scheduling and pattern
matching problems. Examples include resource allocation under
constraints, molecular similarity analyses, image processing,
compiler register allocation, regular expression operations,
natural language recognition, ...
Map coloring is a well-known example of graph coloring,
and the rest of this description uses map coloring terminology
(e.g., colors for properties, areas or entities for nodes, and
borders or neighbors for edges). ToQ can manage
arbitrarily large arrays of adjacency information (utilizing the
Qbsolv
program).
Two output files are generated by "toq -i xyz.adj" - the .qubo
file and the .qbout file (xyzADJ.qubo, xyzADJ.qbout). ToQ reads the
.qbout file and presents the results back to the user. The input
file is recognized via its ".adj" suffix. It has three line types
(Option, Name, Adjacency), which must appear in order. Input data
is case-insensitive, however input case is used for output
presentation. The '#' character initiates a comment, which runs to
the end-of-line, can appear anywhere, and is otherwise ignored.
Fields are separated by one or more (blanks,commas,tabs). Lines
are terminated by the end-of-line.
The Option line must be the first non-comment line.
Only one Option line may be present. The Option line
contains (5+NC) fields:
(Sentinel, NC, Exec, NS, Show, Color1, Color2, ..., ColorNC).
- Sentinel adj: - the first field must be the string "adj:"
- NC Number of colors (3 ≤ NC ≤ 6) or (NC == 0),
(when NC==0, NC is set to 4, and the colors are set
to Red, Green, Blue, Yellow)
- Exec 0/1: 0 (create .qubo file only);
1 (create .qubo file and execute it with Qbsolv)
- NS Number of solutions to show (1-6) silently enforced
- Show 0 - show text results only, or
fName - show text results, use file "fName" to draw map
(when fName is used, NC must 4 and the colors must
be chosen from {Red,Green,Blue,Yellow,Cyan,Purple})
- Color* Strings to represent the 'NC' colors (e.g., 'R G B Y' or
'Red Green Blue Pink Cyan Orange'). Each color name
should start with a different letter.
The Name fields (e.g., nm1, nm2, ...)
define the problem entities.
Each named entity must be (1-16) characters. All the Name lines
must appear before the first Adjacency line.
There must be 1 or more Adjacency
lines, which have this layout:
nm1 nm2, nm3, nm4
These items define the borders between named entities. The above
statement tells ToQ that nm1's neighbors are nm2, nm3, and nm4.
Therefore, in the results, nm1's property (e.g., color), will be
different than those of nm2, nm3, nm4. Each Named entity must
appear on at at least two Adjacency lines. No entity may have more
than 16 borders.
To work correctly, this adjacency option requires a planar map
with no adjacent entities joined only at a single point (for example,
on a USA map, (AZ,CO) and (NM,UT) should not be adjacent). Further,
entities with no adjacencies (e.g., Islands) are not allowed. For
all such maps, 4 colors are sufficient. Here is a very simple map
to be colored with 4 colors (5 different sets of 4 color maps will
be produced). Note that even for this simple map, 3 colors will not
be sufficient (just look at the [P,Q,R,S] quartet to verify).
_________________________
| | map1.adj contents
| P | -------------------
| _________________ | #~~~ Map based on Darmo's Puzzle
| | | | | adj: 4 1 5 0 Red Green Blue Yellow
| | Q | R | | #~~~ 8 counties
| |___|___________| | name: P Q R S T U V W
| | | | | #~~~ Adjacency info
|---| S | T |---| P Q R S T W
| |_______|_______| | Q P,R,S
| | | | | R P Q S T
| | U | V | | S R T U W P Q
| |___________|___| | T P R S U V W
| | U S, T, V, W
| W | V T U W
|_______________________| W P S T U V
Click here for a real, mouse-ready adjaceny file.
Major ToQ Files
===================
Input Output
========= ============================
quboFileNm qboutFileNm
---------- ------------
abc.toq
xyz.toq -q xyzTOQ.qubo xyzTOQ.qbout
jklTOQ.qubo jklTOQ.qbout
mnoTOQ.qbout
pqr.qubo pqr.qbout
def.qbout
ghi.cnf
puz.sud
grf.adj grfADJ.qubo grfADJ.qbout
bbq.cnf -q bbqCNF.qubo bbqCNF.qbout
vwxCNF.qubo vwxCNF.qbout
spqCNF.qbout
ToQ employs a single namespace. Therefore, for
example, "sin", "pi", and "sqrt" are not available as variable
names. Here is a list of all the keywords
(this list is not clickable).
abs epilogue listcmtbools mask23 naesat5 rowvectmtx tnsrready
acos errormgmt listcode mask24 naesatn rules tnsrvect
acosh even listconst mask25 nand same trunc
all exp listconstdef mask26 nbithit sat twoof
amalgam expm1 listconstdefs mask27 ndiff sat12 twoton
and factorial listconsts mask28 ndiff1 sat13 upperbd
antilog fibonacci listdir mask29 nearint sat14 valfile
any fillone listdirdef mask30 nof sat15 varfile
asin fillones listdirdefs mask31 none sat2 vect
asinh fillvec listdirs mask32 nor sat23 vectbit
assert fillzero listfunc mask3201 norless sat24 vectbitcount
assert1 fillzeroes listfuncdef mask3202 normore sat25 vectcompare
assert2 fillzeros listfuncdefs mask3204 not sat3 vectconcat
assertp flipflop listfuncs mask3208 nsame1 sat34 vectcopy
atan floatingpoint listgen mask3210 nuclmagn sat35 vectget
atan2 floor listop mask3220 numbers sat4 vectinit
atanh force listops mask3240 numbvals sat45 vectinsert
binary formalmod listproto mask3280 nxor sat5 vectmtx
bitcount fourthpi listprotos maskn octal satisfiability vectmtxrows
bitmask function listprototype max odd satn vectnot
bmask functionio listprototypes maxabs oneof setbit vectop
bmaskvals gcd listsat maximize or sin vectop2
bool getbit listsatdef mbool outrangeeq sinh vectop3
ceiling graphcoloring listsatdefs min outrangeneq sqrt vectpaint
clade gseries listsats minabs outset sqrt10 vectproc
clades halfpi ln minimize overview sqrt2 vectput
colswap help ln10 mod permutations sqrt3 vectready
colvectmtx hexadecimal ln1p mtx phi sqrt5 vectreverse
combinations if ln2 mtxbit phiinv sqrt6 vectshift
compiler iff ln3 mtxbitcount pi sqrt7 vecttomtx
conffile implies log mtxcompare pi43 sqrt8 viewvector
confile include log102 mtxconcat planck sqrtabs viewvectors
const initfile log103 mtxcopy planck2pi sqrte warningsoff
cos initialize log10e mtxflip popcount sqrtpi where
cosh inrangeeq log2 mtxget post subjto whereami
cubert inrangeneq longline mtxinit postio sudoku wrap
cubert2 inset lowerbd mtxinsertm pow sum wrapoff
cubert3 int lucas mtxinsertv pow2 sumdelta xnor
d2radians intp mask02 mtxnot prime syntax xor
dbpr inv mask03 mtxop print tan xor2sat
dbprint invmod mask04 mtxop3 printf tanh xor3sat
dbprintb irand mask05 mtxpaint printfn thirdpi xref
dbprintf isint mask06 mtxproc printsummary time xtand
dbprintm josephson mask07 mtxput printvar times xtandnot
dbprintt labeling mask08 mtxready printvars timing xteq
dbprintv lcm mask09 mtxreverse printx tnsr xtge
dbprintx leftc mask10 mtxrowvect putbit tnsrbit xtgt
dbquit lefts mask11 mtxshift quant tnsrbitcount xtiff
deciaml limit mask12 mtxswap quantio tnsrcompare xtimplies
diff limits mask13 mtxtovect radians2d tnsrcopy xtle
diff1 lineareq mask14 mtxvectinit rand tnsrget xtlt
electric linelength mask15 mtxvectop randseed tnsrgetstk xtneq
else listall mask16 mtxvectop3 real tnsrinit xtnoop
elseif listbool mask17 nae3sat realp tnsrmtx xtnor
enat listboolfunc mask18 nae4sat return tnsrnot xtnot
end listboolfuncs mask19 nae5sat rightc tnsrop xtor
endfunction listbools mask20 naesat rights tnsrop3 xtornot
endif listcmtall mask21 naesat3 round tnsrput xtxnor
endquant listcmtbool mask22 naesat4 rowswap tnsrputstk xtxor
epilog
The current limits:
4096 Max number of assert: statements
1024 Max number of bool: variables
16 Max number of bool: variables per assert:
128 Max number of variables in a statement
4096 Max number of lines
4095 Max characters in an input line
1024 Max number of variables
16 Max length of variable names
For ToQ, a file with an .adj suffix
describes an adjacency problem (frequently
referred to as a special case of graph labeling known as "graph
coloring"). Graph coloring algorithms are used in a variety of
applications, including a wide range of scheduling and pattern
matching problems. Examples include resource allocation under
constraints, molecular similarity analyses, regular expression
operations, image processing, compiler register allocation,
language recognition, ...
Map coloring is a well-known example of graph coloring,
and the rest of this description uses map coloring terminology
(e.g., colors for properties, areas or entities for nodes, and
borders or neighbors for edges). ToQ can manage arbitrarily large
arrays of adjacency information (utilizing the Qbsolv program).
Two output files are generated by "toq -i xyz.adj" - the .qubo file and
the .qbout file (xyzADJ.qubo, xyzADJ.qbout). ToQ reads the
.qbout file and presents the results back to the user. The input
file is recognized via its ".adj" suffix. It has three line
types (Option, Name, Adjacency), which must appear in order.
Input data is case-insensitive, however input case is used for output
presentation. The '#' character initiates a comment, which runs
to the end-of-line, can appear anywhere, and is otherwise ignored.
Fields are separated by one or more (blanks,commas,tabs). Lines
are terminated by the end-of-line.
The Option line must be the first non-comment line. Only one
Option line may be present.
The Option line contains (5+NC) fields:
(Sentinel,NC,Exec,NS,Show,Color1,Color2,...ColorNC).
- Sentinel − the first field must be the string
"adj:"
- NC − Number of colors (3 ≤ NC ≤ 6) or (NC == 0),
(when NC==0, NC is set to 4, and the colors are set
to Red, Green, Blue, Yellow)
- Exec − 0/1: 0 (create .qubo file only),
1 (create .qubo file and execute it with Qbsolv)
- NS − Number of solutions to show (1-6) silently enforced
- Show − 0 - show text results only, or
fName - show text results, use file fName to draw map
(when fName is used, NC must 4 and the colors must
be chosen from {Red,Green,Blue,Yellow,Cyan,Purple})
- Color* − Strings to represent the NC colors (e.g., 'R G B Y' or
'Red Green Blue Pink Cyan Orange'). Each color name
should start with a different letter.
The name fields (e.g., nm1, nm2, ...) define the problem entities.
Each named entity must be (1-16) characters. All the Name lines
must appear before the first Adjacency line.
There must be 1 or more Adjacency lines, which have this layout:
nm1 nm2, nm3, nm4
These items define the borders between named entities. The above
statement tells ToQ that nm1's neighbors are nm2, nm3, and nm4.
Therefore, in the results, nm1's property (e.g., color), will be
different than those of nm2, nm3, nm4. Each Named entity must
appear on at at least two Adjacency lines. No entity may have more
than 16 borders.
To work correctly, this adjacency option requires a planar map
with no adjacent entities joined only at a single point (for example,
on a USA map, (AZ,CO) and (NM,UT) should not be adjacent). Further,
entities with no adjacencies (e.g., Islands) are not allowed. For
all such maps, 4 colors are sufficient. Here is a very simple map
to be colored with 4 colors (5 different sets of 4 color maps will
be produced). Note that even for this simple map, 3 colors will not
be sufficient (just look at the [P,Q,R,S] quartet to verify).
_________________________
| | map1.adj contents
| P | -------------------
| _________________ | #~~~ Map based on Darmo's Puzzle
| | | | | adj: 4 1 5 0 Red Green Blue Yellow
| | Q | R | | #~~~ 8 counties
| |___|___________| | name: P Q R S T U V W
| | | | | #~~~ Adjacency info
|---| S | T |---| P Q R S T W
| |_______|_______| | Q P,R,S
| | | | | R P Q S T
| | U | V | | S R T U W P Q
| |___________|___| | T P R S U V W
| | U S, T, V, W
| W | V T U W
|_______________________| W P S T U V
ToQ has 3 ways to address maximization and
minimization problems.
- Build a program with constraint variables and assert statements
followed by a "post:" statement, then a single "maximize:" or
"minimize:" statement. The D-Wave finds all the sets of constraint
variable values for which all the asserts are TRUE, then the max/min
statement is executed for all those cases, and the max or min is
selected.
- Use the -QM flag to execute a program comprised of an opening
maximize or minimize statement, followed by a series of "subjto:"
statements. When the "end:" statement is encountered, a QUBO is
built and fed to the D-Wave (via Qbsolv), and the result is then
displayed. This is developing technology, and there are some
restrictions on the statements. Set partitioning is a good
example of this set up.
- Use the -Qm flag to execute a single "maximize:" or
"minimize:" statement which acts on all the combinations of the
declared constraint variables. This mechanism does not use the
D-Wave, but rather does brute force computations and displays the
max and min values with their corresponding variable values. This
mechanism is only provided as a convenience (and performance is
consistent with interpreted code), and the number of
bits to represent all the constraint variables should be less
than about 25.
The D-Wave is probabilistic. If "nResults" on the configuration
file is set to N, the system collects N results, then checks each
for correctness. If one or more results are faulty, another pass
is initiated. Therefore, the sum (S) of the "nOccurrences" of the
successful profiles will be: (S < 2N).
ToQ number representation is straightforward.
Int: variables are 32-bit integers,
and real: variables are 64-bit floating point values.
- Real: values and constants in a ToQ program may have a sign, zero
or one decimal points, an exponent, but no commas.
- Int: variables and constants may have a sign,
and may be expressed in decimal, octal, or hexadecimal. They
may not contain any commas.
- Octal numbers start with "0o"
- Hexadecimal numbers start with "0x"
There is no mechanism to represent
binary numbers. Integers may not have exponents.
The statement "int: abc = 45.3" will generate a
warning and abc will be truncated to to 45, and the
statement "int: vbb = -443.99" will be truncated to
-443 (not rounded to -444).
Here are some examples:
1 4.56 0x1234bc4f 0o7633 -9.8733e-5 +17
-44.39 73.11e-10 1.245e6 987633 -3451 19e+04
567r2 0o56933 0x93eg3a <-- these 3 are errors
qOp is the (growing) quantum toolset from D-Wave.
It is comprised of:
A QUBO (Quadratic Unconstrained Binary Optimization problem) is also
known as UBQP: Unconstrained Binary Quadratic Programming problem.
D-Wave Computer systems employ Adiabatic Quantum Annealing to
solve QUBOs by exploiting some of the strange properties of the
quantum world - solution mechanisms different than those used to solve
these problems on classical computers. QUBOs are NP-hard. A
typical QUBO is concerned with the minimization of a quadratic equation
in N boolean-valued [0,1] variables. Here is a typical example.
Q = Sum[i=1,N]{A(i)*q(i)} + Sum[i=1,N]{Sum[j=i+1,N]{B(i,j)*q(i)*q(j)}}
where the objective is to find the values of the booleans q()
such that Q is a minimum for a given set of values of the
Ai and Bi,j arrays.
The Ai and Bi,j arrays
represent the problem input, and the q() represent the results.
QUBOs are an integral part of many important
computational problems, including pattern matching in machine learning
algorithms, image recognition, financial analysis, computer-aided
design, solid state physics, traffic message management, power network
design, ...
ToQ users can create a Qubo File and use the
Qbsolv program to resolve their program.
Qbsolv is a powerful tool which can "solve" Qubos. It is not
limited by the size of the target D-Wave machine, rather it takes the
input problem and partitions it into D-Wave-size chunks, runs them, and
sends the composite results back to ToQ for presentation
of results to the user.
The Using Qbsolv section describes how to use it,
along with descriptions of the input and output files.
When ToQ sends a problem to the D-Wave, it must be
embedded in the "chimera" interconnection network on the host
machine. The embedding process
employs a random number generator to get started, which means
that subsequent otherwise identical runs may get a different
embedding. You can generate reproducible embedding by
setting the random number generator seed via a commandline
argument ("-Qr") − enter toq -h random for details.
Also, ToQ
programs can use a random number generator during execution.
To get reproducible results, see item (2) below.
ToQ uses a random number generator in two independent ways:
- By using the commandline "-Qr789" option (where "789"
represents an integer in [1-100,000]), you can force reproducibility
on the embedding process.
- Two functions (Rand(), IRand()) are available to generate
a pseudo random sequence of values in a ToQ program. The
RandSeed() function is available to set a seed for the random
number generator to get repeatable sequences. For details,
click rand().
However, note that even with the same embedding, the quantum
nature of the D-Wave may cause you to get different results for the
same problem. For example, suppose a problem has 45 sets of
values for your constraint variables which satisfy all the
asserts in your program. On one run, you may get only 42 aets.
On another run, you may get 41 or 45 or 44. All the solution
sets will satisfy all the asserts, but two sets of 42 may not be
identical.
A clause is satisfiable if at least one element is TRUE.
A problem is satisfiable if all clauses are TRUE. ToQ provides
simple mechanisms to address some satisfiability problems. ToQ
recognizes the following satisfiability functions for use
as the object of an assert statement (all require bool arguments).
- Sat - TRUE when any of the 1-6 arguments is TRUE
- Sat12 - TRUE when exactly 1 of its 2 arguments is TRUE
- Sat13 - TRUE when exactly 1 of the 3 arguments is TRUE
- Sat14 - TRUE when exactly 1 of the 4 arguments is TRUE
- Sat15 - TRUE when exactly 1 of the 5 arguments is TRUE
- Sat2 - TRUE when either of the 2 arguments is TRUE
- Sat23 - TRUE when exactly 2 of the 3 arguments are TRUE
- Sat24 - TRUE when exactly 2 of the 4 arguments are TRUE
- Sat25 - TRUE when exactly 2 of the 5 arguments are TRUE
- Sat3 - TRUE when any of the 3 arguments is TRUE
- Sat34 - TRUE when exactly 3 of the 4 arguments are TRUE
- Sat35 - TRUE when exactly 3 of the 5 arguments are TRUE
- Sat4 - TRUE when any of the 4 arguments is TRUE
- Sat45 - TRUE when exactly 4 of the 5 arguments are TRUE
- Sat5 - TRUE when any of the 5 arguments are TRUE
- SatN - TRUE when exactly N of the remaining arguments are TRUE
- NAE3Sat - TRUE when any pair of the 3 arguments is different
- NAE4Sat - TRUE when any pair of the 4 arguments is different
- NAE5Sat - TRUE when any pair of the 5 arguments is different
- NAESat - TRUE when any pair of the 2-6 arguments is different
- NAESat3 - TRUE when any pair of the 3 arguments is different
- NAESat4 - TRUE when any pair of the 4 arguments is different
- NAESat5 - TRUE when any pair of the 5 arguments is different
- NAESatN - TRUE when any pair of the N (<=6) arguments is different
- Xor2Sat - TRUE when its two arguments are different
- Xor3Sat - TRUE when one or all of its 3 arguments is TRUE
Negation of any of the arguments can be done in 3 ways (these
three examples are equivalent):
bool: @r, @s, @t
assert: SAT3( @r, NOT(@s), @t )
assert: SAT3( @r, !@s, @t )
assert: SAT3( @r, -@s, @t )
Note that the "−" operator reverses the value of its
argument. Further, ToQ accepts standard DIMACS
format files as input (file.cnf). Using this special file
implies:
- No other input is allowed
- The "satisfiability:" directive is assumed
- No need to declare any variables (all handled internally)
- Legal items must be in the range (1-99)
- Enter "help: cnf" to get the format of .cnf files
- Use "toq -t satType" to further modify the behavior
of the .cnf line items. "satType" is one of:
{ 1in2, 1in3, 1in4, 1in5, 2in3, 2in4, 2in5, 3in4, 3in5,
4in5, nae, nae3, nae4, nae5, naen, sat2, sat3, sat4,
sat5, satn, xor2, xor3 }.
This option works only with "cnf" on the Problem line
(not with the "cnf+" option). Enter "help: cnf" for
details about these modifiers and about "cnf+"
If a software simulator is available on your host system, you
may wish to use it for some of your small cases rather than
connecting to an actual D-Wave system. To do so, use this
line in your configuration file (-z option or conffile: directive):
url localhost
int: a, b a = 17 bool: @y3,
@y4, @ynot |
|
real: x1, x2 x1 = 51.33 x2 =
sin(sqrt((x1-2)*(x1+2)) |
|
bool: @a, @b assert: ((@a+@b) > 3) |
|
real: acre, tBar, x, Acre, beta |
|
real: @x, @y x = sqrt(PI*y) |
|
bool: @q, @b int: pp, kk kk = 37 pp
= kk*(@a+@b) |
|
int: @pp, @kk kk = 17 pp = kk*((kk1−1)/2) |
|
real: ee = 1.057, ff = 17.3 assert: (ee > ((ff+1)/ff)) |
|
bool: @r, @s assert: (sqrt(2*PI-4*(@r+@s)) > 1) |
|
bool: @looney, @tooney @looney = 7 |
(Numbering by column)
- a = 17 is misplaced. All declarations must
precede the first executable statement.
- assert: ((@a+@b) > 3) can never be TRUE.
ToQ flags any assert which can't be both TRUE and
FALSE for various combinations of its boolean variables as an error.
- x = sqrt(PI*y) y is uninitialized.
- pp = kk*((kk1−1)/2) kk1 is
not declared.
- assert: (sqrt(2*PI-4*(@r+@s)) >
1) When
@r = @s = 1, the argument to Sqrt() will be negative.
- x2 = sin(sqrt((x1-2)*(x1+2))
mismatched
()s.
- real: acre, tBar, x, Acre,
beta
acre is declared twice.
- pp = kk*(@a+@b) boolean variables
@a and @b may only be used in an
assert statement.
- assert: (ee > ((ff+1)/ff))
assert statements
must act on boolean variables.
- @looney = 7 @looney is a constraint
variable and may not be set by the program.
This file (xyz.sud) describes a sudoku puzzle - 4 sizes are
available (6x6, 9x9, 12x12, 16x16), as well as a variable alphabet.
The format of a .sud file is simpler and less restrictive
than using the standard .toq sudoku format.
Most frequently-found are 9x9 puzzles with the standard alphabet
(123456789). Input is comprised of a header line followed by
6, 9, 12, or 16 data lines which contain the initial cell values.
The header line has two fields:
N Alphabet
where N is one of (6,9,12,16), and Alphabet is a string (with no
spaces). Alphabet may be "std" (representing "123456", "123456789",
"123456789ABC", "123456789ABCDEFG") or may be a string
built from these 31 characters (with no duplicates):
(1-9, A-H, J, K, M, N, P, R-Z)
Note that the alphabet is case-insensitive, and may not contain these
5 characters (0IOLQ). Each data line must contain exactly N
characters from the alphabet and the 4 characters
._*0 (which represent empty cells).
These 6 characters { blank, comma, tab, pipe, dash, plus } are
ignored, and # initiates a comment, which runs to the end of the
line (and thus the rest of the line is ignored (may contain any
character)). Any other character is an error. Blank
lines are ignored (not counted as a data line).
Valid sudoku puzzles have a unique solution. To
execute ToQ on a .sud file, enter: toq
-i xyz.sud – here are five valid examples:
(1) 51 Open | (2) Harder | (3) Very Hard
| |
9 std | 9 Std | 9 STD
| |
...425.3. | _ _ 2 _ _ _ _ 6 9 | 8,0,0, 0,0,0, 0,0,0
.7....5.. | _ 1 _ 5 4 9 2 _ _ | 0,0,3, 6,0,0, 0,0,0 # Try it
....861.. | _ 3 _ _ _ _ 5 1 _ | 0,7,0, 0,9,0, 2,0,0 # by hand
8..9..... | |
32.867.45 | _ 8 _ 1 _ _ 7 _ 6 | 0,5,0, 0,0,7, 0,0,0 # Only 21
.....38.6 | _ _ _ 7 _ _ _ 5 _ | 0,0,0, 0,4,5, 7,0,0 # cells
..854.... | _ _ _ _ 6 _ _ _ 8 | 0,0,0, 1,0,0, 0,3,0 # given
..2....8. | |
.1.698... | _ _ 5 4 _ _ _ 3 _ | 0,0,1, 0,0,0, 0,6,8
| 8 _ _ _ _ 5 _ _ _ | 0,0,8, 5,0,0, 0,1,0
| _ 4 1 _ _ 2 _ _ 5 | 0,9,0, 0,0,0, 4,0,0
---------------------------------------------------------------------------------
(4) 54 Open | (5) 16 x 16
|
9 123456789 | 16 123456789RSTWXYZ
|
5 * * | 4 7 * | 2 6 3 | .... | .5.. | 6.Y. | S.4.
* * * | 1 6 * | 9 * 4 | ..49 | .XR. | 83.. | W...
* * * | * 2 * | * 7 * | ..X6 | 8ZW. | .S.. | .Y..
------+-------+------ | .... | 1... | .W4R | .836
* * 3 | * 1 4 | 7 * * | ------+--------+--------+------
* * * | * * * | * * * | ...8 | .17. | .423 | ..RW
* * 9 | 5 3 * | 6 * * | .... | Z..X | WR.. | ....
------+-------+------ | .X52 | W64. | .1.9 | .TZ.
* 4 * | * 9 * | * * * | .... | ..2. | ..S. | .9X.
1 * 6 | * 5 2 | * * * | ------+--------+--------+------
9 7 2 | * 4 1 | * * 8 | .... | XWS1 | .8T. | 5...
| ...X | 3... | .... | 7.29
| .... | .... | ...7 | 3.TY
| 6... | .Y.. | 5..W | .S..
| ------+--------+--------+------
| .... | 5..Y | ...2 | ..1X
| 8..Z | .... | .... | T2..
| .56R | ..Z. | 3.14 | .7..
| .31. | 9... | Y.7. | Z.5.
A .toq file contains a program for execution by
ToQ. The file is line-oriented, ASCII,
case-insensitive, and blanks and tabs are ignored.
Click here
for a review of ToQ 's syntactic and semantic rules.
A ToQ program is made up of three statement types.
Comments are initiated by the "#" character and run to the
end-of-line. Comments may appear anywhere in the program, and are
otherwise ignored.
- Directives: one word commands which always end with the
":" character. Some directives have arguments. May
appear anywhere in the program. Click here, or enter "toq -d" for a list of all the
directives, or "toq -D" for a list with descriptions.
End: must be the last statement in the program.
- Declarations: all variables must be declared before the
first executable statement. Click here or
enter "toq -H type" for a description of the valid types.
- Executables:
replacement,
control flow, and
assert
statements. For details, click the links or enter "toq -H repl"
or "toq -H control" or "toq -H assert"
Here is a simple example:
varfile: myVars # contains decls, values for (x,y,z)
bool: @a,@b,@c
# ~~~
if: (x == 3)
assert:and(@a,@b)
elseif: (y < 9)
assert:or(@a,@c)
else:
z = x-y
assert:and(@b,or(@a,@c))
endif:
# ~~~
listcode:
end:
The .toqrc file contains some configuration parameters which
may be used in a
ToQ execution. Parameters in a .toqrc file
override values from the environment (enter "toq -H env" for more
details). Some commandline parameters may override .toqrc
values. Your .toqrc file should live in your current working
directory. Here is a sample .toqrc file:
TOQ engine = c4-sw_sample
TOQ token = 123
TOQ url = localhost
TOQ nresults = 1000
This example is set up to run on the D-Wave simulator (part of the
qOp toolset). The keyword engine
may be replaced with solver. When running on a real
D-Wave system, you must supply token with your
40-hexadecimal access word, and the url should be
set to the target machine.
It is recommended and most users find it most convenient to use
the "dw" command to set up their environment.
Click dw or enter "toq -H dw"
for details.
#
# New Mexico (33 Counties) Adjacency File
#
# # Colors # Nodes # Couplers
# -------- ------- ----------
# 4 132 510
# 5 165 720
# 6 198 963
#
adj: 4 1 3 0 Red Greeen Blue Yellow
# ~~~
name: Bernalillo Catron Chaves Cibola Colfax Curry De_Baca Dota_Ana
name: Eddy Grant Guadalupe Harding Hidalgo Lea Lincoln Los_Alamos Luna
name: McKinley Mora Otero Quay Rio_Arriba Roosevelt San_Juan San_Miguel
name: Sandoval Santa_Fe Sierra Socorro Taos Torrance Union Valencia
# ~~~
Bernalillo Cibola, Sandoval, Santa_Fe, Torrance, Valencia
Catron Cibola, Grant, Sierra, Socorro
Chaves De_Baca, Eddy, Lea, Lincoln, Otero, Roosevelt
Cibola Bernalillo, Catron, McKinley, Sandoval, Socorro, Valencia
Colfax Harding, Mora, Taos, Union
Curry Quay, Roosevelt
De_Baca Chaves, Guadalupe, Lincoln, Quay, Roosevelt
Dota_Ana Luna, Otero, Sierra
Eddy Chaves, Lea, Otero
Grant Catron, Hidalgo, Luna, Sierra
Guadalupe De_Baca, Lincoln, Quay, San_Miguel, Torrance
Harding Colfax, Mora, Quay, San_Miguel, Union
Hidalgo Grant, Luna
Lea Chaves, Eddy, Roosevelt
Lincoln Chaves, De_Baca, Guadalupe, Otero, Sierra, Socorro, Torrance
Los_Alamos Rio_Arriba, Sandoval, Santa_Fe
Luna Dota_Ana, Grant, Hidalgo, Sierra
McKinley Cibola, San_Juan, Sandoval
Mora Colfax, Harding, Rio_Arriba, San_Miguel, Santa_Fe, Taos
Otero Chaves, Dota_Ana, Eddy, Lincoln, Sierra
Quay Curry, De_Baca, Guadalupe, Harding, Roosevelt, San_Miguel, Union
Rio_Arriba Los_Alamos, Mora, San_Juan, Sandoval, Santa_Fe, Taos
Roosevelt Chaves, Curry, De_Baca, Lea, Quay
San_Juan McKinley, Rio_Arriba, Sandoval
San_Miguel Guadalupe, Harding, Mora, Quay, Santa_Fe, Torrance
Sandoval Bernalillo, Cibola, Los_Alamos, McKinley, Rio_Arriba, San_Juan, Santa_Fe
Santa_Fe Bernalillo, Los_Alamos, Mora, Rio_Arriba, San_Miguel, Sandoval, Torrance
Sierra Catron, Dota_Ana, Grant, Lincoln, Luna, Otero, Socorro
Socorro Catron, Cibola, Lincoln, Sierra, Torrance, Valencia
Taos Colfax, Mora, Rio_Arriba
Torrance Bernalillo, Guadalupe, Lincoln, San_Miguel, Santa_Fe, Socorro, Valencia
Union Colfax, Harding, Quay
Valencia Bernalillo, Cibola, Socorro, Torrance
Sample-01
(Life, the Universe, and Everything)
# ~~~ factor42.toq ~~~
Regression test
#
# Find two 3-bit factors of 42
#
bool: @a1,@a2,@a3, @b1,@b2,@b3
# ~~~
assert: (((@a1 + 2*@a2 + 4*@a3) * (@b1 + 2*@b2 + 4*@b3)) == 42)
# ~~~
end:
Sample-02
(If−Then−Else: Setup)
# ~~~ simple.toq ~~~
Regression test
#
# Exercise And() and Or()
#
bool: @a, @b, @c, @d
# ~~~
assert: And(Or(@a,@b), Or(@c,@d))
assert: @c != @d
assert: (@a+@d >= (@b+@c))
# ~~~
end:
Sample-02b
(If−Then−Else: In Use)
# ~~~ simpleIF.toq ~~~
Regression test
#
# Simple IF-THEN-ELSE test
#
bool: @a, @b, @c, @d
real: x = PI, y, z
# ~~~
y = Sqrt(x+2)
z = x-y
assert: And(Or(@a,@b), Or(@c,@d))
if: ((z*x)/3 > 3.11)
assert: @c != @d
endif:
assert: (@a+@d >= (@b+@c))
# ~~~
end:
Sample-03
(Graph Coloring)
# ~~~ map51.toq ~~~
Regression test
#
# Find a 3-color map for these 5 countries
#
# -------------------------
# | A |
# | ----------------- |
# | | B
| |
# | |---------------- |
# | | | | | |
# | | C | D | E | |
# | | | | | |
# -------------------------
#
bool: @Ared, @Ablue, @Agreen
bool: @Bred, @Bblue, @Bgreen
bool: @Cred, @Cblue, @Cgreen
bool: @Dred, @Dblue, @Dgreen
bool: @Ered, @Eblue, @Egreen
# ~~~
assert: OneOf(@Ared,@Ablue,@Agreen) # A may be only 1 color
assert: OneOf(@Bred,@Bblue,@Bgreen) # B may be only 1 color
assert: OneOf(@Cred,@Cblue,@Cgreen) # C may be only 1 color
assert: OneOf(@Dred,@Dblue,@Dgreen) # D may be only 1 color
assert: OneOf(@Ered,@Eblue,@Egreen) # E may be only 1 color
#
assert: Nand(@Ared,@Bred) # A,B not both red
assert: Nand(@Ablue,@Bblue) # A,B not both blue
assert: Nand(@Agreen,@Bgreen) # A,B not both green
#
assert: Nand(@Ared,@Cred) # A,C not both red
assert: Nand(@Ablue,@Cblue) # A,C not both blue
assert: Nand(@Agreen,@Cgreen) # A,C not both green
#
assert: Nand(@Ared,@Dred) # A,D not both red
assert: Nand(@Ablue,@Dblue) # A,D not both blue
assert: Nand(@Agreen,@Dgreen) # A,D not both green
#
assert: Nand(@Bred,@Cred) # B,C not both red
assert: Nand(@Bblue,@Cblue) # B,C not both blue
assert: Nand(@Bgreen,@Cgreen) # B,C not both green
#
assert: Nand(@Bred,@Dred) # B,D not both red
assert: Nand(@Bblue,@Dblue) # B,D not both blue
assert: Nand(@Bgreen,@Dgreen) # B,D not both green
#
assert: Nand(@Bred,@Ered) # B,E not both red
assert: Nand(@Bblue,@Eblue) # B,E not both blue
assert: Nand(@Bgreen,@Egreen) # B,E not both green
#
assert: Nand(@Cred,@Dred) # C,D not both red
assert: Nand(@Cblue,@Dblue) # C,D not both blue
assert: Nand(@Cgreen,@Dgreen) # C,D not both green
#
assert: Nand(@Dred,@Ered) # D,E not both red
assert: Nand(@Dblue,@Eblue) # D,E not both blue
assert: Nand(@Dgreen,@Egreen) # D,E not both green
# ~~~
end:
Sample-04
(Simpler Graph Coloring)
# ~~~ map52.toq ~~~
Regression test
#
# Find a 3-color map for these 5 countries
#
# -------------------------
# | A |
# | ----------------- |
# | | B
| |
# | |---------------- |
# | | | | | |
# | | C | D | E | |
# | | | | | |
# -------------------------
#
mbool: 1,3, @A, @B, @C, @D, @E
# ~~~
assert: @A != @B
assert: @A != @C
assert: @A != @E
assert: @B != @C
assert: @B != @D
assert: @B != @E
assert: @C != @D
assert: @D != @E
# ~~~
end:
Sample-05 (Painless Graph Coloring)
# ~~~ map53.toq ~~~
Regression test
#
# Find a 3-color map for these 5 countries
#
# -------------------------
# | A |
# | ----------------- |
# | | B
| |
# | |---------------- |
# | | | | | |
# | | C | D | E | |
# | | | | | |
# -------------------------
#
mbool: 1,3, @A, @B, @C, @D, @E
# ~~~
assert: Diff1(@A, @B,@C,@E)
assert: DIff1(@B, @C,@D,@E)
assert: Diff1(@D, @C,@E)
# ~~~
end:
Sample-06
(Micro-Sudoku)
# ~~~ microsud.toq ~~~
Regression test
#
# Solve this simple Sudoku-like puzzle
#
# ___________________
___________________
# | | | |
| | | |
# | 1 | | |
| 1 | A | B |
# |_____|_____|_____|
|_____|_____|_____|
# | | | |
| | | |
# | | | 2 | ==>
| C | D | 2 |
# |_____|_____|_____|
|_____|_____|_____|
# | | | |
| | | |
# | | 3 | |
| E | 3 | F |
# |_____|_____|_____|
|_____|_____|_____|
#
mbool: 1,3, @A,@B,@C,@D,@E,@F
# ~~~
assert: Diff(1,@A,@B)
# Row 1 entries different
assert: Diff(@C,@D,2)
# Row 2 entries different
assert: Diff(@E,3,@F)
# Row 3 entries different
assert: Diff(1,@C,@E)
# Col 1 entries different
assert: Diff(@A,@D,3)
# Col 2 entries different
assert: Diff(@B,2,@F)
# Col 3 entries different
# ~~~
end:
And here is an alternate solution using NDiff()
mbool: 1,3, @A,@B,@C,@D,@E,@F
# ~~~
assert: NDiff(1,@A,@B) == 3
# Row 1 entries different
assert: NDiff(@C,@D,2) == 3
# Row 2 entries different
assert: NDiff(@E,3,@F) == 3
# Row 3 entries different
assert: NDiff(1,@C,@E) == 3
# Col 1 entries different
assert: NDiff(@A,@D,3) == 3
# Col 2 entries different
assert: NDiff(@B,2,@F) == 3
# Col 3 entries different
# ~~~
end:
Sample-07
(Teenagers)
# ~~~ teenagers.toq ~~~
Regression test
#
# You have 3 teenagers (Al, Bobby, Chris)
# Find the age of each teen given:
#
# 2A - 3B + 2C = 0
#
# 3A + B - 4C = 1
#
# ~~~
mbool: 13,19, @a,@b,@c
# ~~~
assert: (2*@a - 3*@b + 2*@c) == 0
assert: (3*@a + @b - 4*@c) == 1
# ~~~
end:
Sample-08
(Planet of the Sloths)
# ~~~ sloths.toq ~~~
Regression test
#
# On the Planet of the Sloths, how many ways are there to make
# change for a Slork (a Slork is 27 Slents)? The coins of
# the realm are the Slent, the Trey (3 Slents)
# and the Urp (9 Slents).
#
# How many of them have at least one of each coin, less than
# 11 slents and less than 6 urps? What are they?
#
int: slent=1, trey=3, urp=9
mbool: 0,27, @s
mbool: 0,9, @t
mbool: 0,3, @u
# ~~~
assert: @s*slent + @t*trey + @u*urp == 27
# ~~~
post:
assertp: (InRangeEq(@s,1,10) && InRangeEq(@t,1,5) && (@u > 0))
# ~~~
end:
Here is alternate solution 1.
int: slent=1, trey=3, urp=9
mbool: 1,10, @s
mbool: 1,5, @t
mbool: 1,2, @u
# ~~~
assert: @s*slent + @t*trey + @u*urp == 27
# ~~~
post:
assertp: ((@s < 11) && (@t < 6) && (@u < 3))
# ~~~
end:
Here is alternate solution 2.
int: slent=1, trey=3, urp=9
mbool: 1,10, @s
mbool: 1,5, @t
mbool: 1,2, @u
# ~~~
assert: @s*slent + @t*trey + @u*urp == 27
# ~~~
end:
All three samples give the same answer. What are the tradeoffs
associated with choosing one of these?
Sample-09
(The FedEx Problem)
# --- fedex.toq --- Regression Test
#
# You have 5 packages to deliver (in one trip in a truck
# with finite capacity). You want to maximize the priorities
# of the packages you choose. The packages weigh
# { 813, 719, 120, 575, 235 } pounds, and their volumes are
# { 79, 78, 18, 72, 27 } cubic feet. The priorities are
# { 1, 2, 3, 2, 3 } where the higher the priority
# number, the more important the package. Your truck can
# carry 1550 pounds and has 179 cubic feet of space. For
# each run, you want to maximize the sum of the priorities of
# the packages on board. Without concern for packing nor for
# distances, which packages do you take on your first trip?
#
#~~~
bool: @a,@b,@c,@d,@e
int: aw=813, bw=719, cw=120, dw=575, ew=235
int: av=79, bv=78, cv=18, dv=72, ev=27
int: ap=1, bp=2, cp=3, dp=2, ep=3
# ~~~
assert: (@a*aw + @b*bw + @c*cw + @d*dw + @e*ew) < 1550
assert: (@a*av + @b*bv + @c*cv + @d*dv + @e*ev) < 179
# ~~~
post:
maximize: (@a*ap + @b*bp + @c*cp + @d*dp + @e*ep)
# ~~~
end:
Sample-10
(Simple TSP)
Here is the file dist5.
vars 1 10
int: ab = 500
int: ac = 200
int: ad = 185
int: ae = 205
int: bc = 305
int: bd = 360
int: be = 340
int: cd = 320
int: ce = 165
int: de = 302
And here is the ToQ program (which uses
dist5).
# --- tsp53.toq --- Regression Test
# Distances
# A ===========
# A B C D E
# ---------------------------
# B E A | - 500 200 185 205 |
# B | 500 - 305 360 340 |
# C | 200 305 - 320 165 |
# C D D | 185 360 320 - 302 |
# E | 205 340 165 302 - |
# Traveling Salesman ---------------------------
# ~~~
varfile: dist5 # Get the distances
bool: @ab,@ac,@ad,@ae, @bc,@bd,@be, @cd,@ce, @de,
# ~~~
assert: TwoOf(@ab,@ac,@ad,@ae) # All the A paths
assert: TwoOf(@ab,@bc,@bd,@be) # All the B paths
assert: TwoOf(@ac,@bc,@cd,@ce) # All the C paths
assert: TwoOf(@ad,@bd,@cd,@de) # All the D paths
assert: TwoOf(@ae,@be,@ce,@de) # All the E paths
# ~~~
post:
minimize: (@ab*ab + @ac*ac + @ad*ad + @ae*ae + _
_ @bc*bc + @bd*bd + @be*be + @cd*cd + _
_ @ce*ce + @de*de)
# ~~~
end:
Note that the Continuation Character ("_")
has been used here to improve readability.
Sample-11
(Tiny Quant)
# --- q024.toq --- QUANT w/ bools, extBools
#
# Expected results
# --------------------
# 1) bool @b1 1 0 0 1 0 0 0 0 | 0:1 = 7:2
# 2) bool @b2 0 1 0 0 1 0 0 0 | 0:1 = 6:3
# 3) mbool 3,14,2 @m1 3 3 5 5 5 7 9 11 | 3-11'
# ' partial range
#
bool: @b1, @b2
mbool: 3,14,2, @m1
int: n1, n2, n3, n4
# ~~~
quant:
n1 = @b1+3*@b2
n2 = Max(n1,(@m1-6*@b2))
n3 = (@b1+@b2)*@m1
n4 = n1+n2+n3
assert: InRangeEq(n4,5,11)
endquant:
# ~~~
end:
(Early) Draft
Copyright © 2017 D-Wave Systems, Inc.
~~~//~~~