paper-with-me

Papers

SATfeatPy - A Python-based Feature Extraction System for Satisfiability

2022-04-29 · Benjamin Provan-Bessell, Marco Dalla, Andrea Visentin, Barry O'Sullivan

Feature extraction is a fundamental task in the application of machine learning methods to SAT solving. It is used in algorithm selection and configuration for solver portfolios and satisfiability classification. Many approaches have been proposed to extract meaningful attributes from CNF instances. Most of them lack a working/updated implementation, and the limited descriptions lack clarity affecting the reproducibility. Furthermore, the literature misses a comparison among the features. This paper introduces SATfeatPy, a library that offers feature extraction techniques for SAT problems in the CNF form. This package offers the implementation of all the structural and statistical features from there major papers in the field. The library is provided in an up-to-date, easy-to-use Python package alongside a detailed feature description. We show the high accuracy of SAT/UNSAT and problem category classification, using five sets of features generated using our library from a dataset of 3000 SAT and UNSAT instances, over ten different classes of problems. Finally, we compare the usefulness of the features and importance for predicting a SAT instance's original structure in an ablation study.

📄 PDF Abstract BibTeX arXiv:2204.14116

Code (1)

bprovanbessell/satfeatpy 공식 구현

Similar Papers 제목 키워드 기반

EduSAT: A Pedagogical Tool for Theory and Applications of Boolean Satisfiability

2023-08-15 · Yiqi Zhao, Ziyan An, Meiyi Ma, Taylor Johnson

Boolean Satisfiability (SAT) and Satisfiability Modulo Theories (SMT) are widely used in automated verification, but there is a lack of interactive tools designed for educational purposes in this field. To address this g…

Bayesian Statistical Model Checking for Multi-agent Systems using HyperPCTL*

2022-09-06 · Spandan Das, Pavithra Prabhakar

In this paper, we present a Bayesian method for statistical model checking (SMC) of probabilistic hyperproperties specified in the logic HyperPCTL* on discrete-time Markov chains (DTMCs). While SMC of HyperPCTL* using se…

MCP-Solver: Integrating Language Models with Constraint Programming Systems

2024-12-31 · Stefan Szeider

The MCP Solver bridges Large Language Models (LLMs) with symbolic solvers through the Model Context Protocol (MCP), an open-source standard for AI system integration. Providing LLMs access to formal solving and reasoning…

Natural Language Understanding

An Eager Satisfiability Modulo Theories Solver for Algebraic Datatypes

2023-10-18 · Amar Shah, Federico Mora, Sanjit A. Seshia

Algebraic data types (ADTs) are a construct classically found in functional programming languages that capture data structures like enumerated types, lists, and trees. In recent years, interest in ADTs has increased. For…

TSFEL: Time Series Feature Extraction Library

2020-03-21 · SoftwareX 2020 3 · Marília Barandas, Duarte Folgado, Letícia Fernandes, Sara Santos 외

Time series feature extraction is one of the preliminary steps of conventional machine learning pipelines. Quite often, this process ends being a time consuming and complex task as data scientists must consider a combina…

Feature EngineeringTime SeriesTime Series Analysis