Questions tagged [satisfiability]
Satisfiability (SAT) is the problem of determining whether there is a variable assignment that fulfills a given Boolean formula.
442
questions
3
votes
1answer
33 views
Clarification on “clause learning” in DPLL algorithm
I am struggling to understand the idea of conflict-driven clause learning, in particular, I can not understand why the clause we 'learned' is a substantially new (i.e. the clause database does not ...
-1
votes
0answers
19 views
algorithm for a #SAT oracle (#SAT algorithm)
i tried to look for an algorithm that decides whether an input x is in #SAT or not.
$\#SAT$ is defined, at least in this case to be: $<\phi ,k>=\left\{\phi \:is\:a\:boolean\:formula\:with\:at\:...
2
votes
0answers
21 views
Flip Output of SAT problem [duplicate]
Why cant I Just create a TM A that runs a NTM B with a formula to compute the SAT Problem and Just Flip its Output. So when the Input NTM B Returns true (formula is satisfyable) the TM A Return false.
2
votes
1answer
41 views
Special Monotone SAT problem: NP complete?
Say we have the set $X=\{ x_1, x_2, \dots \}$ of variables. Then we consider the following problem: Is the formula
$$\bigwedge_{(a,b,c) \in A}(a \vee b \vee c) \wedge \bigwedge_{(a,b,c) \in B}(\neg a ...
3
votes
1answer
96 views
Polynomial-time linear-reduction from Directed Hamiltonian Path Problem to 3SAT
Is there a polynomial-time reduction from Directed Hamiltonian Path Problem to 3SAT which is linear in the number of vertices? That is, it reduces every directed graph $G$ with $n$ vertices to a ...
4
votes
2answers
244 views
An Exact Method for Solving Small Instances of XORSAT
I have a couple of small instances for XORSAT for which I am to design and implement an exact method. However, there are a few catches. It is guaranteed that there always exists and answer but I need ...
1
vote
0answers
78 views
Class of languages recognizable by n-bit formulas of size at most $T(n)$
A Boolean (combinatoiral) circuit is a labeled (with the labels: AND, OR, NOT, IN, OUT), directed, acyclic graph, that satisfies:
fan-in=2 for the AND and OR nodes
fan-n=1 for the NOT nodes
fan-...
0
votes
0answers
59 views
Give me ideas for an undergraduate final year math project about Boolean Satisfiability and SAT solvers
Context
I am a student starting an undergrad math project.
I was instructed to read Donald Knuth's Fascicle 6: Satisfiability and come up with ideas for a project from this material.
I have 13 weeks ...
1
vote
0answers
32 views
Are there any resources or forums online for helping me understand TAOCP?
Context
I am doing an undergrad math project that involves exploring Donald Knuth's "TAOCP, Volume 4, fascicle 6: Satisfiability".
I am having trouble parsing some of this material.
Surely there ...
2
votes
0answers
39 views
Boolean matrix / satisfiability problem [duplicate]
Let $M$ be an $m\times n$ matrix with all elements in $\{1,0\}$, $m >> n$. Let $\mathbf{v}_0, \ldots, \mathbf{v}_n$ be the columns of $M$.
I want to find all sets of columns $S = \{\mathbf{v}_{...
2
votes
1answer
50 views
Encoding set of At-Most-One constraints as a MAX-SAT problem
Assume a set of variable $V$ = $\{v_1,...,v_m\}$.
Given total $n$ at-most-one (AMO) constraints (at most one element in a given set is true) set [of the below form], over the variable set $V$,
$$ ...
1
vote
1answer
53 views
Integer programming to MAX-SAT translation
Reading A Comparison of Methods for Solving MAX-SAT
Problems, I can see that a MAX-SAT problem can be translated to an integer programming (IP) problem.
Definition of MAX-SAT [Wikipedia]:
The ...
4
votes
2answers
110 views
Is it feasible to solve this subset cover problem with SAT solver?
The problem is to find $\mathcal{S}$, a minimal collect of subsets of $\{1,\dots, 17\}$ such that the two conditions are satisfied:
if $S \subseteq \mathcal{S}$ then $|S|=6$;
for any $A \subseteq \{1,...
0
votes
0answers
24 views
CNF2 = { φ | φ is a satisfiable CNF-formula in which each variable appears at most 2 times}. Show CNF2 is in P
CNF2 = { φ | φ is a satisfiable CNF-formula in which each variable appears at most 2 times}. Show CNF2 is in P.
I found this solution:
We use the method of resolution to take the variables out ...
0
votes
0answers
67 views
CNFH = {⟨φ⟩| φ is a satisfiable cnf-formula where each clause contains any number of literals, but at most one negated literal} ∈ P
The problem derived from the book of Sipser and the question was already posted (link) with partial comments.
Let CNFH = {⟨φ⟩| φ is a satisfiable cnf-formula where each clause contains any
number ...
0
votes
0answers
64 views
Using induction prove that a K-SAT problem is NP-Complete
Using induction on k, how do I prove that the K-SAT problem is NP-complete?
On wikipedia, it describes the Cook-Levin theorem to prove that K-SAT is NPC by reducting the K-SAT problem to a circuit-...
3
votes
1answer
24 views
CNF satisfiability with a bound on number of clauses
Consider the CNF-sat problem with n literals and k clauses. If k scales linearly in n, we get np-completeness (e.g., 3-sat where each literal appears at most 4 times). Do we still get np-completeness ...
4
votes
2answers
110 views
Are SAT problems with at most two false clauses NP-complete?
Is the problem of deciding whether a SAT instance, where at most two clauses are false (that is, any given variable assignment will either lead to all clauses being true, all but one, or all but two), ...
2
votes
1answer
24 views
Significance of quantifier ordering in quantified boolean formulas (kQBF vs. QBF)
I am studying solvers of quantified boolean formulas (QBF) as a generalization of SAT solving. The standard DIMACS format of SAT specification is extended to QDIMACS, which adds "a ..." and "e
..." ...
5
votes
2answers
231 views
checking '<' for two binary numbers in a cnf-formula
I want to check whether a arbitrary binary number is less or equal to another binary number in a cnf-formula. I can already construct a formula, which is not in cnf:
Lets say n and m are two-digit ...
1
vote
1answer
38 views
Find a truth assignment of 2SAT that has the most number of true variables?
Given a 2SAT instance in CNF where each clause has at most two literals. Let $m$ be the number of clauses and $n$ be the number of variables et let $k$ be a positive number.
Question: Is there a ...
4
votes
1answer
108 views
Are SAT problems with at most one false clause NP-complete?
Is the problem of deciding whether a SAT instance, where at most one clause is false (that is, any given variable assignment will either lead to all clauses being true, or all but one), is satisfiable ...
1
vote
1answer
95 views
How to encode reachability in a graph with walls as a SAT problem
Suppose we have a graph that represents a grid of cells. We are given a cell to start in and a cell that's the destination. There are cells that we cannot enter and they are known as walls. Finally we ...
2
votes
1answer
77 views
Practical hard 3-sat instances
The $3-SAT$ problem is known to be NP-complete problem. Which means that (as far as I understand), unless $P \neq NP$, for every algorithm $A$ which decides $3-SAT$, $A$ runs in super polynomial time (...
-1
votes
2answers
75 views
A question about NP and coNP
It is an open question if NP $\neq$ Co-NP but if the conjecture were proved, this would mean that P $\neq$ NP
because P is closed under complement.
Now a fact that fails to enter my head is the ...
1
vote
0answers
82 views
Min-Ones-2-SAT getting to vertex cover
In the Min-Ones-2-SAT problem, we are given a 2-CNF formula φ and an integer k, and the objective is to decide whether there exists a satisfying assignment for φ with at most k variables set to true....
1
vote
1answer
33 views
Is inverse CNF polynomial?
Suppose we are given a CNF formula $F$ with $n$ variables and $m$ clauses. The question is whether we can represent $\lnot F$ as a CNF formula with the number of clauses polynomial in $n$ and $m$?
7
votes
1answer
614 views
Random restarts for unsatisfiable instances
In the worst case, Boolean satisfiability (assuming P!=NP) takes exponential time. Nonetheless, modern SAT solvers using variants of DPLL, are able to solve enough instances to be useful in practice.
...
1
vote
1answer
53 views
Is properly quantified 3SAT complete for PSPACE and all PH levels?
I know 3SAT is NP-complete and QSAT is PSPACE-complete. However, is it true that
$$\exists X_1 \forall X_2 \cdots Q_k X_k \colon \varphi(X_1, \ldots, X_k)$$
is complete for $\Sigma_k$, the ...
3
votes
1answer
78 views
High-dimensional geometry and P vs. NP
Background: Recently, I obtained the following equivalent problem to SAT. We are given as input a CNF formula with $n$ variables and $m$ clauses. Suppose we have an $n$-dimensional hyper-cube centered ...
0
votes
2answers
52 views
Does the naive conversion of a Boolean Formula to CNF have a polynomial or exponential complexity?
I am reading the naive conversion to CNF, this procedure is explaining in this book book, but I have not found a conplexity analysis of this algorithm:
elimination of equivalence
Elimination of ...
2
votes
1answer
40 views
CLIQUE $\leq_p$ SAT
i'm trying to reduce CLIQUE to SAT:
Given: Graph G=(Vertices V, Edges E) and $k \in \mathbb{N}$
Output: Formular F such that if G contains a complete subgraph of size k, the formular is satisfiable (...
0
votes
1answer
61 views
A doubt on converting NOT gate to CNF formula
For a NOT gate if $x_1$ is input and $x_2$ is the corresponding output, I see the equivalent CNF (conjunctive normal form) is $(x_1 \lor x_2) \land (\overline x_1 \lor \overline x_2)$.
My ...
2
votes
0answers
130 views
Second Order QBF
Consider a universe with two elements 0,1 and a second order formula, i.e. of the form "forall R exists S ... such that F", where R,S are relation symbols of some given arity, and F is some first ...
0
votes
1answer
39 views
Encoding a “not-k-out-of-n” constraint for SAT solvers
I'm finding myself needing to encode a "not-k-out-of-n" constraint in a SAT solver.
The "at-most-k-out-of-n" constraint for SAT solvers is something I can find research about -- this paper by Frisch ...
3
votes
0answers
75 views
Determine if a graph has exactly 1 cycle using a SAT solver
I have a connected undirected graph whose edges are either enabled or disabled. I want to create a set of clauses that are SAT iff all enabled edges are part of a single loop.
If I assert that each ...
5
votes
1answer
357 views
SAT algorithm for determining if a graph is disjoint
What are some good algorithms to have a SAT (CNF) solver determine if a given graph is fully-connected or disjoint?
The best one I can think of is this:
Number the nodes 1..N, where N is the number ...
0
votes
2answers
221 views
Reducing Graph Reachability to SAT (CNF)
So I came across this problem in my textbook. I was wondering how to develop a reduction from the Graph Reachability problem to SAT (CNF) problem. (i.e. formula is satisfiable iff there exists a path ...
2
votes
2answers
66 views
Prove that this language is NP-Hard
Given
$$\mathrm{\#3SAT} = \{ (w, y) \mid w\text{ is a $\mathrm{3SAT}$ instance with at least $y$ satisfying assignments}\}\,,$$
prove that $\mathrm{\#3SAT}$ is NP-Hard.
I am currently stuck with ...
4
votes
0answers
91 views
What is the generating algorithm for the “komb” instances found on satcompetition.org?
For the 2017 and 2018 Random SAT Tracks of the SAT Competition ran by the International Conference on Theory and Applications of Satisfiability Testing there are small, yet difficult, random 3-SAT ...
4
votes
2answers
108 views
Can every Turing Machine be translated into a SAT formula?
For the proof of "Cook-Levin Theorem", for a Turing Machine $M$ that accepts a language $L \in NP$ and input $x \in \{0,1\}^*$, we can create a SAT Formula, that is satisfiable if and only if $M$ ...
4
votes
0answers
39 views
Is there a correspondence of steps between DPLL and sequent-calculus?
Is there a correspondence between the steps in using DPLL to find out that a formula in propositional logic is unsatisfiable and using sequent calculus to prove that its negation is valid?
And given ...
1
vote
2answers
232 views
Reduce 4-SAT to 5-SAT
given is a reduction from 4-SAT to 5-SAT.
How is it possible to describe such a function?
I found some informations about reduction 3-SAT to 4-SAT here, but it can't help me so much.
0
votes
0answers
28 views
Is retrospective inference NP-hard?
Here is a minimal working example of the question:
Consider a network with nodes arranged in a pyramid: $1$ node in the first row, $1+d$ nodes in the second, $1+2d$ nodes in the third, and so on, ...
2
votes
0answers
43 views
Is a “stacked”, “local” version of 3-SAT NP-hard?
In this previous question, I learned that if each variable in a string $C \in 3\text{-SAT}$ appears only "locally", then finding a satisfying assignment is no longer NP-hard. My question below builds ...
2
votes
1answer
34 views
Translation of diagnosis problem to SAT
I have the following diagnosis problem:
h(A): z1 = not(in1)
h(D): z2 = not(in2)
h(B): z3 = z1 or z2
h(C): out1 = not(z3)
h(E): out2 = not(z3)
This is an image of the system:
I have an observation ...
7
votes
1answer
413 views
Is a “local” version of 3-SAT NP-hard?
Below is my simplification of part of a larger research project on spatial Bayesian networks:
Say a variable is "$k$-local" in a string $C \in 3\text{-CNF}$ if there are fewer than $k$ clauses ...
3
votes
1answer
35 views
Finding a language that is $NP^L$-complete
I'm trying to prove a theorem and as a lemma I would like to identify an $NP^L$-complete language. I was thinking something like a machine that can decide $SAT$ equipped with an oracle for $L$ can ...
4
votes
3answers
514 views
Showing that HALF-2-SAT is in P
I need to show that the following problem is in P:
$$\begin{align*}\text{HALF-2-SAT} = \{ \langle \varphi \rangle \mid \, &\text{$\varphi$ is a 2-CNF formula and there exists an assignment} \\
&...
2
votes
1answer
24 views
Satisfiability Toward A Sequential Circuit
Define a sequential circuit model be a directed graph with each vertices being a boolean gate. The difference is that we allow cycles in the boolean circuit. Each cycle will determine a boolean ...
