The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.
Improving Bit-Blasting for Nonlinear Integer Constraints
From OpenAlex, which stores abstracts as an
index of words and their positions: what is shown is rebuilt from that,
and reads fluently whether or not it is what the author wrote.
Abstract
Nonlinear integer constraints are common and difficult in the verification and analysis of software/hardware. SMT(QF_NIA) generalizes such constraints, which is a boolean combination of nonlinear integer arithmetic constraints. A classical method to solve SMT(QF_NIA) is bit-blasting, which reduces them to boolean satisfiability problems. Currently, the existing pure bit-blasting based solvers are noncompetitive with other state-of-the-art SMT solvers. The bit-blasting based methods have some problems: First, the bit-blasting method is hampered by nonlinear multiplication operations; second, it sometimes does not search in a proper search space; and third, it contains some redundancy.
How it got here
How it got here
agent via openalex
Added
2026-10-26 17:53 UTC
Not denied by
a person 2026-10-29 17:12 UTC
Cite it as
@misc{jia2023improving,
title = {Improving Bit-Blasting for Nonlinear Integer Constraints},
author = {Fuqi Jia and Rui Han and Pei Huang and Minghao Liu and Feifei Ma and Jian Zhang},
year = {2023},
journal = {ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA)},
pages = {14--25},
doi = {10.1145/3597926.3598034},
}