Recent developments in SAT solvers and model checkers have allowed supposedly exponential-time problems to be solved and checked in practice. Here we suggest that a new tool is needed for system synthesis: The SSMG, (Sequential Symbolic Model Generator) finds solutions to problems phrased in terms of next state functions.
Most SAT solvers require CNF input, but converting to this leads to an explosion of terms in itself. Certain SAT solvers can accept arbitrary logic expressions, such as the one from prover.com (Stalmark) or those based on the method of [GIU99]. However, when we consider projection through the next state function, as implemented in our HPRLS project, another form of exponential blow-up is experienced.
What is required for our approach to system synthesis is a SAT-like solver, that generates solutions, but where the problem is phrased in terms of a number of free (or partially constrained) variables and their nth-power next state functions. The solution is valid for all settings of the free variables. This problem lies between SAT and generalised QBF (quantified boolean formula) problems.
SSMG is a program that accepts the following input:
Hence, its input is rather like that of a model checkers except for the presence of the list X of fuse variables. The job of SSMG is to find a setting of the fuse variables such that the assertions, A, are all always satisfied. SSMG input can either be an extended DIMACS file or in the form of basic ASCII declarations and logic equations.
SSMG can be used without next-state declarations, D, as a basic combinational SAT solver. Even without referring to the next-state of variables, our DIMACS extensions allow two new classes of variable to be defined. Firstly, we allow the user to list variables that cannot be the basis of a useful case split. Secondly, we allow the user to list variables that must be universally quantifed. An existential solution found for the remaining variables (SAT solution) must be valid for all settings of the universally quantifed variables. Finally, one does not have to use CNF or DIMACS at all because the equation form of input can be used.
A conventional model checker cannot be used to generate this solution by handing it the negation of A, since the counter example it produces will be valid for only one setting of F, whereas the SSMG generates a solution that satisfies A for all settings of F.
The BV1 implementation of SMGG will be described in the white paper HERE. The SAT part of this implementation uses a Davis-Putman core where case splits are selected by a small set of heuristics. Input is in the form of simple equations, or CNF if used purely as a SAT solver. Output is either a counter-example or a fuse mapping, expressed using simple XML. Mature sat-solver techniques, such as non-linear backtracking and recursive learning can be applied in future.
The DIMACS CNF input file supports a couple of extensions to facilitate input from external tools that support universal quantification in their conversion to CNF.
A relation D is formed, that relates the current and next states D(q, q'). D typically contains most of the sat fuses whose value we must find, but equally these may occur in I or A.
We use the following procedure to generate the model:
The program is run from the command line and is normally called `ssmg' and this should be followed by any options and then the source file name.
ssmg [ options ] srcfilename
Example CNF run
$ ./ssmg -o spool -c /homes/djg/bcd/hgen5-v100-s2029002754.cnf
CBG SSMG Version BV1.12
CNF input: Found 0 unit clauses, 709 non-trivial clauses
dp starting
******** FOUND
Solution found ok
Checker: 709 satisifed clauses out of 709. 79 fuses unbound.
The output file is in XML format. Here is an example example output. Only one solution is returned. The algorithm we use can result in a fuse being set to 0, 1 or X, although there is no guarantee that all possible X's are included in the result. There were 79 unset fuses in this example solution.
The '-o fn' command line option causes output to be written to a file. Without this the output is to the screen.
The '-v' command line flag causes verbose output. Capital V is more verbose still.
The '-c' command line flag causes the input file to be read as a standard CNF file instead of being parsed by yacc in the expression language.
The sets X and F of variables may be defined by default rules or by declarations in the input file. The default rules are that any variable that begins with 'x' defaults to being a fuse variable. Any other variable that is not given an initial value or a next state function is a free initially or thereafter respectively. External inputs to the system are modelled in this way.
The '-x' command line flag allows one to change the default prefix for sat fuse variables. The default is that all variables begining with 'x' must be found values that make all of the model properties hold. However, '-x doh' would cause all variables begining with 'doh' to become sat fuses instead.
A standard DIMACS CNF file contains a line
p cnf atoms clausesfollowed by the CNF data. Such data can be solved for SAT by SSMG, and so SSMG can be used as a normal sat solver.
We extend the CNF file format by allowing a number of the atoms to be considered to be universally quantified instead of solved for. These atoms are denoted by listing them on a line that starts with the letter U and ends with a zero. For example:
U 10 11 22 33 66 102 0
This is not be very useful for a normal SAT solver since one can normally miss out these atoms from all the clauses instead. It does make one difference in the case of a clause that is a trivial tautology. Specifically, if a clause contains both x and -x and x is then listed under U, the remainder of the tautological clause is exposed to influence the solution.
We also extend the CNF file format to allow a number of the atoms to be declared as `non-fuse' meaning they should not be used as the basis for a DP case split. There are two aspects two this. Firstly, where an intermediate variable is introduced during CNF conversion, then as reported in [GIU99], it is unneccesasry to consider such new variables during case split. For example
(A + B.C)can be converted to CNF while preserving satisfiability as
(A + Y)(~Y + B)(~Y + C)but there is no need to do a case split on the new variable Y.
Secondly, where a universally quantified variable is below the new variable Y, then Y needs to become a Skolem function. For example
\Ax.(A + x.C)requires Y(x) to be introduced
\Ax.\Ey.(A + y)(~y + x)(~y + C) = \Ax.(A + Y(x))(~Y(x) + x)(~Y(x) + C)If Y(x) is represented in the CNF file as just another literal, it is wrong to do a case split on that literal, since its value cannot be forced independently of other literals in the file.
Therefore, we introduce a second extension to the CNF file that allows such skolem literals to be identified and to be excluded as case split targets:
S 122 366 121 0these literals are only used for resolution eliminations.
Non-CNF input must use the following syntax:
Comments are introduced with double slash
// This is a comment
Initial values of variables are given by assigning to I(x). More general starting conditions are introduce using the 'initial' statement.
I(variable) := exp; initial exp;
Next state functions are given by assigning to X(x).
X(variable) := exp;
The only CTL quantifier implemented at the moment is `AG', meaning that all properties must hold along all paths leading to all reachable states. This is the only one I currently need.
Rather than using the string 'AG', model constraints are introduced with always or never and are true for the initial states and all reachable states. The two statements are interchangable by negating the expression. The conditions required to be true only in the initial state are introduced by any number of initial statements.
always exp; never exp; initial exp;
Macro or intermediate style definitions are given by assigning to a macro variable name
myvar := exp;
Boolean expressions may use the following operators with binding powers given on this page:H1OPERATORS.
~ ^ == != | & && || ! \/ /\ => <=>
Variables that are not assigned are assumed to be external inputs, free to change on any step, unless they start with the letter 'x' (or other string given on the command line).
Universal quantification is implied by default for all unconstrained values: i.e. the model generated must be true for all possible unconstrained initial value and external input patterns.
Lab members can copy a snapshot zip file release from my directory d310/hprls/ssmg/bv1/ssmg.zip. Externals, please send me an email.
[GIU99] Applying the Davis-Putnam procedure to non-clausal formulas. (1999) Enrico Giunchiglia, Roberto Sebastiani Lecture Notes in Computer Science
March 07: This page is under construction. SSMG is now part of the H2 tool. See there for more info: LINK.
(C) March 2006 DJ Greaves.