solver/simplex.h
00001 /*
00002  * simplex.h
00003  *
00004  *  Created on: Aug 26, 2008
00005  *      Author: isil
00006  */
00007 
00008 #ifndef SIMPLEX_H_
00009 #define SIMPLEX_H_
00010 
00011 #include "bigfraction.h"
00012 #include "Matrix.h"
00013 #include "time.h"
00014 #include <vector>
00015 class slack_matrix;
00016 
00017 /*
00018  * lp_sat determines the satisfiability of a system Ax <= b using
00019  * the Simplex algorithm. If no satisfying assignment is desired,
00020  * pass NULL for sat_assign.
00021  */
00022 
00023 bool lp_sat(Matrix & m, vector<bigfraction>* sat_assign, bool verbose);
00024 bool verify_solution(Matrix& m, vector<bigfraction>& assignments);
00025 
00026 bool lp_sat_internal(slack_matrix & sm, vector<bigfraction>* sat_assign,
00027                 bool verbose, int *fraction_result_index);
00028 bool is_trivially_sat(Matrix & m);
00029 void set_trivial_solution(vector<bigfraction> & fa, int num_vars);
00030 
00031 
00032 
00033 
00034 #endif /* SIMPLEX_H_ */