[eclipse-clp-users] Backttacking optimisation

From: Christian Wirth <tyrion_at_...215...>
Date: Wed, 07 Apr 2010 14:33:20 +0200
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.3.0 : Tue Apr 16 2024 - 09:13:20 CEST