NDLI: SAT Modulo Linear Arithmetic for Solving Polynomial Constraints

Content Provider	Springer Nature Link
Author	Borralleras, Cristina Lucas, Salvador Oliveras, Albert Rodríguez Carbonell, Enric Rubio, Albert
Copyright Year	2010
Abstract	Polynomial constraint solving plays a prominent role in several areas of hardware and software analysis and verification, e.g., termination proving, program invariant generation and hybrid system verification, to name a few. In this paper we propose a new method for solving non-linear constraints based on encoding the problem into an SMT problem considering only linear arithmetic. Unlike other existing methods, our method focuses on proving satisfiability of the constraints rather than on proving unsatisfiability, which is more relevant in several applications as we illustrate with several examples. Nevertheless, we also present new techniques based on the analysis of unsatisfiable cores that allow one to efficiently prove unsatisfiability too for a broad class of problems. The power of our approach is demonstrated by means of extensive experiments comparing our prototype with state-of-the-art tools on benchmarks taken both from the academic and the industrial world.
Starting Page	107
Ending Page	131
Page Count	25
File Format	PDF
ISSN	01687433
Journal	Journal of Automated Reasoning
Volume Number	48
Issue Number	1
e-ISSN	15730670
Language	English
Publisher	Springer Netherlands
Publisher Date	2010-09-04
Publisher Place	Dordrecht
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Non-linear arithmetic Constraint solving Polynomial constraints SAT modulo theories Termination System verification Mathematical Logic and Foundations Artificial Intelligence (incl. Robotics) Mathematical Logic and Formal Languages Symbolic and Algebraic Manipulation
Content Type	Text
Resource Type	Article
Subject	Artificial Intelligence Computational Theory and Mathematics Software

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Cutting to the Chase : Solving Linear Integer Arithmetic

6 Years of SMT-COMP

Linear Quantifier Elimination

Formalization and Implementation of Modern SAT Solvers

Mechanically Proving Termination Using Polynomial Interpretations

SAT Solving for Termination Proofs with Recursive Path Orders and Dependency Pairs

Formal verification of a generic framework to synthesize SAT-provers

An Experiment with Satisfiability Modulo SAT

SMELS: Satisfiability Modulo Equality with Lazy Superposition

SAT Modulo Linear Arithmetic for Solving Polynomial Constraints

Similar Documents

Cutting to the Chase : Solving Linear Integer Arithmetic

6 Years of SMT-COMP

Linear Quantifier Elimination

Formalization and Implementation of Modern SAT Solvers

Mechanically Proving Termination Using Polynomial Interpretations

SAT Solving for Termination Proofs with Recursive Path Orders and Dependency Pairs

Formal verification of a generic framework to synthesize SAT-provers

An Experiment with Satisfiability Modulo SAT

SMELS: Satisfiability Modulo Equality with Lazy Superposition

SAT Modulo Linear Arithmetic for Solving Polynomial Constraints