MSAFinder

What is MSAFinder?

MSAFinder is the component of Mistral that can be used to compute minimum satisfying assignments (MSA) of Presburger arithmetic formulas. An MSA of a formula F is a partial satisfying assignment of F that contains as few variables as possible, but is still sufficient to imply the validity of the formula. A precise definition of MSAs as well as the algorithm MSAFinder uses to compute MSAs is described in this paper.

Using MSAFinder

To compute minimum satisfying assignments of Presburger arithmetic formulas, use the msa method provided in Constraint.h. Here is an example code snippet that illustrates how to compute MSAs:

Term* x = VariableTerm::make("x");
Term* y = VariableTerm::make("y");
Term* z = VariableTerm::make("z");

map<Term*, long int> elems1;
elems1[x] = 1;
elems1[y] = 1;
Term* t1 = ArithmeticTerm::make(elems1, 0);

map<Term*, ling int> elems2;
elems2[x] = 1;
elems2[y] = 1;
elems2[z] = 1;
Term* t2 = ArithmeticTerm::make(elems2, 0);

Constraint c1(t1, ConstantTerm::make(0), ATOM_GT);
Constraint c2(t2, ConstantTerm::make(5), ATOM_LT);
Constraint c3 = (c1 | c2);

map<Term*, SatValue> min_assign;
int min_vars = c3.msa(min_assign);
for(auto it = min_assign.begin(); it!= min_assign.end(); it++) {
	Term* t = it->first;
	SatValue sv = it->second;
	cout << t->to_string() << ":" << sv.to_string() << "\t";

}

Here, c3 corresponds to the formula x+y>0 | x+y+z <=5. The return value, min_vars, of the msa method tells us how many variables the MSA of c3 contains, and the map min_assign gives the actual minimum satisfying assignment. The for loop in the above code snippet prints a satisfying assignment for each variable in the msa. In this particular example, the minimum satisfying assignment of c3 contains only one variable, namely z, and an MSA of c3 is z=0.

When computing minimum satisfying assignments, one can also assign a cost to each variable. In this case, the msa method yields a partial satisfying assignment that minimizes the sum of the costs of each variable used in the assignment. For instance, consider the cost function C such that C(x) = 1, C(y) = 1, C(z) = 5. Under this cost function, z= 0 is no longer an MSA of (x+y > 0 | x+y+z <=5 ) because the cost of the assignment z=0 is 5, and there exists a satisfying assignment with smaller cost, such as y= 0 and x=1. The following code snippet shows how to obtain an MSA for c3 subject to a cost function C(x) = 1, C(y) = 1, C(z) =5.

map<VariableTerm*, int> costs;
costs[x] = 1;
costs[y] = 1;
costs[z] = 5;


map<Term*, SatValue> min_assign;
int msa_cost = c3.msa(min_assign, costs);
for(auto it = min_assign.begin(); it!= min_assign.end(); it++) {
	Term* t = it->first;
	SatValue sv = it->second;
	cout << t->to_string() << ":" << sv.to_string() << "\t";

}

For this example, msa_cost is 2 and the MSA is printed as y:0 x:1.