| Home |
| Download |
| vallstAPI.h |
| API functions |
| Manual |
| Forums |
| Donate |
The solver will find a satisfying assignment to the variables, making all formulas true, or prove that there is no satisfying assignment.
(Confer 0-1 integer programming (0-1 ILP), pseudo-boolean constraints, propositional satisfiability (SAT)).
You can also tell the solver to maximize or minimize constraint constants.
Moreover there are "global" formula types available such as the tour type with the intended meaning that a solution corresponding to nodes and edges in a complete directed irreflexive graph must be a tour (i.e. a Hamiltonian cycle). This is useful for more efficient coding and solving of e.g. asymmetric traveling salesperson problems.
Vallst is available both as an API, see vallstAPI.h, and in a standalone, command line based, version.
Vallst is distributed under the open source license RPL. (Informally, RPL is roughly like GPL but stricter; you are not allowed to use (e.g. link) RPLed programs within a company without making your work available.) For a copy of the whole license, including vallst's EXHIBIT A section, see LICENSE. (For more on open source, see http://www.opensource.org.)Or you might prefer to use vallst under an alternativ commercial license instead.
If you don't do a "make install" and still want to use the scripts, you probably need to redefine the variable vallstcom at the top of the scripts that you want to use. Set it to "vallstcom=/dir/vallst" where dir is the full path of the directory where you installed the solver.
The API is fast, reentrant, supports incremental use, supports temporary assumptions, supports axiom strengthening, etc.
The intentions are to maintain vallst to be as fast and robust as possible, improving it by implementing any new good ideas, and to include into the API any useful functionality.
There is a short paper available giving an overview of some of the algorithms behind the solver.
Symmetry (automorphism) detection isn't implemented yet. However, there is an outline of an implementation and it will be implemented within a few month or so.
It might very well be possible to relatively easily improve the important branching heuristic for the search. At the moment, basically the branching variable is just taken randomly from the last open formula (akin to part of the heuristic in Berkmin).
Here is an example to illustrate the point: Suppose that we want to solve the asymmetric traveling salesperson problem, atsp. A way to code the problem is to represent each edge (i,j) by a variable p(i,j) which is true iff the edge (i,j) is to be part of the tour. Then the goal is to minimize the sum of all edges. To ensure that the solution is a tour one can add that each node must have at most 1 in-edge and 1 out-edge, and at least 1 in-edge and 1 out-edge. However, that's not enough since a tour is not guaranteed. A solution with many cycles would be permissible, e.g. 0->1->0, 2->3->2. AFAIK it's not possible to express that the solution must be a tour in an optimal way (i.e. quadratic in the number of nodes) using some limited ("local"?) language. What one can do is to simply introduce a new "global" type saying that, given the (local) atsp situation described above, the solution must code a tour. This is what is done in vallst, see VallstFormulaType_ggcdiTour. With this new type one would be able to code the problem optimally and the prover can also solve the problem in a good way.
Now the question arise which problems could be useful to solve with vallst and which formula types that should be added. Admittedly, attacking (a)tsp with vallst might not have been the smartest choice since the methods used by usual tsp solvers obviously seem better suited to solve tsp than the methods used in vallst (at least currently). There are some impressive and intimidating results like a proved optimal tour for all cities in Sweden, about 25k cities, and a close to optimal tour for all cities in the world. But as an example, a proof of concept, the adding of a special tour type in vallst works fine. And there are many problems where the methods used by vallst are the best suited.
Maybe one should convert the recursive sorting function into an iterative one. You can also avoid the segfault by enlarging the stack size (e.g. by 'ulimit' under linux; 'unlimit' under solaris).
If you did a "make install" anyone ought to be able to #include vallstAPI.h and link to the API with the compiler option -lvallst.
Other input formats can also be read. See Traveling salesperson problem and Pseudo boolean input format.
c This is a comment. cv [<nrOf3Clauses> [<nrOfLitOccs>]] p [nrOfVars] [optional text that will be skipped]
There is usually no need to include prologues. If you don't, vallst will if possible read the file an extra time, before the actual parse phase, to estimate prologue values. Even if you supply a prologue, vallst will ignore it if the --ignore-prologue flag is true, which it is by default. See Vallst prologue for more.
Variables are written 1, 2, 3... Negated variables are written -1, -2, -3,... Note that this is in contrast to the API/internal representation of literals where the nth variable is 2n and its negation is 2n+1.
Here are examples of axioms:
c Clause 1 \/ -2 \/ 4 1 -2 4 0
'0' marks the end of a formula (formulas don't have to be contained to one line).
Constraints are written like "< c p0 p1 p2 ... 0" meaning that more than c of p0, p1, ... must be true. Example:
c More than 1 of 2, 3 and -6 must be true, i.e. 1 < '2'+'3'+'-6': < 1 2 3 -6 0
c 3 < 4*'2' + 3*'3' + 1*'-6': <* 3 4 2 3 3 1 -6 0
c More-than disjunction: c '5' \/ 1 < '-2'+'4'+'7'+'9' <\/ 5 1 -2 4 7 9 0
c <->{ -8, 9, 10, 11 } (i.e -8<->9<->10<->11)
c (This says that an even number of the literals are true.)
c (If there are an odd number of literals, an odd number of them must be true.)
<-> -8 9 10 11 0
c -<->{ 12, 13, -14 }
xor 12 13 -14 0
The following types of constraints are also allowed and will be transformed into their equivalent constraints using <* and <. Below, p, q,... are numbers, possibly negated.
c 3 >= 2p+3q+1r >=* 3 2 p 3 q 1 r c 2 >= p+q+r >= 2 p q r
You can also tell vallst to optimize things as e.g. in:
c Maximize the constraint constant c, c >= 4, s.t. c < 3p + 7q + 2r + 1s. <* max 4 3 p 7 q 2 r 1 s
There are also non-local (Global) formula types. This one --- together with its complementing local part --- says that literals representing edges in a Graph with n nodes where the graph is Complete, Directed and Irreflexive should constitute a tour (visiting all nodes in the graph).
c Any solution must be a tour. q is the first literal representing an edge, c e.g. 1 or -2. n is the number of nodes in the graph (the dimension (dim)). ggcdit q n
There are three comment types with special meaning. These three special comments --- cva, cvn and cve --- have their special meaning only in the body, not in the prologue (including any part above the prologue).
Axioms and consequences: "cva" and "cvn" toggles between axioms and non-axioms. For example:
p -1 3 6 0 c This is an axiom by default. cvn Formulas below this comment are non-axioms (consequences of the axioms). 2 5 -6 0 c This is a non-axiom. 4 5 -9 0 c This is a non-axiom too. cva Formulas below this comment are axioms. 1 2 -3 0 c Axiom. 2 7 -9 0 c Axiom. ...
Variable definitions: There is also a special comment to define historic equivalences between variables:
c Peripheral historic literal equivalences: 2<->-2113; 3<->337; 4<->337 cve -2113 2 337 3 337 4
Note that if you use a global formula type, that type covers a range of variables which therefor in effect occur in formulas. Hence you shouldn't use a cve definition "cve r p" to define an equivalence p<->r if p is covered by a global type.
If a model is printed, what is printed will be an expanded model where also the cve definitions hold.
You can use a cve definition "cve r p" even if p occurs in formulas but then you must have a theory that entails the equivalence of r and p (e.g. have an axiom r<->p). And then the point of the cve definition "cve r p" is lost.
The --tsp option specifies that the input file is a tsp problem. Actually, the implementation of support for tsp is currently not finished! (But support for atsp is.)
If the input file name ends with .atsp or .tsp, it is assumed that the problem is an atsp respectively a tsp and the --atsp or --tsp command line option won't be necessary.
If the input file name ends with .opb or .pb, it is assumed that the problem is a pb problem and the --pb command line option won't be necessary.
The pb-problem will be converted to the internal format. A kink is that min: +{c_i*p_i} will be transformed into (max) 0 < +{c_i*-p_i}. Hence, if all models are such that p_i need to be true, no models will be found. If this scenario could actually be possible, you need to take care of it. This problem is automatically taken care of if you use the script vallstSAT2005PB.sh (and you can look at vallstSAT2005PB.sh for one way of handling this).
There is also vallstlocal.sh. If you haven't installed vallst globally (using make install), you could use vallstlocal.sh, perhaps after modifying it.
If you are optimizing you might prefer to use vallstSAT2005PB.sh. (If you are using ordinary, non-pb, files you can add the option --pb=no.)
Generated on Mon Jul 18 11:34:14 2005 for Vallst by doxygen 1.4.3.