SAT stands for the Boolean satisfiability problem.
5
votes
2answers
63 views
What are the current best upper bounds of #P?
#P is the class of counting problems for problems in NP. In other words, a solution to #P returns the number of solutions to a particular problem in NP.
I'm wondering if there have been any studies ...
-1
votes
0answers
26 views
how to run minisat+ sat solver [closed]
I downloaded the minisat+zip file
I extracted the zip.According to install file i run
make rx
but i have the following result:
...
-4
votes
0answers
46 views
Start using SAT Solvers [migrated]
What i actually want to do is to turn a math problem ,i have to solve,to a Boolean Satisfiability problem and solve it using a SAT Solver.
I wonder if someone knows any manual,guide or anything that ...
3
votes
1answer
144 views
How is this graphical representation of SAT/CSP instances called?
Given a CNF formula (SAT problem), we can construct the constraint/dependency graph, which contains a vertex for each variable and a hyperedge for each clause. Same goes for CSPs, where we have a ...
2
votes
0answers
45 views
How fast can we group clauses with few variables in common in k-SAT?
Given a k-SAT problem with $C$ clauses and $V$ variables, we can group the clauses together into groups of $g$ clauses with few exceptions, where the exceptions contain $g-1$ or fewer clauses. If we ...
1
vote
1answer
66 views
Implied Clause and Resolvent
(I posted this question on MathSE first, no answer, that is the reason why I come here.)
Let $F$ be a 3-CNF formula on $n$ variables. A clause $c$ is implied by the formula if $F$ and $F \wedge c$ ...
10
votes
2answers
434 views
Restricted Monotone 3CNF formula: counting satisfying assignments (both modulo $2^n$ and modulo $2$)
Consider a Monotone 3CNF formula having both the following additional restrictions:
Every variable appears in exactly $2$ clauses.
Given any $2$ clauses, they share at most $1$ variable.
I would ...
7
votes
1answer
100 views
How do I use canonical ordering to reduce symmetry in the SAT encoding of the pigeonhole problem?
In the paper "Efficient CNF Encoding for Selecting 1 from N Objects", the authors introduce their "commander variable" technique for encoding the constraint, and then talk about the pigeonhole ...
5
votes
0answers
199 views
The latest concerning Valiant-Vazirani
I'm wondering what the best method obtained for the Valiant-Vazirani theorem is. We can state the following criteria:
(1) First and foremost, has anyone been able to derandomize it?
(2) If not, ...
8
votes
1answer
830 views
About Inverse 3-SAT
Context: Kavvadias and Sideri have shown that the Inverse 3-SAT problem is coNP Complete:
Given $\phi$ a set of models on $n$ variables, is there a 3-CNF formula such that $\phi$ is its exact set of ...
3
votes
1answer
109 views
About Closure under Resolution
The question looks very simple, that is why I posted it first on MathSE, unsuccesfully - no answer for 12 days. I tried to find a short and elegant answer to the question, but I haven't succeed yet. ...
10
votes
1answer
215 views
A 3-CNF formula that requires resolution width $5$
Recall that the width of a resolution refutation $R$ of a CNF formula $F$ is the maximal number of literals in any clause occurring in $R$. For every $w$, there are unsatisfiable formulas $F$ in ...
0
votes
0answers
119 views
How to figure out the number of variables that need to be set to solve SAT problem [closed]
The question is, how does the number of variables that need to be set in $\text{k-SAT}$ problems depend on the number of literals and variables? Or is this currently unknwon?
(In some SAT problem, ...
27
votes
0answers
436 views
Problem unsolvable in $2^{o(n)}$ on inputs with $n$ bits, assuming ETH?
If we assume the Exponential-Time Hypothesis, then there is no $2^{o(n)}$ algorithm for $n$-variable 3-SAT, and many other natural problems, such as 3-COLORING on graphs with $n$ vertices. Notice ...
3
votes
0answers
88 views
Hardness of Horn-modulated Satsifiability problem?
It is known that there is sharp complexity jump between Horn 3-SAT and 3-SAT problems. The former is $P$-complete while the later is $NP$-complete. I would like to see a continuous spectrum of ...
6
votes
2answers
182 views
Inappoximability status of Max One in Three SAT for satisfiable instances
What is the inapproximability status of Max-One-in-Three SAT for satisfiable instances?
7
votes
1answer
216 views
What are the #P-complete subfamilies of #2-SAT?
Short version.
The original proof that #2-SAT is #P-complete shows, in fact, that those instances of #2-SAT which are both monotone (not involving the negations of any variables) and bipartite (the ...
3
votes
1answer
123 views
Constraint satisfaction problem on a graph
Consider the set $S = \{1, \dots, n\}$ and $n$ subsets $S_i \subseteq S$ of size $d$ each (think of $S_i$ as neighborhoods of vertex $i$ in some $d$-regular graph, although the graph structure is not ...
3
votes
2answers
161 views
What is the best-known inapproximability result for MIN-3CNF-DELETION?
I am really curious what the best-known inapproximability result is for MIN-3CNF-DELETION. To clarify, this is the problem of minimizing the number of unsatisfied clauses in a CNF
SAT formula with at ...
0
votes
1answer
219 views
Counting reduction from #SAT to #HornSAT?
Is it possible to find a counting reduction from #SAT to #HornSAT? I haven't found this question posted here, so decided to check if anyone has any answer to this. Let me explain what do I mean by ...
-3
votes
1answer
283 views
Help proving a 3CNF related prob. is in P
I need help proving that this problem is decidable in polynomial-time:
Input: a 3CNF formula with more than one clause.
Question: can the formula be divided into two satisfiable 3CNF formulas ?
...
6
votes
1answer
106 views
When we use a proof of unsatisfiability to derive an interpolant, isn't using the interpolant to check satisfiability now redundant?
A few papers I've been reading have algorithms on using interpolants for the following clauses (bounded model checking):
$$ \begin{align*}
A &= I \wedge T_1 \\
B &= T_2 \wedge T_3 \wedge ...
7
votes
1answer
452 views
Checking formulas with two quantifiers ($\forall \exists$) - 2QBF
SAT solvers give a powerful way to check the validity of a boolean formula with one quantifier.
For instance, to check the validity of $\exists x . \varphi(x)$, we can use a SAT solver to determine ...
2
votes
1answer
179 views
Reduction/transformation from MinCostSat to MaxSat
I recently ran into MaxSAT competitions website and was looking into the problem formulation. I vaguely remember reading somewhere that MinCostSAT and MaxSAT are related to each other and one can be ...
6
votes
1answer
277 views
More efficient Cook-Levin reduction
In the Arora-Barak book, in the Cook-Levin reduction, the resulting SAT formula is of size $T(n)\log(T(n))$, where $T(n)$ is the running time of the given Turing machine.
Is there a method to get a ...
3
votes
2answers
204 views
Finding the Length of the shortest Accepting path of a NDTM
Let $M$ be a NDTM (non deterministic Turing machine) which decides a certain NP-complete language, say SAT.
$M$ computes any instance $I$ of the NP-complete problem in at most $p(n)$ non ...
9
votes
1answer
320 views
Context-sensitive grammar for SAT?
By a classic result of Kuroda, the complexity class NSPACE[$n$] (also known as NLIN-SPACE) is precisely the class CSL of context-sensitive languages. The satisfiability problem SAT is in NSPACE[$n$], ...
25
votes
2answers
682 views
Ladner's Theorem vs. Schaefer's Theorem
While reading the article "Is it Time to Declare Victory in Counting Complexity?" over at the "Godel's Lost Letter and P=NP" blog, they mentioned the dichotomy for CSP's. After some link following, ...
13
votes
3answers
488 views
Shortest Equivalent CNF Formula
Let $F_1$ be a satisfiable CNF Formula with $n$ variables and $m$ clauses. Let $S_{F_1}$ be the solution space of $F_1$.
Consider the problem of determining, given $F_1$, another CNF Formula $F_2$ ...
9
votes
2answers
546 views
Are quasi-polynomial sized circuits for 3-SAT trivial?
Suppose we consider 3-SAT with $v$ variables and $c$ clauses. I am researching a method that appears to take $O(v^{2+\log c})$ time/space to solve any SAT problem fitting this description, to within ...
-1
votes
1answer
133 views
What is known about NP hard problems that access preprocessed information?
Please accept my apologies ahead of time since I fear that this isn't an adequate question for cstheory. I plan on releasing my ideas to get feedback, but I don't know if my target audience will ...
6
votes
2answers
231 views
The worst-case scenario(s) for MAX3E SAT
MAX3E SAT is defined as SAT with all clauses consisting of 3 literals and their possible negations. We define clause counting, for this question, as the ability to count the total number of satisfied ...
0
votes
0answers
201 views
On Vertex Coloring of Permutation Graph and Comparability Graph and 2-SAT
I have 2 questions.
Firstly, I am not sure about differences between Permutaion Graphs and Comparability Graphs. The latter graph class includes the other class. Is there a specific example of graph ...
1
vote
1answer
135 views
How the Number of Clauses Change the Complexity of Worst Case k-SAT ?
Is there a conjecture such that if the conjecture holds then the following (1) and (2) hold ?
(1)The worst case time complexity of k-SAT with n variables and m clauses reaches the maximum value, if m ...
1
vote
1answer
181 views
Can an oracle allowing errors be non-relativizing?
I am experimenting with k-SAT. I'm using an oracle that returns the total number of satisfiable truth assignments, which is in #P. The interest here is that this total is returned modulo a natural ...
6
votes
1answer
275 views
Consequences of sub-exponential proofs/algorithms for SAT
Would there be any major consequences if SAT had at most subexponential unsat proofs or even more strongly, SAT had subexponential-time algorithms?
12
votes
1answer
498 views
Ranking the Difficulty of NP Hard Problems in Practice
This question is tightly related to another post: Phase Transitions in NP Hard Problems but it is somewhat different. While that question is about the hardness of particular instances of NP hard ...
12
votes
4answers
383 views
Are there any algorithms for SAT solving which are not DPLL based?
Are there any algorithms for SAT solving which are not DPLL based?
Or are all algorithms used by SAT solvers are DPLL based?
5
votes
2answers
313 views
minimum true monotone 3SAT
I am interested in a SAT variation where the CNF formula is monotone (no variables are negated). Such a formula is obviously satisfiable.
But say the number of true variables is a measure of how ...
5
votes
1answer
325 views
How many tautologies are there?
Given m, n, k how many of k-DNFs with n variables and m clauses are tautology? (or how many K-CNFs are unsatisfiable?)
6
votes
1answer
462 views
Complexity of Exactly $A$-SAT
Let define the "Exactly $A$-SAT" problem : Given a CNF formula $F$ and a set $A$ of positive integers, is it true that the number of models of $F$ is in $A$?
What is the complexity of Exactly ...
10
votes
1answer
847 views
Unique SAT vs Exactly $m$ models
Unique SAT is the well known problem : given a CNF formula $F$, is it true that $F$ has exactly one model ?
I am interested in « Exactly $m$-SAT » problem : given a CNF formula $F$ and an integer ...
7
votes
2answers
541 views
A variant of Critical SAT in DP
A language $L$ is in the class $DP$ iff there are two languages $L1 \in NP$ and $L2 \in coNP$ such that $L = L1 \cap L2$
A canonical $DP$-complete problem is SAT-UNSAT : given two 3-CNF expressions, ...
16
votes
1answer
886 views
Minimum Unsatisfiable 3-CNF Formulae
I am currently interested in obtaining (or constructing) and studying 3-CNF formulae which are unsatisfiable, and are of minimum size. That is, they must consist of as few clauses (m = 8 preferably) ...
12
votes
1answer
413 views
A topological space related to SAT: is it compact?
The Satisfiability problem is, of course, a fundamental problem in theoretical CS. I was playing with one version of the problem with infinitely many variables. $\newcommand{\sat}{\mathrm{sat}} ...
1
vote
1answer
244 views
1- in -$k$ SAT to $k$-SAT reduction
The reduction from $k$-SAT to 1-in-$k$ SAT is known.
Would you help me to find a reduction from 1-in-$k$ SAT to $k$-SAT ? Thanks.
-2
votes
1answer
556 views
Solving $n$-SAT and #$n$-SAT
Let $F$ be an $n$–SAT formula on $n$ variables (ie a CNF formula containing exclusively total clauses, with all variables in each), and let $c$ be the number of different clauses in $F$ ($c \le 2^n$).
...
6
votes
2answers
495 views
4
votes
1answer
227 views
Approximating Random MAX-k-SAT
It is known [de la Vega & Karpinski 2002] that random instances of MAX-3-SAT on $n$ variables can be approximated up to fraction at least 8/9 w.h.p. tending to 1 as $n$ tends to infinity.
Should ...
11
votes
0answers
343 views
DPLL and Lovász Local Lemma
Let $\varphi$ be a CNF formula. Suppose that each of $\varphi$'s clauses consist of exactly $t$ literals (and, moreover, all literals within one particular clause correspond to different variables). ...
