Wombit

a portfolio bit-vector solver using word-level propagation

Wenxi Wang, Harald Søndergaard, Peter J. Stuckey

Research output: Contribution to journalArticleResearchpeer-review

1 Citation (Scopus)

Abstract

We develop an idea originally proposed by Michel and Van Hentenryck of how to perform bit-vector constraint propagation on the word level. Most operations are propagated in constant time, assuming the bit-vector fits in a machine word. In contrast, bit-vector SMT solvers usually solve bit-vector problems by (ultimately) bit-blasting, that is, mapping the resulting operations to conjunctive normal form clauses, and using SAT technology to solve them. Bit-blasting generates intermediate variables which can be an advantage, as these can be searched on and learnt about. As each approach has advantages, it makes sense to try to combine them. In this paper, we describe an approach to bit-vector solving using word-level propagation with learning. We have designed alternative word-level propagators to Michel and Van Hentenryck’s, and evaluated different variants of the approach. We have also experimented with different approaches to learning and back-jumping in the solver. Based on the insights gained, we have built a portfolio solver, Wombit, which essentially extends the STP bit-vector solver. Using machine learning techniques, the solver makes a judicious up-front decision about whether to use word-level propagation or fall back on bit-blasting.

Original languageEnglish
Pages (from-to)723-762
Number of pages40
JournalJournal of Automated Reasoning
Volume63
Issue number3
DOIs
Publication statusPublished - Oct 2019

Keywords

  • Bit-blasting
  • Bit-vector solver
  • Constraint propagation
  • Machine learning
  • Portfolio solvers
  • Word-level reasoning

Cite this

Wang, Wenxi ; Søndergaard, Harald ; Stuckey, Peter J. / Wombit : a portfolio bit-vector solver using word-level propagation. In: Journal of Automated Reasoning. 2019 ; Vol. 63, No. 3. pp. 723-762.
@article{794eb11dde744f6b96e1f8df61d67559,
title = "Wombit: a portfolio bit-vector solver using word-level propagation",
abstract = "We develop an idea originally proposed by Michel and Van Hentenryck of how to perform bit-vector constraint propagation on the word level. Most operations are propagated in constant time, assuming the bit-vector fits in a machine word. In contrast, bit-vector SMT solvers usually solve bit-vector problems by (ultimately) bit-blasting, that is, mapping the resulting operations to conjunctive normal form clauses, and using SAT technology to solve them. Bit-blasting generates intermediate variables which can be an advantage, as these can be searched on and learnt about. As each approach has advantages, it makes sense to try to combine them. In this paper, we describe an approach to bit-vector solving using word-level propagation with learning. We have designed alternative word-level propagators to Michel and Van Hentenryck’s, and evaluated different variants of the approach. We have also experimented with different approaches to learning and back-jumping in the solver. Based on the insights gained, we have built a portfolio solver, Wombit, which essentially extends the STP bit-vector solver. Using machine learning techniques, the solver makes a judicious up-front decision about whether to use word-level propagation or fall back on bit-blasting.",
keywords = "Bit-blasting, Bit-vector solver, Constraint propagation, Machine learning, Portfolio solvers, Word-level reasoning",
author = "Wenxi Wang and Harald S{\o}ndergaard and Stuckey, {Peter J.}",
year = "2019",
month = "10",
doi = "10.1007/s10817-018-9493-1",
language = "English",
volume = "63",
pages = "723--762",
journal = "Journal of Automated Reasoning",
issn = "0168-7433",
publisher = "Springer-Verlag London Ltd.",
number = "3",

}

Wombit : a portfolio bit-vector solver using word-level propagation. / Wang, Wenxi; Søndergaard, Harald; Stuckey, Peter J.

In: Journal of Automated Reasoning, Vol. 63, No. 3, 10.2019, p. 723-762.

Research output: Contribution to journalArticleResearchpeer-review

TY - JOUR

T1 - Wombit

T2 - a portfolio bit-vector solver using word-level propagation

AU - Wang, Wenxi

AU - Søndergaard, Harald

AU - Stuckey, Peter J.

PY - 2019/10

Y1 - 2019/10

N2 - We develop an idea originally proposed by Michel and Van Hentenryck of how to perform bit-vector constraint propagation on the word level. Most operations are propagated in constant time, assuming the bit-vector fits in a machine word. In contrast, bit-vector SMT solvers usually solve bit-vector problems by (ultimately) bit-blasting, that is, mapping the resulting operations to conjunctive normal form clauses, and using SAT technology to solve them. Bit-blasting generates intermediate variables which can be an advantage, as these can be searched on and learnt about. As each approach has advantages, it makes sense to try to combine them. In this paper, we describe an approach to bit-vector solving using word-level propagation with learning. We have designed alternative word-level propagators to Michel and Van Hentenryck’s, and evaluated different variants of the approach. We have also experimented with different approaches to learning and back-jumping in the solver. Based on the insights gained, we have built a portfolio solver, Wombit, which essentially extends the STP bit-vector solver. Using machine learning techniques, the solver makes a judicious up-front decision about whether to use word-level propagation or fall back on bit-blasting.

AB - We develop an idea originally proposed by Michel and Van Hentenryck of how to perform bit-vector constraint propagation on the word level. Most operations are propagated in constant time, assuming the bit-vector fits in a machine word. In contrast, bit-vector SMT solvers usually solve bit-vector problems by (ultimately) bit-blasting, that is, mapping the resulting operations to conjunctive normal form clauses, and using SAT technology to solve them. Bit-blasting generates intermediate variables which can be an advantage, as these can be searched on and learnt about. As each approach has advantages, it makes sense to try to combine them. In this paper, we describe an approach to bit-vector solving using word-level propagation with learning. We have designed alternative word-level propagators to Michel and Van Hentenryck’s, and evaluated different variants of the approach. We have also experimented with different approaches to learning and back-jumping in the solver. Based on the insights gained, we have built a portfolio solver, Wombit, which essentially extends the STP bit-vector solver. Using machine learning techniques, the solver makes a judicious up-front decision about whether to use word-level propagation or fall back on bit-blasting.

KW - Bit-blasting

KW - Bit-vector solver

KW - Constraint propagation

KW - Machine learning

KW - Portfolio solvers

KW - Word-level reasoning

UR - http://www.scopus.com/inward/record.url?scp=85056335383&partnerID=8YFLogxK

U2 - 10.1007/s10817-018-9493-1

DO - 10.1007/s10817-018-9493-1

M3 - Article

VL - 63

SP - 723

EP - 762

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

SN - 0168-7433

IS - 3

ER -