About: Manthan: A Data-Driven Approach for Boolean Function Synthesis

Facets (new session)
Description
Metadata
Settings
- owl:sameAs
- Inference Rule:

About: Manthan: A Data-Driven Approach for Boolean Function Synthesis Goto Sponge NotDistinct Permalink

An Entity of Type : schema:ScholarlyArticle, within Data Space : wasabi.inria.fr associated with source document(s)

Attributes	Values
type	Academic Article research paper schema:ScholarlyArticle
isDefinedBy	Covid-on-the-Web dataset
has title	Manthan: A Data-Driven Approach for Boolean Function Synthesis
Creator	Golia, Priyanka Meel, Kuldeep Roy, Subhajit
Source	PMC
abstract	Boolean functional synthesis is a fundamental problem in computer science with wide-ranging applications and has witnessed a surge of interest resulting in progressively improved techniques over the past decade. Despite intense algorithmic development, a large number of problems remain beyond the reach of the state of the art techniques. Motivated by the progress in machine learning, we propose [Formula: see text], a novel data-driven approach to Boolean functional synthesis. [Formula: see text] views functional synthesis as a classification problem, relying on advances in constrained sampling for data generation, and advances in automated reasoning for a novel proof-guided refinement and provable verification. On an extensive and rigorous evaluation over 609 benchmarks, we demonstrate that [Formula: see text] significantly improves upon the current state of the art, solving 356 benchmarks in comparison to 280, which is the most solved by a state of the art technique; thereby, we demonstrate an increase of 76 benchmarks over the current state of the art. Furthermore, [Formula: see text] solves 60 benchmarks that none of the current state of the art techniques could solve. The significant performance improvements, along with our detailed analysis, highlights several interesting avenues of future work at the intersection of machine learning, constrained sampling, and automated reasoning.
has issue date	2020-06-16(xsd:dateTime)
bibo:doi	10.1007/978-3-030-53291-8_31
has license	cc-by
sha1sum (hex)	35b44141ad8d23b54cb3c4e187c8538a5e3bb413
schema:url	https://doi.org/10.1007/978-3-030-53291-8_31
resource representing a document's title	Manthan: A Data-Driven Approach for Boolean Function Synthesis
has PubMed Central identifier	PMC7363189
schema:publication	Computer Aided Verification
resource representing a document's body	covid:35b44141ad8d23b54cb3c4e187c8538a5e3bb413#body_text
is schema:about of	named entity 'DEVELOPMENT' named entity 'APPLICATIONS' named entity 'WIDE' covid:arg/35b44141ad8d23b54cb3c4e187c8538a5e3bb413 named entity 'QBF' named entity 'SAT solver' named entity 'leaf node' named entity 'Skolem functions' named entity 'Skolem function' named entity 'subroutines' named entity 'Manthan' named entity 'debugging' named entity 'Skolem function' named entity 'runtime performance' named entity 'Manthan' named entity 'Manthan' named entity 'machine learning' named entity 'Boolean functions' named entity 'Manthan' named entity 'Manthan' named entity 'Arithmetic' named entity 'Manthan' named entity 'decision tree' named entity 'Skolem function' named entity 'algorithm' named entity 'Skolem function' named entity 'quantified variables' named entity 'Boole' named entity 'algorithm' named entity 'Skolem function' named entity 'conjunctive normal form' named entity 'ID3 algorithm' named entity 'pseudocode' named entity 'Manthan' named entity 'machine learning' named entity 'heuristics' named entity 'existentially quantified variables' named entity 'disjunction' named entity 'Boolean function' named entity 'subroutine' named entity 'decision-tree' named entity 'Manthan' named entity 'Skolem functions' named entity 'Manthan' named entity 'data set' named entity 'high-performance' named entity 'heuristic' named entity 'Tabajara' named entity 'sample complexity' named entity 'Skolem functions' named entity 'SAT solvers' named entity 'QBF' named entity 'Skolem functions' named entity 'decidability' named entity 'MaxSAT' named entity 'Conflict-Driven Clause Learning' named entity 'black boxes' named entity 'knowledge compilation' named entity 'Skolem function' named entity 'disjunction' named entity 'SAT solver' named entity 'Manthan' named entity 'Boolean functions' named entity 'Verilog' named entity 'Boolean' named entity 'Manthan' named entity 'existentially quantified' named entity 'knowledge compilation' named entity 'unsatisfiable' named entity 'Manthan' named entity 'Boolean function' named entity 'unsatisfiable' named entity 'functional composition' named entity 'recursively' named entity 'Skolem functions' named entity 'PicoSAT' named entity 'Formula 1' named entity 'polynomial' named entity 'partial order' named entity 'MaxSAT' named entity 'Barbarik'

Faceted Search & Find service v1.13.91 as of Mar 24 2020

Alternative Linked Data Documents: Sponger | ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 07.20.3229 as of Jul 10 2020, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (94 GB total memory)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software