• Classified by Research Topic • Sorted by Date • Classified by Publication Type •
Phase Transition Behavior of Cardinality and XOR Constraints .
Yash Pote, Saurabh Joshi and Kuldeep S. Meel.
In Proceedings of International Joint Conference on Artificial Intelligence (IJCAI), August 2019.
The runtime performance of modern SAT solvers is deeply connected to the phase transition behavior of CNF formulas. While CNF solving has witnessed significant runtime improvement over the past two decades, the same does not hold for several other classes such as the conjunction of cardinality and XOR constraints, denoted as CARD-XOR formulas. The problem of determining satisfiability of CARD-XOR formulas is a fundamental problem with wide variety of applications ranging from discrete integration in the field of artificial intelligence to maximum likelihood decoding in coding theory. The runtime behavior of random CARD-XOR formulas is unexplored in prior work. In this paper, we present the first rigorous empirical study to characterize the runtime behavior of 1-CARD-XOR formulas. We show empirical evidence of a surprising phase-transition that follows a non-linear tradeoff between CARD and XOR constraints.
@inproceedings{PJM19,
title={Phase Transition Behavior of Cardinality and XOR Constraints },
author={Pote, Yash and Joshi, Saurabh and Meel, Kuldeep S.},
bib2html_pubtype={Refereed Conference},
booktitle=IJCAI,
month=aug,
year={2019},
bib2html_rescat={Phase Transitions},
bib2html_dl_pdf={../Papers/ijcai19pjm.pdf},
abstract={The runtime performance of modern SAT solvers is deeply connected to the phase transition behavior of CNF formulas. While CNF solving has witnessed significant runtime improvement over the past two decades, the same does not hold for several other classes such as the conjunction of cardinality and XOR constraints, denoted as CARD-XOR formulas. The problem of determining satisfiability of CARD-XOR formulas is a fundamental problem with wide variety of applications ranging from discrete integration in the field of artificial intelligence to maximum likelihood decoding in coding theory. The runtime behavior of random CARD-XOR formulas is unexplored in prior work. In this paper, we present the first rigorous empirical study to characterize the runtime behavior of 1-CARD-XOR formulas. We show empirical evidence of a surprising phase-transition that follows a non-linear tradeoff between CARD and XOR constraints.
}
}
Generated by bib2html.pl (written by Patrick Riley with layout from Sanjit A. Seshia ) on Sun Apr 14, 2024 11:15:51