Project

General

Profile

Actions

Bug #514

closed

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

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

Status:
Closed
Priority:
High
Assignee:
Category:
-
Target version:
Start date:
10/30/2010
Due date:
% Done:

0%

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

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 open1 closed)

Related to BLAST - Bug #566: Useful block sets are SAT on some of generic test driversClosedPavel Shved11/16/2010

Actions
Actions

Also available in: Atom PDF