I need to optimise terms for solution existence checks by sorting the term clauses. (They are in CNF and OR clauses do not need to be considered atm) I'm currently sorting them by the most common variable and i'm adding clauses always, when all variables of this clause are already bound by an earlier clause. The term itself is designed like this: (pred1,(pred2,(pred3,pred4))) But i still have alot useless backtracking. The solver changes/bindes variables that have nothing to do with the current failing clause. Therefore, i'm interested how exactly the solver works. In which order are variables bound ? How get's the term tree parsed ? Who is the next variable for a backtracking change determined ?Received on Wed Apr 07 2010 - 12:33:29 CEST
This archive was generated by hypermail 2.2.0 : Thu Feb 02 2012 - 02:31:58 CET