Questions tagged [sat]
Questions about the Boolean satisfiability problem from computability and complexity theory. If your question is about the college entrance exam called the SAT, you are on the wrong site.
23
questions
1
vote
0
answers
439
views
Possible cardinalities of the sets tautologically implied by minimal sets
Question
Consider the set $V$ of all unordered 3-clauses $(l_1, l_2, l_3)$, where $l_i$ is a literal (i.e. a variable $x$ or its negation $\neg x$), and no clause contains two literals having the same ...
- 11
1
vote
1
answer
91
views
Is it possible to find UNSATisfiable solutions to a SAT problem with a SAT problem?
I'm working with several problems, which can have special unsatisfiable configurations.
For example, consider the simple function $f(x,y)=x+y+2$ with $n$-bit unsigned inputs and $(n+2)$-bit unsigned ...
- 11
4
votes
1
answer
304
views
Lower bound on the number of solutions of 2SAT
To compute the number of solutions of a 2SAT is a hard problem. Is there some nontrivial lower or upper bound on this number in terms of a “coarse-grained” description of the Boolean formula, for ...
- 1,149
8
votes
0
answers
232
views
Size of 3-SAT assignments
Let $F(N,M)$ be the set of 3-SAT formula with $N$ variables and $M$ clauses. For a given formula $f\in F(N,M)$, we can ask for the set $s_f$ of truth assignments that satisfy $f$. (If $f$ is ...
- 3,700
8
votes
0
answers
241
views
Sum of perfect matching construction
Suppose we have two bipartite graphs $G_1$ and $G_2$ with perfect matching count $P_1$ and $P_2$ respectively then their disjoint union gives a bipartite graph with perfect matching $P_1P_2$.
Is ...
- 13.5k
1
vote
0
answers
63
views
Reduction maximum independent set to MIS in a very dense graph
We got a reduction maximum independent set to MIS in a very dense graph,
or alternatively negative monotone 2-CNF to MAX-ONEs with a formula
with many clauses.
Let $G$ be graph of order $n$ and ...
- 24k
3
votes
1
answer
635
views
Is strictly harder than NP-hard cryptography possible?
Looks like there is cryptography based on NP-hard problem, e.g. McEliece cryptosystem. The algorithm is an asymmetric encryption algorithm and is based on the hardness of decoding a general linear ...
- 24k
5
votes
1
answer
928
views
Does this prove Collatz is a $\Sigma_1$ problem?
So I got an email from one of my colleagues on the Collatz Conjecture with a link to the article Computer Scientists Attempt to Corner the Collatz Conjecture by Kevin Hartnett in Quanta Magazine.
On ...
- 13.5k
3
votes
2
answers
238
views
Mapping problems to Boolean formulas for SAT solvers
I came across Marijn Heule and Oliver Kullmann's paper on recent techniques in highly efficient SAT solvers. In particular they describe the Pythagorian Triple Problem, which they solved using that ...
- 145
-1
votes
1
answer
82
views
How to encode minimality constraint into SAT? [closed]
How to encode maximality/minimality constraints in SAT or its variants such as MaxSAT or MinSAT? For example, let us say (x1 OR x2) AND (x2 OR x3 OR x4) AND (x4 OR x5) is a formula. I want its ...
1
vote
0
answers
35
views
Is there an algorithm for this constrained Hypergraph optimization problem?
I'm currently developing an algorithm for computing knot coloring invariants and got to the following question:
Given a set $S$ and a certain hyper-graph $H \subseteq S^3 $, find a decomposition $S = ...
- 133
16
votes
4
answers
861
views
Representing mathematical statements as SAT instances
The following problem (call it THEOREMS) belongs to class NP.
Input: Mathematical statement $S$ (written in some formal system such as ZFC) and positive integer $n$ written in unary.
Output: "Yes" if ...
- 771
2
votes
0
answers
65
views
$3$SAT generation with prescribed number of solutions
Given $n,k\in\Bbb N$ with $0\leq k \leq 2^n$ can we generate an uniformly random instance among all possible solutions of an $n$ variable $3$-SAT instance and exactly $k$ solutions in $poly(n\log k)$ ...
- 13.5k
-1
votes
1
answer
400
views
What is wrong with the argument that zero permanent is polynomial?
This Lecture summarizes some well known facts about $\#P$ completeness of permanent.
Given a CNF formula $\phi$ on $n$ variables, they construct
matrix $A$ such that:
$$perm(A)=4^{3m} \#SAT(\phi)$$
...
- 24k
0
votes
0
answers
247
views
Does "U-SAT in P" imply "P=NP"
Valiant & Vazirani proved SAT transforms UNIQUE SAT under randomized probabilistic reductions in polynomial time. Calabro et al. showed that UNIQUE k-SAT is as hard as k-SAT. Now the question is, ...
- 1
2
votes
0
answers
176
views
relationship of max-sat and min-cut in theory and practice [closed]
I have been using MAX-SAT solver to obtain the exact ground state of ising spin glass model:
For 1D periodic model, for systems with 50 binary variables and interaction range of 15th nearest ...
- 867
3
votes
3
answers
252
views
What kind of SAT am I dealing with here?
Problem set up: I have a long list of variables, $v_i$ (say about 200 total).
I am given a bunch of Boolean statements as follows:
$$\omega_1\land \omega_2\land \omega_3\land \omega_4\land \omega_5 \...
- 301
6
votes
0
answers
152
views
Complexity of finding three perfect matchings with no edge in common in a bridgeless cubic graph
According to a conjecture:
Conjecture (Fan & Raspaud, 1994) Every bridgeless cubic graph contains three perfect matchings with no edge in common.
Equivalent statement here
Main question:
...
- 24k
10
votes
1
answer
605
views
How hard is Heyting satisfiability, i.e. the constructive version of SAT? In particular, is 2-HSAT NL-complete or is it harder?
First of all, is it clear what I mean by $k$-HSAT?
I'm assuming that for $k>2$, $k$-HSAT is NP-complete, but the details of the reductions between $k$-HSAT and $k$-SAT aren't obvious to me.
I'm ...
- 447
0
votes
2
answers
811
views
Generating 3SAT circuit for Integer factorization example
I read somewhere that 3SAT can be used to solve Integer Factorization.
If that is true, could someone teach me a simple example of generating the 3SAT by using a small number? Let's say you are given ...
- 3
18
votes
7
answers
3k
views
SAT and Arithmetic Geometry
This is an agglomeration of several questions, linked by a single observation: SAT is equivalent to determining the existence of roots for a system of polynomial equations over $\mathbb{F}_2$ (note ...
- 1,358
1
vote
1
answer
301
views
Counterexamples for this algorithm for recognizing lexicographic product of graphs?
Found a possible reduction from recognizing lexicographic product of graphs to 2SAT
(since 2SAT is polynomial, the algorithm is polynomial).
Can't prove completeness of the algorithm and since it is ...
- 24k
1
vote
0
answers
86
views
Deciding / Approximating Parity of Small Depth Decision Trees
Let C be a circuit such that:
C: $\{0,1\}^n$ to $\{0,1\}$
the top most gate is a parity gate
all the inputs to the parity gate are small depth decision trees
there is a total of $2^{ log^k n}$ ...
- 35