Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [boolean-formulas]

The tag has no usage guidance.

14
votes
1answer
305 views

The problem of deciding whether a monotone CNF implies a monotone DNF

Consider the following decision problem Input: A monotone CNF $\Phi$ and a monotone DNF $\Psi$. Question: Is $\Phi \to \Psi$ a tautology? Definitely you can solve this problem in $O(2^n \cdot \...
1
vote
1answer
48 views

Is there a standard format for Dependent QBF?

I know there is a standard input format DIMACS for a formula is in conjunctive normal form (CNF) and QDIMACS for quantified Boolean formulas. Is there a similar standard format for the Dependent-QBF (...
2
votes
1answer
175 views

Fourier decomposition in terms of another basis

Given a Boolean function $f:\{-1,1\}^n\rightarrow \{-1,1\}$, it is well know that the Fourier decomposition of $f$ can be written as $f(x)=\sum_{S\subseteq \{1,\ldots,n\}} \widehat{f}(S) \prod_{i\in S}...
4
votes
0answers
112 views

Reduce $m$-clause 3SAT to PLANAR-3SAT in $O(m^{2-\varepsilon})$

The classic reduction from 3SAT to PLANAR-3SAT requires a removal of $O(m^2)$ crossings from a rectilinear representation of 3SAT with $m$ clauses. However, the crossing number inequality suggests ...
2
votes
1answer
242 views

Minimum Unsatisfiable Core

Recently in a course I'm taking, we have been learning about the DPLL(T) algorithm for SMT solving. The basic outline goes like this: ...
15
votes
3answers
279 views

Quantified Boolean Formulas with logarithmic alternations

I'm studying a problem which is hard for the class of quantified boolean formulas with a logarithmic number of alternations of the quantifiers. A problem in this class would look like: $\forall (x_1, ...
4
votes
0answers
126 views

Evaluating boolean formula without knowing all values

I am looking for research approaches for the following problem: assume we have a set of $m$ computers, each carries a bit, and a Boolean formula $\varphi$ over those $m$ variables. The computers are ...
3
votes
0answers
136 views

Shrinkage Exponent of Formulas over the Full Binary Basis

Håstad has shown that the shrinkage exponent of boolean formulas over the De Morgan basis is 2. In other words, if one keeps each variable of the formula alive with probability $p$ and restricts it ...
2
votes
1answer
75 views

Complexity of generating a pseudo-Boolean function

A pseudo-Boolean function is a mapping from $\mathcal{B}^n = \{0, 1\}^n$ to $\mathbb{R}$. Following is a pseudo-Boolean function. $$s_1 s_4 - s_2 s_3 - s_3 s_5 - s_2 s_5 + s_1 + s_4 - s_1 s_3 - ...
3
votes
1answer
116 views

Symbolic Execution of the Quine-McCluskey Algorithim

If I understand correctly, the Quine–McCluskey algorithm will find the minimum boolean formula size for given boolean function. Has there been any attempts to (for lack of a better term) symbolically ...
11
votes
2answers
255 views

What is the complexity of the equivalence problem for read-once decision trees?

A read-once decision tree is defined as follows: $True$ and $False$ are read-once decision trees. If $A$ and $B$ are read-once decision trees and $x$ is a variable not occurring in $A$ and $B$, ...
2
votes
3answers
177 views

How hard is it to find a “well-distributed” subset of models of a propositional formula?

We consider the propositional language $\mathcal{L}_{\mathit{PS}}$ defined over a finite alphabet $\mathit{PS}$ and the usual logical connectives. An interpretation is an assignment $\mathit{PS} \...
12
votes
0answers
266 views

Computing $\operatorname{MAJ}_n$ by $\operatorname{MAJ}_m$ in depth 2

Can the majority of $n$ bits be computed by a depth 2 formula all of whose gates compute the majority of $m$ bits where $m=O(n^c)$ for a constant $c<1$? Such a formula contains $m+1$ gates and $m^2$...
1
vote
1answer
81 views

What is the complexity of the set of closed boolean tautologies assuming well formed formulae?

Let's define two CFGs: S ::= 0 | 1 | (S+S) | (S*S) S' ::= 0 | 1 | S+S | S*S | (S) And two languages: M = { w | S generates w, and w evaluates to 1 } M'...
8
votes
1answer
1k views

Conversion between k-SAT and XOR-SAT

According to XOR Satisfiability Solver Module for DPLL Integration by Tero Laitinen, we need $2^{n-1}$ CNF clauses to convert an $n$ literal XOR-SAT clause if we do not want to increase the number of ...
7
votes
1answer
311 views

May Boolean circuits be exponentially more concise than Boolean formulae?

Consider a family $(f_n)_{1 \leq n}$ of Boolean functions, where $f_n$ is a function on $n$ variables. Consider for every $n$ the smallest Boolean formula $F_n$ describing $f_n$, and the smallest ...
4
votes
3answers
163 views

Remove unneeded atoms in CNF minimalization (SAT preprocessing)

This might be a very basic question. I am interested in all atoms of a propositional formula that can be removed from a particular formula, while the derived formula has the same satisfiability ...
2
votes
2answers
176 views

Number of SAT checks that are needed to find all combinations of subset of boolean variables of a propositional formula

Please mind that I sometimes lack formal mathematical knowledge and English is not my first language, so I might miss the right words. Please change the tile if needed. Also, I have choosen this site ...
6
votes
0answers
769 views

k-CNF ←→ k-DNF conversion to minimize errors

the following problem/question seems fundamental/hard. it appears in some circuit theory proofs, graph theory, and maybe elsewhere. looking for any nontrivial insight. will add various known/nearby ...
2
votes
2answers
462 views

Size of decision tree for f is polynomial in the DNF size of f and CNF size of f

I've been having hard time with proving the following claim: Let $f:\{T,F\}^n\rightarrow \{T,F\}$ be a boolean function. Let $size_{DT}(f)$ denote the number of leaves in the smallest (w.r.t the ...
10
votes
1answer
345 views

Boolean formula balancing in $\mathsf{AC^0}$

I am looking for references about the complexity of Boolean formula balancing problem. In particular, Was it known that Boolean formulas can be balanced in $\mathsf{AC^0}$? Is there a simple proof of ...