"Studies on Convexity of DNF Formulae" by Josue A. Ruiz

ORCID

https://orcid.org/0009-0007-0674-9783

Date of Award

Spring 2025

Language

English

Embargo Period

5-9-2025

Document Type

Dissertation

Degree Name

Doctor of Philosophy (PhD)

College/School/Department

Department of Computer Science

Program

Computer Science

First Advisor

Paliath Narendran

Second Advisor

Amir Masoumzadeh

Committee Members

Chinwe Ekenna, Jeff Offutt

Keywords

convexity, upward closure, DNF, Boolean formula, gap

Subject Categories

Cybersecurity | Logic and Foundations | Theory and Algorithms

Abstract

In this dissertation, we investigate the problem of determining whether a Boolean formula given in disjunctive normal form (DNF) is convex. Although Boolean formulas have various applications, our research focuses on the practical application for rule-based access control policies, where policies are often expressed as a set of Boolean rules. Understanding the structural properties of such formulas is crucial for determining whether a policy can be efficiently represented within a specific access control model.

The main contribution of this research is the conception and analysis of convexity derived from the “gap problem.” In this context, convexity is characterized by the absence of gaps between any two arbitrary terms in a DNF formula, where a gap suggests a missing intermediate assignment that would otherwise bridge the terms within the Boolean space. By formalizing this notion, we derive necessary and sufficient conditions for a DNF formula to be convex, identifying possible differences between any two terms regarding the literals they do and do not share.

In addition to convexity, we discuss related properties, including upward closure and co-convexity. A significant aspect of this research is the development of algorithms for checking these properties. We propose methods and conduct complexity analyses. An important contribution of this research is reducing the verification problem to an instance of the Boolean satisfiability problem (SAT). This allows us to utilize efficient SAT solvers to address these challenges. Additionally, we employ graph-based algorithms on a special subclass of DNF formulas to optimize the verification process of the properties mentioned above.

License

Creative Commons Attribution 4.0 International License
This work is licensed under a Creative Commons Attribution 4.0 International License.

Share

COinS