Artificial Conflict Sampling for Real Satisfiability Problems

James H. Davenport; Ali K. Uncu

doi:10.1109/SYNASC57785.2022.00018

Artificial Conflict Sampling for Real Satisfiability Problems

Austrian Academy of Sciences

Research output: Chapter or section in a book/report/conference proceeding › Chapter 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 language	English
Title of host publication	2022 24th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC)
Editors	Bruno Buchberger, Mircea Marin, Viorel Negru, Daniela Zaharie
Place of Publication	United States
Publisher	IEEE
Pages	55-58
Number of pages	4
ISBN (Electronic)	9781665465458
DOIs	https://doi.org/10.1109/SYNASC57785.2022.00018
Publication status	Published - 25 May 2023
Event	24th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2022 - Linz, Austria Duration: 12 Sept 2022 → 15 Sept 2022

Publication series

Name	Proceedings of the International Symposium on Symbolic and Numeric Algorithms for Scientific Computing
Publisher	IEEE
ISSN (Electronic)	2470-881X

Conference

Conference	24th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2022
Country/Territory	Austria
City	Linz
Period	12/09/22 → 15/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

Funding

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

Access to Document

10.1109/SYNASC57785.2022.00018

Cite this

Davenport, J. H., & Uncu, A. K. (2023). Artificial Conflict Sampling for Real Satisfiability Problems. In B. Buchberger, M. Marin, V. Negru, & D. Zaharie (Eds.), 2022 24th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC) (pp. 55-58). (Proceedings of the International Symposium on Symbolic and Numeric Algorithms for Scientific Computing). IEEE. https://doi.org/10.1109/SYNASC57785.2022.00018

Artificial Conflict Sampling for Real Satisfiability Problems. / Davenport, James H.; Uncu, Ali K.
2022 24th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC). ed. / Bruno Buchberger; Mircea Marin; Viorel Negru; Daniela Zaharie. United States: IEEE, 2023. p. 55-58 (Proceedings of the International Symposium on Symbolic and Numeric Algorithms for Scientific Computing).

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

Davenport, JH & Uncu, AK 2023, Artificial Conflict Sampling for Real Satisfiability Problems. in B Buchberger, M Marin, V Negru & D Zaharie (eds), 2022 24th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC). Proceedings of the International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, IEEE, United States, pp. 55-58, 24th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2022, Linz, Austria, 12/09/22. https://doi.org/10.1109/SYNASC57785.2022.00018

Davenport JH , Uncu AK. Artificial Conflict Sampling for Real Satisfiability Problems. In Buchberger B, Marin M, Negru V, Zaharie D, editors, 2022 24th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC). United States: IEEE. 2023. p. 55-58. (Proceedings of the International Symposium on Symbolic and Numeric Algorithms for Scientific Computing). doi: 10.1109/SYNASC57785.2022.00018

Davenport, James H. ; Uncu, Ali K. / Artificial Conflict Sampling for Real Satisfiability Problems. 2022 24th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC). editor / Bruno Buchberger ; Mircea Marin ; Viorel Negru ; Daniela Zaharie. United States : IEEE, 2023. pp. 55-58 (Proceedings of the International Symposium on Symbolic and Numeric Algorithms for Scientific Computing).

@inproceedings{9a4253b804ed4ae3870972cf955599f9,

title = "Artificial Conflict Sampling for Real Satisfiability Problems",

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.",

keywords = "Conflicting Points, Equational Constraints, Root Isolation, Strict Inequalities",

author = "Davenport, {James H.} and Uncu, {Ali K.}",

note = "Funding Information: JHD and AKU were partially supported by the UK{\textquoteright}s EPSRC under grant EP/T015713/1. AKU was also supported by FWF under P-34501N ; 24th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2022 ; Conference date: 12-09-2022 Through 15-09-2022",

year = "2023",

month = may,

day = "25",

doi = "10.1109/SYNASC57785.2022.00018",

language = "English",

series = "Proceedings of the International Symposium on Symbolic and Numeric Algorithms for Scientific Computing",

publisher = "IEEE",

pages = "55--58",

editor = "Bruno Buchberger and Mircea Marin and Viorel Negru and Daniela Zaharie",

booktitle = "2022 24th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC)",

address = "USA United States",

}

TY - GEN

T1 - Artificial Conflict Sampling for Real Satisfiability Problems

AU - Davenport, James H.

AU - Uncu, Ali K.

N1 - 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

PY - 2023/5/25

Y1 - 2023/5/25

N2 - 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.

AB - 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.

KW - Conflicting Points

KW - Equational Constraints

KW - Root Isolation

KW - Strict Inequalities

UR - http://www.scopus.com/inward/record.url?scp=85163059053&partnerID=8YFLogxK

U2 - 10.1109/SYNASC57785.2022.00018

DO - 10.1109/SYNASC57785.2022.00018

M3 - Chapter in a published conference proceeding

AN - SCOPUS:85163059053

T3 - Proceedings of the International Symposium on Symbolic and Numeric Algorithms for Scientific Computing

SP - 55

EP - 58

BT - 2022 24th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC)

A2 - Buchberger, Bruno

A2 - Marin, Mircea

A2 - Negru, Viorel

A2 - Zaharie, Daniela

PB - IEEE

CY - United States

T2 - 24th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2022

Y2 - 12 September 2022 through 15 September 2022

ER -

Artificial Conflict Sampling for Real Satisfiability Problems

Abstract

Publication series

Conference

Bibliographical note

Funding

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Pushing Back the Doubly-Exponential Wall of Cylindrical Algebraic Decomposition

Cite this

Artificial Conflict Sampling for Real Satisfiability Problems

Abstract

Publication series

Conference

Bibliographical note

Funding

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Projects

Pushing Back the Doubly-Exponential Wall of Cylindrical Algebraic Decomposition

Cite this