About: Reducing Bit-Vector Polynomials to SAT using Gröbner Bases

Not logged in : Login

(Sponging disallowed)

Facets (new session)
Description
Metadata
Settings
- Rule:
- Inverse Functional Properties:
- "Same As":

About: Reducing Bit-Vector Polynomials to SAT using Gröbner Bases Goto Sponge NotDistinct Permalink

An Entity of Type : bibo:BookSection, within Data Space : linkeddata.uriburner.com:28898 associated with source document(s)

Attributes	Values
type	http://eprints.org/ontology/BookSectionEPrint http://eprints.org/ontology/EPrint Article Book Section
seeAlso	HTML Summary of #81001 Reducing Bit-Vector Polynomials to SAT using Gröbner Bases
sameAs	Reducing Bit-Vector Polynomials to SAT using Gröbner Bases
http://www.loc.gov...erms/relators/EDT	Lusa Pulina Seidl Martina
http://eprints.org/ontology/hasDocument	Reducing Bit-Vector Polynomials to SAT using Gröbner Bases (PDF) Reducing Bit-Vector Polynomials to SAT using Gröbner Bases (Other) Reducing Bit-Vector Polynomials to SAT using Gröbner Bases (Other) Reducing Bit-Vector Polynomials to SAT using Gröbner Bases (Other) Reducing Bit-Vector Polynomials to SAT using Gröbner Bases (Other) Reducing Bit-Vector Polynomials to SAT using Gröbner Bases (Other)
Title	Reducing Bit-Vector Polynomials to SAT using Gröbner Bases
described by	https://demo.openlinksw.com/about/id/entity/https/raw.githubusercontent.com/annajordanous/CO644Files/main/export_kar_RDFN3.n3
Date	2020-07-05
Creator	Neil Evans Andy King Thomas Seed
status	peer reviewed published
Publisher	Springer
abstract	We address the satisfiability of systems of polynomial equations over bit-vectors. Instead of conventional bit-blasting, we exploit word-level inference to translate these systems into non-linear pseudo-boolean constraints. We derive the pseudo-booleans by simulating bit assignments through the addition of (linear) polynomials and applying a strong form of propagation by computing Gröbner bases. By handling bit assignments symbolically, the number of Gröbner basis calculations, along with the number of assignments, is reduced. The final Gröbner basis yields expressions for the bit-vectors in terms of the symbolic bits, together with non-linear pseudo-boolean constraints on the symbolic variables, modulo a power of two. The pseudo-booleans can be solved by translation into classical linear pseudo-boolean constraints (without a modulo) or by encoding them as propositional formulae, for which a novel translation process is described.
Is Part Of	https://kar.kent.ac.uk/id/repository
Subject	QA Mathematics (inc Computing science)
list of authors	https://kar.kent.ac.uk/id/eprint/81001#authors
list of editors	https://kar.kent.ac.uk/id/eprint/81001#editors
volume	12178
is topic of	https://raw.githubusercontent.com/annajordanous/CO644Files/main/export_kar_RDFN3.n3
is primary topic of	HTML Summary of #81001 Reducing Bit-Vector Polynomials to SAT using Gröbner Bases

Faceted Search & Find service v1.17_git144 as of Jul 26 2024

Alternative Linked Data Documents: iSPARQL | ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 08.03.3331 as of Aug 25 2024, on Linux (x86_64-ubuntu_noble-linux-glibc2.38-64), Single-Server Edition (378 GB total memory, 15 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software