All Questions
15 questions
2
votes
1
answer
84
views
1-in-k-SAT problem restricted to only positive literals and at most two occurrences of a variable
1-in-k-SAT problem is to determine if there’s an assignment to variables such that every clause has exactly one true literal.
Is this problem known to be in P when restricted to positive literals, and ...
1
vote
1
answer
109
views
Specialized SAT solver (?)
(Context)
Given two byte arrays of length 16, say $L$ and $H$, one can define a mapping $M$ from the set of all bytes to itself in the following way.
If $0 \le b \lt 256$ is a byte, let $\text{lo}(b)$ ...
1
vote
1
answer
125
views
Understanding the Strong Exponential Time Hypothesis
Let $n$ be the number of variables in the input formula and $m$ the number of clauses. Define $s_k = \inf\{\delta : k\text{-SAT can be solved in } 2^{\delta n} \text{ time}\}$. The strong exponential ...
1
vote
1
answer
70
views
Proving 2SAT is in P vs algorithm for finding a satisfying assignment
I want to understand the proof in the following link that 2SAT is in P. What is the need for the last corollary? Wouldn't be enough to just prove the case for the graph with the help of the path ...
2
votes
1
answer
58
views
Satisfiability of bounded assignment of input variables to CNF formula
Consider a CNF formula $F$ such that all the literals in every clause must be negative ( here is an example : $F$ = ($\bar{x_{1}}$ $\wedge$ $\bar{x_{2}}$) $\vee$ ($\bar{x_{3}}$ $\wedge$ $\bar{x_{4}}$ $...
4
votes
1
answer
101
views
Attempt to reduce to problem of inner product
The problem of Orthogonality: gives $n$ vectors of dimension $k$ and another set of same, can a pair be found with inner product = $0$?
The problem of max product: likewise two sets each $n$ vectors (...
1
vote
0
answers
151
views
Reduction between Parity-SAT and approximate counting
Consider two problems as defined here.
Approximate counting: Given a Boolean function $f(x)$, for $x \in \{0, 1\}^{n}$, distinguish between the two cases:
The number of satisfying assignments for $f(...
1
vote
0
answers
63
views
Different definitions of Exponential Time Hypothesis
I am reading basics of Exponential Time Hypothesis (ETH). There are two statements for it:
Statement 1
There exists no $2^{o(n)}$ algorithm for $3$-SAT, where $n$ is the number of variables.
Statement ...
0
votes
1
answer
905
views
3SAT and directed graph
Given a 3SAT instance (a Boolean expression in three conjunctural normal form), we draw a directed graph, where for each Boolean variable $x_{i}$ we have the nodes $x_{i}$ and $!x_{i}$; for each ...
1
vote
0
answers
203
views
Could you show the intractibility of SAT by showing that the number of variables contributing to an arbitrary unsatisfied clause is not constant? [closed]
Preface: This is not an attempted proof at P vs NP
Starting with some CNF Boolean expression ϕ, by the rules of logical disjunction, a clause is only unsatisfied if each of the literals in it are ...
1
vote
2
answers
2k
views
What are known 3SAT to 2SAT reductions?
Is there a way to convert a 3SAT formula into a equisatisfiable 2SAT formula? Each method is of interest, even those that grow exponentially.
(So if, for example, my 3SAT formula has 16 variables and ...
5
votes
1
answer
356
views
Algorithm for a special case of SAT/#SAT
Does anyone know of an algorithm that can solve the following special case of SAT in polynomial time? Are there any algorithms that can solve the counting (#SAT) version of it in polynomial time?
...
9
votes
1
answer
159
views
What is the name of the problem? (partitioning graph into three covers)
I was wondering if this problem has a name:
Given a simple graph whose edges are colored red, blue and green, $G=(V,B\cup R\cup G)$, is there a vertex-coloring $c:V\to \{B,R,G\}$ such that every edge ...
3
votes
1
answer
854
views
Can quantified renamable Horn formulas be identified using the same procedure as unquantified formulas?
Definition: A renamable Horn formula is a Boolean formula that can be transformed into a Horn formula by flipping the polarity of every instance of one of more of its variables.
Example:
$\qquad (...
6
votes
2
answers
746
views
Modeling the problem of finding all stable sets of an argumentation framework as SAT
As a continuation of my previous question i will try to explain my problem and how i am trying to convert my algorithm to a problem that can be expressed in a CNF form.
Problem: Find all stable sets ...