Bug #514: BLAST's useful blocks generation algorithm is suboptimal for SMT solvers - BLAST - Open-Source Projects

Actions

Copy link

Bug #514

closed

BLAST's useful blocks generation algorithm is suboptimal for SMT solvers

Added by Pavel Shved about 14 years ago. Updated about 13 years ago.

Status:

Closed

Priority:

High

Assignee:

Pavel Shved

Category:

Target version:

2.6

Start date:

10/30/2010

Due date:

% Done:

Estimated time:

Detected in build:

any

Platform:

Published in build:

9c0646f

Description

One of the core tasks in the useful-blocks algorithm is to find the first i such that conjunction of predicates from 1 to i is UNSAT.

For incremental solvers it was OK to push predicates one-by-one, anbd check for satisfiability. But for SMTlib solvers it's suboptimal. An algorithm that employs some kind of binary search and works in a logarithmic number of calls to solvers could—oh, no, should—be much faster.

We need to carefully design and implement it.

Files

Download all files

before_ub_profile_short (1.21 KB) before_ub_profile_short	reduced cxusb profile BEFORE useful-blocks fix	Pavel Shved, 11/16/2010 03:40 PM
after_ub_profile_short (2.11 KB) after_ub_profile_short	reduced cxusb profile AFTER useful-blocks fix	Pavel Shved, 11/16/2010 03:40 PM

Related issues 1 (0 open — 1 closed)

Actions

Copy link

Updated by Pavel Shved about 14 years ago

Logarithmic algorithm was implemented, and it resides on our development server in branch useful-blocks-fix. It demonstrated performance improvement, although most time seems to be taken by processing of initialization block (see #511).

As soon as tests on my machine finish, I'll merge the fix to the ldv-tools main branch.

Actions

Copy link Download all files

Updated by Pavel Shved about 14 years ago

File before_ub_profile_short before_ub_profile_short added
File after_ub_profile_short after_ub_profile_short added
Status changed from New to Resolved
Published in build set to 9c0646f

As a result of this optimization, for example, on cxusb driver, the number of calls to SMT solver reduced from 32630 to 831, and the overall time is 7 times less than it was before (10 times less if you count BLAST exclusively).

Attached to the post are a couple of [shortened] profiles of analysis of a cxusb driver with iteration limit. Other than in runtime, the launches differ in nothing else.

The fixes are now merged into master, and reside in commit:9c0646f.

Actions

Copy link

Updated by Evgeny Novikov almost 14 years ago

This should be closed?

Actions

Copy link

Updated by Pavel Shved almost 14 years ago

I wouldn't actually close it before we resolve bug #566 and/or make another full-kernel run with analysis of all the errors appeared. Let it hang for a while.

Actions

Copy link