-
Hardness of Random Reordered Encodings of Parity for Resolution and CDCL
Authors:
Leroy Chew,
Alexis de Colnet,
Friedrich Slivovsky,
Stefan Szeider
Abstract:
Parity reasoning is challenging for Conflict-Driven Clause Learning (CDCL) SAT solvers. This has been observed even for simple formulas encoding two contradictory parity constraints with different variable orders (Chew and Heule 2020). We provide an analytical explanation for their hardness by showing that they require exponential resolution refutations with high probability when the variable orde…
▽ More
Parity reasoning is challenging for Conflict-Driven Clause Learning (CDCL) SAT solvers. This has been observed even for simple formulas encoding two contradictory parity constraints with different variable orders (Chew and Heule 2020). We provide an analytical explanation for their hardness by showing that they require exponential resolution refutations with high probability when the variable order is chosen at random. We obtain this result by proving that these formulas, which are known to be Tseitin formulas, have Tseitin graphs of linear treewidth with high probability. Since such Tseitin formulas require exponential resolution proofs, our result follows. We generalize this argument to a new class of formulas that capture a basic form of parity reasoning involving a sum of two random parity constraints with random orders. Even when the variable order for the sum is chosen favorably, these formulas remain hard for resolution. In contrast, we prove that they have short DRAT refutations. We show experimentally that the running time of CDCL SAT solvers on both classes of formulas grows exponentially with their treewidth.
△ Less
Submitted 1 February, 2024;
originally announced February 2024.
-
Towards Uniform Certification in QBF
Authors:
Leroy Chew,
Friedrich Slivovsky
Abstract:
We pioneer a new technique that allows us to prove a multitude of previously open simulations in QBF proof complexity. In particular, we show that extended QBF Frege p-simulates clausal proof systems such as IR-Calculus, IRM-Calculus, Long-Distance Q-Resolution, and Merge Resolution. These results are obtained by taking a technique of Beyersdorff et al. (JACM 2020) that turns strategy extraction i…
▽ More
We pioneer a new technique that allows us to prove a multitude of previously open simulations in QBF proof complexity. In particular, we show that extended QBF Frege p-simulates clausal proof systems such as IR-Calculus, IRM-Calculus, Long-Distance Q-Resolution, and Merge Resolution. These results are obtained by taking a technique of Beyersdorff et al. (JACM 2020) that turns strategy extraction into simulation and combining it with new local strategy extraction arguments.
This approach leads to simulations that are carried out mainly in propositional logic, with minimal use of the QBF rules. Our proofs therefore provide a new, largely propositional interpretation of the simulated systems. We argue that these results strengthen the case for uniform certification in QBF solving, since many QBF proof systems now fall into place underneath extended QBF Frege.
△ Less
Submitted 12 February, 2024; v1 submitted 13 October, 2022;
originally announced October 2022.
-
Jacobian Granger Causal Neural Networks for Analysis of Stationary and Nonstationary Data
Authors:
Suryadi,
Yew-Soon Ong,
Lock Yue Chew
Abstract:
Granger causality is a commonly used method for uncovering information flow and dependencies in a time series. Here we introduce JGC (Jacobian Granger Causality), a neural network-based approach to Granger causality using the Jacobian as a measure of variable importance, and propose a thresholding procedure for inferring Granger causal variables using this measure. The resulting approach performs…
▽ More
Granger causality is a commonly used method for uncovering information flow and dependencies in a time series. Here we introduce JGC (Jacobian Granger Causality), a neural network-based approach to Granger causality using the Jacobian as a measure of variable importance, and propose a thresholding procedure for inferring Granger causal variables using this measure. The resulting approach performs consistently well compared to other approaches in identifying Granger causal variables, the associated time lags, as well as interaction signs. Lastly, through the inclusion of a time variable, we show that this approach is able to learn the temporal dependencies for nonstationary systems whose Granger causal structures change in time.
△ Less
Submitted 19 May, 2022;
originally announced May 2022.
-
Open government geospatial data on buildings for planning sustainable and resilient cities
Authors:
Filip Biljecki,
Lawrence Zheng Xiong Chew,
Nikola Milojevic-Dupont,
Felix Creutzig
Abstract:
As buildings are central to the social and environmental sustainability of human settlements, high-quality geospatial data are necessary to support their management and planning. Authorities around the world are increasingly collecting and releasing such data openly, but these are mostly disconnected initiatives, making it challenging for users to fully leverage their potential for urban sustainab…
▽ More
As buildings are central to the social and environmental sustainability of human settlements, high-quality geospatial data are necessary to support their management and planning. Authorities around the world are increasingly collecting and releasing such data openly, but these are mostly disconnected initiatives, making it challenging for users to fully leverage their potential for urban sustainability. We conduct a global study of 2D geospatial data on buildings that are released by governments for free access, ranging from individual cities to whole countries. We identify and benchmark more than 140 releases from 28 countries containing above 100 million buildings, based on five dimensions: accessibility, richness, data quality, harmonisation, and relationships with other actors. We find that much building data released by governments is valuable for spatial analyses, but there are large disparities among them and not all instances are of high quality, harmonised, and rich in descriptive information. Our study also compares authoritative data to OpenStreetMap, a crowdsourced counterpart, suggesting a mutually beneficial and complementary relationship.
△ Less
Submitted 28 June, 2021;
originally announced July 2021.
-
Quantum-inspired identification of complex cellular automata
Authors:
Matthew Ho,
Andri Pradana,
Thomas J. Elliott,
Lock Yue Chew,
Mile Gu
Abstract:
Elementary cellular automata (ECA) present iconic examples of complex systems. Though described only by one-dimensional strings of binary cells evolving according to nearest-neighbour update rules, certain ECA rules manifest complex dynamics capable of universal computation. Yet, the classification of precisely which rules exhibit complex behaviour remains a significant challenge. Here we approach…
▽ More
Elementary cellular automata (ECA) present iconic examples of complex systems. Though described only by one-dimensional strings of binary cells evolving according to nearest-neighbour update rules, certain ECA rules manifest complex dynamics capable of universal computation. Yet, the classification of precisely which rules exhibit complex behaviour remains a significant challenge. Here we approach this question using tools from quantum stochastic modelling, where quantum statistical memory -- the memory required to model a stochastic process using a class of quantum machines -- can be used to quantify the structure of a stochastic process. By viewing ECA rules as transformations of stochastic patterns, we ask: Does an ECA generate structure as quantified by the quantum statistical memory, and if so, how quickly? We illustrate how the growth of this measure over time correctly distinguishes simple ECA from complex counterparts. Moreover, it provides a more refined means for quantitatively identifying complex ECAs -- providing a spectrum on which we can rank the complexity of ECA by the rate in which they generate structure.
△ Less
Submitted 20 March, 2024; v1 submitted 25 March, 2021;
originally announced March 2021.
-
Avoiding Monochromatic Rectangles Using Shift Patterns
Authors:
Zhenjun Liu,
Leroy Chew,
Marijn Heule
Abstract:
Ramsey Theory deals with avoiding certain patterns. When constructing an instance that avoids one pattern, it is observed that other patterns emerge. For example, repetition emerges when avoiding arithmetic progression (Van der Waerden numbers), while reflection emerges when avoiding monochromatic solutions of $a+b=c$ (Schur numbers). We exploit observed patterns when coloring a grid while avoidin…
▽ More
Ramsey Theory deals with avoiding certain patterns. When constructing an instance that avoids one pattern, it is observed that other patterns emerge. For example, repetition emerges when avoiding arithmetic progression (Van der Waerden numbers), while reflection emerges when avoiding monochromatic solutions of $a+b=c$ (Schur numbers). We exploit observed patterns when coloring a grid while avoiding monochromatic rectangles. Like many problems in Ramsey Theory, this problem has a rapidly growing search space that makes computer search difficult. Steinbach et al. obtained a solution of an 18 by 18 grid with 4 colors by enforcing a rotation symmetry. However, that symmetry is not suitable for 5 colors.
In this article, we will encode this problem into propositional logic and enforce so-called internal symmetries, which preserves satisfiability, to guide SAT-solving. We first observe patterns with 2 and 3 colors, among which the "shift pattern" can be easily generalized and efficiently encoded. Using this pattern, we obtain a new solution of the 18 by 18 grid that is non-isomorphic to the known solution. We further analyze the pattern and obtain necessary conditions to further trim down the search space. We conclude with our attempts on finding a 5-coloring of a 26 by 26 grid, as well as further open problems on the shift pattern.
△ Less
Submitted 23 December, 2020;
originally announced December 2020.
-
No-boarding buses: Agents allowed to cooperate or defect
Authors:
Vee-Liem Saw,
Lock Yue Chew
Abstract:
We study a bus system with a no-boarding policy, where a "slow" bus may disallow passengers from boarding if it meets some criteria. When the no-boarding policy is activated, people waiting to board at the bus stop are given the choices of \emph{cooperating} or \emph{defecting}. The people's heterogeneous behaviours are modelled by inductive reasoning and bounded rationality, inspired by the El Fa…
▽ More
We study a bus system with a no-boarding policy, where a "slow" bus may disallow passengers from boarding if it meets some criteria. When the no-boarding policy is activated, people waiting to board at the bus stop are given the choices of \emph{cooperating} or \emph{defecting}. The people's heterogeneous behaviours are modelled by inductive reasoning and bounded rationality, inspired by the El Farol problem and the minority game. In defecting the no-boarding policy, instead of the minority group being the winning group, we investigate several scenarios where defectors win if the number of defectors does not exceed the maximum number of allowed defectors but lose otherwise. Contrary to the classical minority game which has $N$ agents repeatedly playing amongst themselves, many real-world situations like boarding a bus involves only a subset of agents who "play each round", with \emph{different subsets playing at different rounds}. We find for such realistic situations, there is no phase transition with no herding behaviour when the usual control paramater $2^m/N$ is small. The absence of the herding behaviour assures feasible and sustainable implementation of the no-boarding policy with allowance for defections, without leading to bus bunching.
△ Less
Submitted 26 October, 2019; v1 submitted 28 June, 2019;
originally announced June 2019.
-
Feasible Interpolation for QBF Resolution Calculi
Authors:
Olaf Beyersdorff,
Leroy Chew,
Meena Mahajan,
Anil Shukla
Abstract:
In sharp contrast to classical proof complexity we are currently short of lower bound techniques for QBF proof systems. In this paper we establish the feasible interpolation technique for all resolution-based QBF systems, whether modelling CDCL or expansion-based solving. This both provides the first general lower bound method for QBF proof systems as well as largely extends the scope of classical…
▽ More
In sharp contrast to classical proof complexity we are currently short of lower bound techniques for QBF proof systems. In this paper we establish the feasible interpolation technique for all resolution-based QBF systems, whether modelling CDCL or expansion-based solving. This both provides the first general lower bound method for QBF proof systems as well as largely extends the scope of classical feasible interpolation. We apply our technique to obtain new exponential lower bounds to all resolution-based QBF systems for a new class of QBF formulas based on the clique problem. Finally, we show how feasible interpolation relates to the recently established lower bound method based on strategy extraction.
△ Less
Submitted 7 June, 2017; v1 submitted 4 November, 2016;
originally announced November 2016.
-
Critical Transitions in Public Opinion: A Case Study of American Presidential Election
Authors:
Ning Ning Chung,
Lock Yue Chew,
Choy Heng Lai
Abstract:
At the tip** point, it is known that small incident can trigger dramatic societal shift. Getting early-warning signals for such changes are valuable to avoid detrimental outcomes such as riots or collapses of nations. However, it is notoriously hard to capture the processes of such transitions in the real-world. Here, we demonstrate the occurrence of a major shift in public opinion in the form o…
▽ More
At the tip** point, it is known that small incident can trigger dramatic societal shift. Getting early-warning signals for such changes are valuable to avoid detrimental outcomes such as riots or collapses of nations. However, it is notoriously hard to capture the processes of such transitions in the real-world. Here, we demonstrate the occurrence of a major shift in public opinion in the form of political support. Instead of simple swap** of ruling parties, we study the regime shift of a party popularity based on its attractiveness by examining the American presidential elections during 1980-2012. A single irreversible transition is detected in 1991. Once a transition happens, recovery to the original level of attractiveness does not bring popularity of the political party back. Remarkably, this transition is corroborated by tell-tale early-warning signature of critical slowing down. Our approach is applicable to shifts in public attitude within any social system.
△ Less
Submitted 18 October, 2016;
originally announced October 2016.
-
Lifting QBF Resolution Calculi to DQBF
Authors:
Olaf Beyersdorff,
Leroy Chew,
Renate Schmidt,
Martin Suda
Abstract:
We examine the existing Resolution systems for quantified Boolean formulas (QBF) and answer the question which of these calculi can be lifted to the more powerful Dependency QBFs (DQBF). An interesting picture emerges: While for QBF we have the strict chain of proof systems Q-Resolution < IR-calc < IRM-calc, the situation is quite different in DQBF. Q-Resolution and likewise universal Resolution a…
▽ More
We examine the existing Resolution systems for quantified Boolean formulas (QBF) and answer the question which of these calculi can be lifted to the more powerful Dependency QBFs (DQBF). An interesting picture emerges: While for QBF we have the strict chain of proof systems Q-Resolution < IR-calc < IRM-calc, the situation is quite different in DQBF. Q-Resolution and likewise universal Resolution are too weak: they are not complete. IR-calc has the right strength: it is sound and complete. IRM-calc is too strong: it is not sound any more, and the same applies to long-distance Resolution. Conceptually, we use the relation of DQBF to EPR and explain our new DQBF calculus based on IR-calc as a subsystem of FO-Resolution.
△ Less
Submitted 27 April, 2016;
originally announced April 2016.
-
Tableau vs. Sequent Calculi for Minimal Entailment
Authors:
Olaf Beyersdorff,
Leroy Chew
Abstract:
In this paper we compare two proof systems for minimal entailment: a tableau system OTAB and a sequent calculus MLK, both developed by Olivetti (1992). Our main result shows that OTAB-proofs can be efficiently translated into MLK-proofs, i.e; MLK p-simulates OTAB. The simulation is technically very involved and answers an open question posed by Olivetti (1992) on the relation between the two calcu…
▽ More
In this paper we compare two proof systems for minimal entailment: a tableau system OTAB and a sequent calculus MLK, both developed by Olivetti (1992). Our main result shows that OTAB-proofs can be efficiently translated into MLK-proofs, i.e; MLK p-simulates OTAB. The simulation is technically very involved and answers an open question posed by Olivetti (1992) on the relation between the two calculi. We also show that the two systems are exponentially separated, i.e; there are formulas which have polynomial size MLK-proofs, but require exponential-size OTAB- proofs.
△ Less
Submitted 7 May, 2014;
originally announced May 2014.
-
Impact of edge-removal on the centrality betweenness of the best spreaders
Authors:
N. N. Chung,
L. Y. Chew,
J. Zhou,
C. H. Lai
Abstract:
The control of epidemic spreading is essential to avoid potential fatal consequences and also, to lessen unforeseen socio-economic impact. The need for effective control is exemplified during the severe acute respiratory syndrome (SARS) in 2003, which has inflicted near to a thousand deaths as well as bankruptcies of airlines and related businesses. In this article, we examine the efficacy of cont…
▽ More
The control of epidemic spreading is essential to avoid potential fatal consequences and also, to lessen unforeseen socio-economic impact. The need for effective control is exemplified during the severe acute respiratory syndrome (SARS) in 2003, which has inflicted near to a thousand deaths as well as bankruptcies of airlines and related businesses. In this article, we examine the efficacy of control strategies on the propagation of infectious diseases based on removing connections within real world airline network with the associated economic and social costs taken into account through defining appropriate quantitative measures. We uncover the surprising results that removing less busy connections can be far more effective in hindering the spread of the disease than removing the more popular connections. Since disconnecting the less popular routes tend to incur less socio-economic cost, our finding suggests the possibility of trading minimal reduction in connectivity of an important hub with efficiencies in epidemic control. In particular, we demonstrate the performance of various local epidemic control strategies, and show how our approach can predict their cost effectiveness through the spreading control characteristics.
△ Less
Submitted 28 March, 2012;
originally announced March 2012.
-
Network Extreme Eigenvalue - from Multimodal to Scale-free Network
Authors:
Ning Ning Chung,
Lock Yue Chew,
Choy Heng Lai
Abstract:
The extreme eigenvalues of adjacency matrices are important indicators on the influences of topological structures to collective dynamical behavior of complex networks. Recent findings on the ensemble averageability of the extreme eigenvalue further authenticate its sensibility in the study of network dynamics. Here we determine the ensemble average of the extreme eigenvalue and characterize the d…
▽ More
The extreme eigenvalues of adjacency matrices are important indicators on the influences of topological structures to collective dynamical behavior of complex networks. Recent findings on the ensemble averageability of the extreme eigenvalue further authenticate its sensibility in the study of network dynamics. Here we determine the ensemble average of the extreme eigenvalue and characterize the deviation across the ensemble through the discrete form of random scale-free network. Remarkably, the analytical approximation derived from the discrete form shows significant improvement over the previous results. This has also led us to the same conclusion as [Phys. Rev. Lett. 98, 248701 (2007)] that deviation in the reduced extreme eigenvalues vanishes as the network size grows.
△ Less
Submitted 22 December, 2011; v1 submitted 13 July, 2011;
originally announced July 2011.
