ISAT 2016
Introduction
Details about the purpose of iSAT can be found on the official web page which states:
iSAT has been developed to facilitate automated reasoning about large Boolean combinations of non-linear arithmetic constraints involving transcendental functions. The core of iSAT is based on a tight integration of recent DPLL-style SAT solving techniques (like lazy clause evaluation, conflict-driven learning, non-chronological backtracking, and restarts) with interval-based arithmetic constraint solving.
Installed version
iSAT is installed as a so called generic software module. This means, it is available on most of our environments. This implies, that every module on each of our different environments actually links to the same software path:
/cm/shared/uniol/software/generic/iSAT/<iSAT_version>
These versions are installed and and currently available ...
... on envirnoment hpc-uniol-env:
- 'iSAT/1.0-Singularity
... on environment hpc-env/6.4:
- 'iSAT/1.0-Singularity
... on environment hpc-env/8.3:
- 'iSAT/1.0-Singularity
Using iSAT
The iSAT module iSAT/1.0-Singularity is installed as a Singularity container. If you are already accustomed to working with containers e.g. Docker, you should not have any problems getting started. But even if you are not familiar with containarized software, we made it as easy as possible to get started with iSAT.
Usually, to call an executable from a singularity container, you have to go through singularity like this: singularity exec <container_name.sif> <command_inside_container> .
But on our cluster we set up some scripts for the most important functions:
- isat <arguments> <input_file>
- actually calls iSAT like this: singularity run <container_image> <your_arguments+file>
- execute_shell_command <executable> <arguments> <input_file>
- executes any command in case just calling isat is not enought.
- e.g.: execute_shell_command ls -la /usr/local/bin ## print binary directory inside iSAT container and immediately exit container session afterwards
- isat_shell
- Only recommendet for more experienced linux users.
- opens a bash shell within the container.
- exit with CMD + D or exit
- isat_bmc
- Executes binary isat_bmc .
- isat_probsat_tree_test
- Executes binary isat_probsat_tree_test .
- parallel_isat --i <input_file>
- Executes binary parallel_isat .
- sigmoid_prop_test <arguments> <input_file>
- Executes binary sigmoid_prop_test .
- test_deductions <arguments>
- Executes binary test_deductions .
Naturally, these scripts only work during the time fluka/***-Singularity is loaded.
Using iSAT executables
To find out on how to use the different iSAT binaries, you can call the aid scripts without options to find out if the developers embedded a help function. isat_bmc for example, prints out a help message after calling it. So, after loading the module, call said script to print out a help text to get you started:
$ isat_bmc
This is iSAT 0.1.
Usage: isat_bmc --i inputfile
General iSAT options:
--heu=bmc-fwd : BMC forward
bmc-bwd : BMC backward
b-fst : Boolean first
b-lst : Boolean last
int-fst : Integer first
int-lst : Integer last
vsids : VSIDS
You may specify up to four variable ordering heuristics.
The second heuristic will be used to sort the variables
that are equal wrt. the first heuristics, etc.
disc-fst : split all discrete variables down to the msw (normally
thus down to being point-valued) before splitting any
real-valued variable.
dyn-abs-width : Override the given static order and == Introduction ==
Details about the purpose of iSAT can be found on the [https://projects.avacs.org/projects/isat/ official web page] which states:
<blockquote>
iSAT has been developed to facilitate automated reasoning about large Boolean combinations of non-linear arithmetic constraints involving transcendental functions. The core of iSAT is based on a tight integration of recent DPLL-style SAT solving techniques (like lazy clause evaluation, conflict-driven learning, non-chronological backtracking, and restarts) with interval-based arithmetic constraint solving.
</blockquote>
== Installed version ==
iSAT is installed as a so called <tt>generic</tt> software module. This means, it is available on most of our environments. This implies, that every module on each of our different environments actually links to the same software path: <br>
''/cm/shared/uniol/software/generic/iSAT/<iSAT_version>''
These versions are installed and and currently available ...
<br/>
... on envirnoment ''hpc-uniol-env'':
*'''iSAT/1.0''-Singularity
<br/>
... on environment ''hpc-env/6.4'':
*'''iSAT/1.0''-Singularity
<br/>
... on environment ''hpc-env/8.3'':
*'''iSAT/1.0''-Singularity
== Using iSAT ==
The iSAT module ''iSAT/1.0-Singularity'' is installed as a Singularity container. If you are already accustomed to working with containers e.g. ''Docker'', you should not have any problems getting started. But even if you are not familiar with containarized software, we made it as easy as possible to get started with ''iSAT''.
Usually, to call an executable from a singularity container, you have to go through singularity like this: <tt>singularity exec <container_name.sif> <command_inside_container> </tt>. <br/> But on our cluster we set up some scripts for the most important functions:
* <tt>isat <arguments> <input_file> </tt>
** actually calls iSAT like this: singularity run <container_image> <your_arguments+file>
* <tt>execute_shell_command <executable> <arguments> <input_file> </tt>
** executes any command in case just calling isat is not enought.
**e.g.: execute_shell_command ls -la /usr/local/bin ## print binary directory inside iSAT container and immediately exit container session afterwards
* <tt>isat_shell </tt>
** Only recommendet for more experienced linux users.
** opens a bash shell within the container.
** exit with <tt>CMD + D</tt> or <tt>exit</tt>
* <tt>isat_bmc </tt>
** Executes binary <tt>isat_bmc </tt>.
* <tt>isat_probsat_tree_test </tt>
** Executes binary <tt>isat_probsat_tree_test </tt>.
* <tt>parallel_isat --i <input_file> </tt>
** Executes binary <tt>parallel_isat </tt>.
* <tt>sigmoid_prop_test <arguments> <input_file> </tt>
** Executes binary <tt>sigmoid_prop_test </tt>.
* <tt>test_deductions <arguments> </tt>
** Executes binary <tt>test_deductions </tt>.
Naturally, these scripts only work during the time ''fluka/***-Singularity'' is loaded.
== Using iSAT executables==
To find out on how to use the different iSAT binaries, you can call the aid scripts without options to find out if the developers embedded a help function. <tt>isat_bmc</tt> for example, prints out a help message after calling it.
So, after loading the module, call said script to print out a help text to get you started:
<pre>
$ isat_bmc
This is iSAT 0.1.
Usage: isat_bmc --i inputfile
General iSAT options:
--heu=bmc-fwd : BMC forward
bmc-bwd : BMC backward
b-fst : Boolean first
b-lst : Boolean last
int-fst : Integer first
int-lst : Integer last
vsids : VSIDS
You may specify up to four variable ordering heuristics.
The second heuristic will be used to sort the variables
that are equal wrt. the first heuristics, etc.
disc-fst : split all discrete variables down to the msw (normally
thus down to being point-valued) before splitting any
real-valued variable.
dyn-abs-width : Override the given static order and always prefer the
variable with the largest absolute interval width.
dyn-rel-width : Override the given static order and always prefer the
variable with the largest relative interval width.
If both are given, absolute wins over relative.
--msw=[real] : Minimum splitting width of an interval
(must be > 2*prabs, default: 0.01)
--prabs=[real] : Neglect deductions with absolute progress
less than prabs (default: 0.001)
--prrel=[real] : Neglect deductions with relative progress
less than prrel (must be in [0,0.5), default: 0)
--dont-split : Propagate only, never perform a split. This can
be used to find nondeterminism in a model.
--idv=[real] : Set interval divide value
(must be > 1.0, default: 2.0)
--ch-sat-often : Enables a satisfiability check after
each propagation phase
--pspl : Provides point splitting
--purification : Enables purification rule
--restart : Enables restarting
--cont-unknown : Continues search after each UNKNOWN
--preprocessed : Given input formula has already been
preprocessed (e.g. because it is the
output of --export-cldb).
--verify-sol : If a candidate solution box is found by iSAT
it will be analyzed
--split="x y" : Prefer the given list of variables for
splitting, i.e. split these down to the msw
first.
--range="x[1] y[2]" : Instead of normal solver mode, perform
a range estimation on the specified variables
in the given unwinding depth. You can specify
a list of variables with one unwinding depth
each. If you want variable x1 to be range-
estimated on depths 1 and 3, just use a list
like "x[1] x[3]". The depths refer to the
BMC unwinding depths, i.e. are always 0 for
pure EXPR formulae and start at 0 for INIT
instances in BMC mode.
Print options:
--nosol : Solution is not printed
--pdpos=[nat] : Number of post-decimal positions (default: 8)
--export-cldb : Exports the solver core clause DB
BMC-related options:
--start-depth : BMC starting depth (default: 0)
--max-depth : BMC maximal number of unwindings
(default: 2147483647)
Documentation
The manual is provided as a pdf-file. You can find this file here.
