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.

Filter by
Sorted by
Tagged with
1 vote
1 answer
63 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 ...
3 votes
1 answer
140 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 ...
8 votes
0 answers
227 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,396
8 votes
0 answers
232 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 ...
  • 13k
1 vote
0 answers
51 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 ...
  • 23.5k
3 votes
1 answer
571 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 ...
  • 23.5k
5 votes
1 answer
870 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 ...
  • 13k
3 votes
2 answers
200 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 ...
-1 votes
1 answer
68 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
33 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
771 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 ...
  • 721
2 votes
0 answers
61 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)$ ...
  • 13k
0 votes
0 answers
233 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)$$ ...
  • 23.5k
0 votes
0 answers
244 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
157 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 ...
  • 857
3 votes
3 answers
245 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
151 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: ...
  • 23.5k
10 votes
1 answer
575 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 ...
0 votes
2 answers
753 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,348
1 vote
1 answer
296 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 ...
  • 23.5k
1 vote
0 answers
81 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}$ ...