Artificial Conflict Sampling for Real Satisfiability Problems

Research output: Chapter or section in a book/report/conference proceedingChapter in a published conference proceeding

Abstract

We outline some preliminary ideas on a guided theory assignment of variables in a real (QF_NRA) satisfiability problem. One objective of this approach is to mix the topdown approach of cylindric algebraic decomposition and the bottom-up approach of partial theory assignments of modern SAT/SMT solvers. We use equational constraints and a single strict inequality at a time to artificially create conflicting variable assignment traces, which can later be used in conflict resolution to enrich the constraints of the original satisfiability problem.

Original languageEnglish
Title of host publication2022 24th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC)
EditorsBruno Buchberger, Mircea Marin, Viorel Negru, Daniela Zaharie
Place of PublicationUnited States
PublisherIEEE
Pages55-58
Number of pages4
ISBN (Electronic)9781665465458
DOIs
Publication statusPublished - 25 May 2023
Event24th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2022 - Linz, Austria
Duration: 12 Sept 202215 Sept 2022

Publication series

NameProceedings of the International Symposium on Symbolic and Numeric Algorithms for Scientific Computing
PublisherIEEE
ISSN (Electronic)2470-881X

Conference

Conference24th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2022
Country/TerritoryAustria
CityLinz
Period12/09/2215/09/22

Bibliographical note

Funding Information:
JHD and AKU were partially supported by the UK’s EPSRC under grant EP/T015713/1. AKU was also supported by FWF under P-34501N

Keywords

  • Conflicting Points
  • Equational Constraints
  • Root Isolation
  • Strict Inequalities

ASJC Scopus subject areas

  • Computational Theory and Mathematics
  • Decision Sciences (miscellaneous)
  • Computational Mathematics
  • Modelling and Simulation
  • Numerical Analysis

Fingerprint

Dive into the research topics of 'Artificial Conflict Sampling for Real Satisfiability Problems'. Together they form a unique fingerprint.

Cite this