Formula types

Formula types
#define	VallstFormulaType_clause   (VallstLiteral_MAX-1)
#define	VallstFormulaType_equivalence   (VallstLiteral_MAX-5)
#define	VallstFormulaType_negEquivalence   (VallstLiteral_MAX-4)
#define	VallstFormulaType_moreThan   (VallstLiteral_MAX-6)
#define	VallstFormulaType_moreThanDis   (VallstLiteral_MAX-7)
#define	VallstFormulaType_moreThanMult   (VallstLiteral_MAX-8)
#define	VallstFormulaType_ggcdiTour   (VallstLiteral_MAX-9)
#define	VallstFormulaType_erased   (VallstLiteral_MAX-10)

---

Detailed Description

For any formula a you can easily introduce a Tseitin name p for the formula such that p<=>a --- disregarding global types.

Formulas of type >=* and >= aren't supported directly. Instead you have to transform them into <*- and <-formulas. See vallst_lessThanEqMultToMoreThanMult() and vallst_lessThanEqToMoreThan().

(Negated) equivalences will be normalized so that all the literals in them are unnegated. E.g. <->{-p,-q,-r} will be turned into -<->{p,q,r} where p, q and r are variables.

---

Define Documentation

#define VallstFormulaType_clause   (VallstLiteral_MAX-1)

Arbitrary long disjunction, \/{...}. Definition at line 458 of file vallstAPI.h.

#define VallstFormulaType_equivalence   (VallstLiteral_MAX-5)

Arbitrary long equivalence, <->{...} (i.e p1<->p2<->p3<->p4<->...<->pn (saying that an even number of the literals are true if n is even and saying that an odd number of the literals are true if n is odd)). Definition at line 465 of file vallstAPI.h.

#define VallstFormulaType_erased   (VallstLiteral_MAX-10)

Marks that the formula has been erased. Although you can't use this type directly, you might still encounter this type because formulas can be erased by vallst. Say e.g. that you have named an axiom b which later gets erased by vallst (e.g. because it's simplified away or recognized to be subsumed). Then you have a name of an erased axiom and if you e.g. call vallst_formulaType() with the name you will get VallstFormulaType_erased back. Definition at line 581 of file vallstAPI.h.

#define VallstFormulaType_ggcdiTour   (VallstLiteral_MAX-9)

The meaning of the global axiom type VallstFormulaType_ggcdiTour is that any solution interpreted as nodes and edges in a complete directed irreflexive graph, assuming a canonical coding, must be a tour (i.e. a Hamiltonian cycle (visiting every node in the graph)). This formula type only covers the non-local part of formulas stating that the solution is a tour. Accompanying this formula must be the concluding local part. Otherwise the meaning and behaviour of the solver is undefined. Here is an example that will clear things up: Suppose that you have a problem involving a complete directed irreflexive graph with n nodes 0,1...n-1. n is the dimension (dim) and the graph has n*(n-1) edges. Suppose that any solution to the problem must result in a tour of the graph; confer the asymmetric traveling salesperson problem, atsp. Let the graph be coded by variables p(i,j) with i!=j, i<n and j<n. p(i,j) will be true iff the edge (i,j) in the graph will be used in the solution. Assume that in actual fact p(i,j) will be represented by vallst literals q, q+2, q+4... where q is some offset start vallst literal, e.g. 2. q may be odd. If q is 2 then let edge (0,1) be represented by vallst variable 2, (0,2) by 4, (0,3) by 6, (1,0) by 2*((n-1)+1), (1,2) by 2*((n-1)+2), (2,0) by 2*(2*(n-1)+1)... The local part of formulas saying that a solution must be a tour says that each node has at most 1 in-edge and 1 out-edge, and at least 1 in-edge and 1 out-edge: for all i<n, n-3 < +{-p(i,j): j!=i, j<n} for all i<n, n-3 < +{-p(j,i): j!=i, j<n} for all i<n, \/{p(i,j): j!=i, j<n} for all i<n, \/{p(j,i): j!=i, j<n} Then if you add a non-local tour axiom with vallst literal start q and with dimension n, you are ensured that any solution is a tour. The call to vallst_addAxiom() would be vallst_addAxiom( vi, [q,n], 2, VallstFormulaType_ggcdiTour ). As said, the tour type assumes the canonical coding of the graph described above. For a further definition of the canonical coding and utilities, see the macros vallst_ggcditEdgeToLit() and vallst_ggcditLitToEdge() (where dim is n above). Definition at line 569 of file vallstAPI.h.

#define VallstFormulaType_moreThan   (VallstLiteral_MAX-6)

Arbitrary long constraint on the form c < p+q+r+..., where c is a constant. I.e. the formula says that at least c+1 of p,q,... should be true. With c=0, the formula is equivalent to a disjunction and it's slightly more efficient to use the clause form. Note though that there can be good reasons for using c=0, namely in cases where you later on might want to increase the constant. See vallst_lessThanEqToMoreThan() for transforming a >=-formula into a <-formula. Definition at line 483 of file vallstAPI.h.

#define VallstFormulaType_moreThanDis   (VallstLiteral_MAX-7)

For formulas p\/a where a is of more-than type. With this type you can Tseitin name more-than formulas without using more-than-mult: Let a be c < q0 + .. + qn. Then p <=> a is equivalent to -p \/ a and p \/ -a where -a can be expressed as n-c < -q0 + ... + -qn. Having more-than-dis means that the more-than type isn't strictly necessary. However, using more-than rather than more-than-dis when possible is a little bit more efficient and transparent. Note that if you are looking for a p \/ /\{q0,...,qn} formula type you can use more-than-dis with c=n, i.e. p \/ n<q0+...+qn. Definition at line 496 of file vallstAPI.h.

#define VallstFormulaType_moreThanMult   (VallstLiteral_MAX-8)

Arbitrary long constraint on the form c < d0*p0 + d1*p1 + ... where c and di are constants. A Tseitin name p for a more-than-mult formula a = c < +{di*pi} can be defined like this: q \/ a <=> c < +{di*pi} + (c+1)*q. Also, +{di} = +{di*pi} + +{di*-pi}. Hence, -a <=> c >= +{di*pi} <=> c >= +{di} - +{di*-pi} <=> +{di*-pi} >= +{di} - c <=> +{di}-c-1 < +{di*-pi}. Therefor p <=> a can be expressed by translating -p \/ a and p \/ -a. See vallst_lessThanEqMultToMoreThanMult() for transforming a >=*-formula into a <*-formula. Negative constants are not allowed. You can transform negative literal constants like this: c < ... + -d*p + ... <=> c+d < ... + d*-p + ... If the formula is very long you might want to input d0, d1,... in increasing order since internally they will be sorted that way using an algorithm which is fast on already increasing formulas but which might be slow on non-increasing formulas. Excessive variable constants, as in e.g. 3 < 9*p + 7*q + 5*r + ..., are allowed and could be useful if you plan on incrementing the main constant, 3, later on (see vallst_addNamedAxiom() and axiom altering functions). Though, rather than using excessive constants you might want to use vallst_alterAxiomIncMTMKeepAboves() instead. Examples: vallst.c. Definition at line 524 of file vallstAPI.h.

#define VallstFormulaType_negEquivalence   (VallstLiteral_MAX-4)

Arbitrary long negated equivalence (xor), -<->{...} (i.e -(p<->q<->r<->s<->...)). Definition at line 469 of file vallstAPI.h.

---