pstlab / oRatio

oRatio is an Integrated Logic and Constraint based solver
Apache License 2.0
6 stars 1 forks source link

Tableau pivoting performance issue #2

Closed riccardodebenedictis closed 6 years ago

riccardodebenedictis commented 6 years ago

Most of the time (>85%) of a standard resolution process is spent in performing pivoting operations. Until better strategies are found, which would minimize the need of such operations, it could be worth to optimize them.

A tableau data structure, with the following characteristics, should be introduced:

Notice that pivoting operations can be parallelized, further enhancing efficiency!

riccardodebenedictis commented 6 years ago

the pivoting procedure has been enhanced resulting in more than 50% performance improvement. parallelizing the pivoting procedure results in too much time: the thread creation does not seam to worth the parallelization..