Phase Transition Behavior of Cardinality and XOR Constraints

Authors: Yash Pote, Saurabh Joshi, Kuldeep S. Meel

IJCAI 2019 | Conference PDF | Archive PDF | Plain Text | LLM Run Details

Reproducibility Variable Result LLM Response
Research Type Experimental 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. ... We performed experiments with 9 values of n.
Researcher Affiliation Academia Yash Pote1 , Saurabh Joshi2 and Kuldeep S. Meel1 1National University of Singapore 2IIT Hyderabad, India
Pseudocode No The paper does not contain any pseudocode or clearly labeled algorithm blocks.
Open Source Code Yes The data and scripts associated with this project are available at https://github.com/meelgroup/1-CARD-XOR
Open Datasets No The paper describes a process for generating instances for experiments but does not provide access information for a publicly available or open dataset. Instances are generated programmatically based on parameters.
Dataset Splits No The paper describes generating instances for evaluation but does not specify explicit training, validation, or test dataset splits in the conventional sense of machine learning datasets.
Hardware Specification Yes We used a high performance computing cluster of 25 nodes for our experiments. Each node consisted of an Intel R Xeon R E5-2690 v3 CPU with 24 cores and 96GB of RAM divided evenly among the cores, with each core having access to 4GB of RAM.
Software Dependencies No The paper mentions using "Crypto Mini SAT [Soos et al., 2009]" and "PBLib [Philipp and Steinke, 2015]" but does not specify version numbers for these software components.
Experiment Setup Yes For each n {50, 75, 100, 125, 150, 175, 200, 250, 300} we generated an instance of 1-CARD-XOR for all values of k [0, n] and sn [1, n]. We repeated the experiments 10 times for each data point with n = {75, 100} to get a finer estimate on the satisfiability at the transition threshold. ... A timeout of 2000 seconds was used for all experiments.