Superredundancy: A tool for Boolean formula minimization complexity analysis
A superredundant clause is a clause that is redundant in the resolution closure of a formula. The converse concept of superirredundancy ensures membership of the clause in all minimal CNF formulae that are equivalent to the given one. This allows for building formulae where some clauses are fixed when minimizing size. An example are proofs of complexity hardness of the problems of minimal formula size. Others are proofs of size when forgetting variables or revising a formula. Most clauses can be made superirredundant by splitting them over a new variable.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Minimization of Boolean Complexity in In-Context Concept Learning
What factors contribute to the relative success and corresponding difficulties of in-context learning for Large Language Models (LLMs)? Drawing on insights from the literature on human concept learning, we test LLMs on c…
In-Context LearningGeneral Boolean Formula Minimization with QBF Solvers
The minimization of propositional formulae is a classical problem in logic, whose first algorithms date back at least to the 1950s with the works of Quine and Karnaugh. Most previous work in the area has focused on obtai…
A Heuristic Approach to Two Level Boolean Minimization Derived from Karnaugh Mapping
The following paper presents a heuristic method by which sum-of-product Boolean expressions can be simplified with a specific focus on the removal of redundant and selective prime implicants. Existing methods, such as th…
Learning from Satisfying Assignments Using Risk Minimization
In this paper we consider the problem of Learning from Satisfying Assignments introduced by \cite{1} of finding a distribution that is a close approximation to the uniform distribution over the satisfying assignments of …
parameter estimationQuadratization of Symmetric Pseudo-Boolean Functions
A pseudo-Boolean function is a real-valued function $f(x)=f(x_1,x_2,\ldots,x_n)$ of $n$ binary variables; that is, a mapping from $\{0,1\}^n$ to $\mathbb{R}$. For a pseudo-Boolean function $f(x)$ on $\{0,1\}^n$, we say t…