Questions tagged [satisfiability]
Satisfiability (SAT) is the problem of determining whether there is a variable assignment that fulfills a given Boolean formula.
3
votes
0answers
23 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
55 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
25 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
40 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
29 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
390 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
32 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
339 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
20 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 ...
4
votes
1answer
35 views
MAXSAT approximation
We have been studying a 1/2-approximation for MAXSAT which runs in expected polynomial time, by randomly assigning True/False to each variable and repeating until we reach an assignment with at least ...
0
votes
0answers
19 views
What would be a good way to prove NP-Completeness of Min-satisfiablity problem
I am trying to prove the NP-Completeness of Min-satisfiability problem which can be defined as: Given a CNF formula (Set of clauses of 1 or more boolean variables) and a number x, there exists a ...
0
votes
1answer
61 views
3-DNF proves the algorithm is in P class
To understand fully, please read link
After, reading the link we will take a look at how we recover our solutions to a constrained Sudoku Puzzle.
If we assume that a sudoku puzzle was generated with ...
2
votes
2answers
74 views
Proof that POSITIVE-3-SAT is in the complexity class P
I have the following language:
$$\text{POSITIVE-3-SAT} = \{\langle\phi\rangle \mid \phi\text{ is a satisfiable boolean formula in conjunctive normal form,}\\ \text{ in which all clauses consist of ...
8
votes
2answers
2k views
Is “Reachable Object” really an NP-complete problem?
I was reading this paper where the authors explain Theorem 1, which states "Reachable Object" (as defined in the paper) is NP-complete. However, they prove the reduction only in one direction, i.e. ...
1
vote
0answers
121 views
Can someone give me the resolution procedure for 2 SAT, which is O (nˆ2)
According to Wikipedia, Even, S .; Itai, A .; Shamir, A. cited it in "On the complexity of time table and multi-commodity flow problems".
The paper can be found here: http://www.cs.technion.ac.il/...
0
votes
1answer
31 views
Resolution when clauses contain more than 1 complementary literals
Let's assume that we have clauses $(l_1 \lor l_2 \lor l_3), (\neg l_1 \lor \neg l_2 \lor l_4), (l_1 \lor l_2 \lor l_5), (\neg l_1 \lor \neg l_2 \lor l_6)$, where both $l_1$ and $l_2$ are complementary ...
0
votes
1answer
18 views
Can someone give me the definition of #Monotone-2SAT?
In the decision problem, I set all variables to true and see if the formula is satisfiable.
My question is because I do not understand how there can be multiple solutions, though all variables are ...
1
vote
0answers
52 views
The NP completeness proof for a variation of the 3CNF-SAT problem
There is a variation of 3CNF-SAT which is called 10-3-CNF-SAT = {<$\Phi$>: $\Phi$ is a satisfiable CNF formula with $\textbf{at most}$ 3 literals per clause and every variable occurs in $\textbf{at ...
0
votes
2answers
68 views
Why is Boolean satisfiability such a rare case?
In the space of all K-sat formulas, True and False should have an equal set size. For every un-Satisfiable formula (F), there will an F' (or F-prime) which will be Satisfiable by definition. I cannot ...
3
votes
2answers
77 views
Is every X3SAT instance with no cycles satisfiable?
Exactly 1 in 3 SAT (X3SAT) is a variation of the Boolean Satisfiability problem. Given a set of clauses, where each clause has three literals, is there an assignment such that in each clause exactly ...
1
vote
1answer
61 views
Counting models satisfying a boolean formula
I'm trying to implement the #2-SAT algorithm from the paper "Counting Satisfying Assignments in 2-SAT and 3-SAT" (Dahllöf, Jonsson and Wahlström, Theor. Comput. Sci. 332(1–3):265–...
1
vote
2answers
38 views
Can problems of class P be transformed into SAT formula?
I know that NP problems can be transformed into SAT (due to this fact, SAT is considered to be a NP Complete problem). I am not sure if P problems can too be transformed into SAT.
0
votes
1answer
34 views
Fine-grained complexity of 3-CNF formula evaluation
It's well known that 3-SAT is in NP, which means that one can evaluate a 3-CNF formula in polynomial time. However, I was wondering what the tightest upper bound is for formula verification, expressed ...
2
votes
2answers
35 views
Calculating the number of assignments satisfying a general propositional formula
I know, for a disjunctive clause of the form $x_1 \vee ... \vee x_i$, the number of assignments satisfying it is simply $2^i - 1$, but what about for a general formula? Is the number of satisfying ...
1
vote
1answer
16 views
For a given k-DNF formula, what is the size of the formula for the purpose of complexity?
I am currently in the process of proving some complexity bounds about k-DNF. However I am confused what the $n$ in the time complexity would refer to in this case (that is that I don't know how the "...
0
votes
0answers
26 views
Can I use the Quine-McCluskey to simplify a CNF which is not a product of maxterms?
As I understand it the Quine-McCluskey method allows you to start with a set of maxterms (or minterms), and combine them pairwise in a systematic way into a smaller set of clauses with a smaller set ...
2
votes
1answer
39 views
Refutation in first order logic
Consider the following statement
In FOL, we can reduce entailment checking to satisfiability checking:
$S \models S' \iff S \land \neg S'$ is satisfiable (This proof
strategy is called ...
1
vote
1answer
61 views
Why Cook-Levin thorem's proof can mean SAT's NP-Hardness
I'm studying about Cook-Levin theorem but there is a problem I faced. Cook-Levin theorem shows that any NPTM can be encoded as a boolean formula. About given language $A$, instance $w$, and NPTM $M$ ...
3
votes
0answers
45 views
relationship between SAT and Min-ones SAT
If SAT can be decided in polynomial time, is it clear that Min-ones SAT can be decided in polynomial time? The idea I had was to take a poly decider of SAT and try it on a formula OR'd with all ...
0
votes
1answer
53 views
Seeking nontrivial small SAT/UNSAT instances
I need SAT instances, involving 9 to 20 variables. They need to be hard to solve for humans. Both SAT and UNSAT instances are needed.
I tried random-SAT generators on the web, but the results were ...
1
vote
0answers
186 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
1answer
55 views
Reducing 3SAT to MAX-3SAT
I have the following problem:
Consider the MAX-3-SAT problem: given a Boolean function in
Conjunctive Normal Form (CNF) determine the maximum number of clauses
that can be satisfied. Prove that ...
0
votes
1answer
41 views
n-DNF boolean formula k satisfiability
Given an n variable boolean DNF formula and a number k, does this formula has satisfying input combination greater than k?. (0<=k<=2^n).
Where input is infinite number of n tuples where ...
1
vote
0answers
109 views
Is the solution to Independent Set or Vertex Cover from 3-SAT optimum?
There are plenty of resources online discussing 3-SAT reductions to Independent Set or Vertex Cover problem. I am unable to find a resource which states that a satisfiable assignment to 3-SAT results ...
1
vote
0answers
33 views
3-SAT wher each literal appears at most once [duplicate]
I'm currently following a course and we have to prove that a restricted version of the 3-SAT decision problem where each literal appears at most once is solveable in polynomial time.
I think such a ...
1
vote
1answer
46 views
Why not do these checks on the number of clauses in 3-SAT?
I've been writing a 3-SAT solver for fun and comparing its performance against the solver pycosat. My solver vastly outperforms pycosat in two special cases, where I solve by doing simple, obvious ...
1
vote
2answers
55 views
Why is Max SAT in P if SAT in P?
It holds that if SAT could be solved in poly time, one can also find in poly time the assignment that satisfies most clauses of the original formula.
Does anyone have any idea how to show this?
Let's ...
2
votes
1answer
125 views
Directed HAM Cycles with Additional Constraints to SAT
The $n$ dimensional hypercube $Q_n$ is a graph that has a vertex $v_s$ for each string $s \in \{0, 1\}^n$ and an edge between two vertices $v_s$ and $v_t$ if and only if the Hamming distance between $...
3
votes
1answer
466 views
In SAT, do we require an assignment for arbitrary variables?
I am reading about the Satisfiability Problem, in page (5) the author gives the following example :
$(P \lor Q \lor R) \wedge
(\bar{P} \lor Q \lor \bar{R}) \wedge
(P \lor \bar{Q} \lor S) \wedge
(\bar{...
0
votes
1answer
31 views
Sat instance size and definition of TIME(f(n))
Sat usually is defined as the language of a 'reasonable' encoding of satisfable Cnf formulas over n variables.
Question: a Cnf formula over n variable with m clauses has a size (as a function of n) ...
4
votes
0answers
105 views
Maximum-minimum-satisfiability [closed]
In MAX-SAT, we are given a formula and want to maximize the number of satisfied clauses. I.e., given a formula $\phi = c_1 \cap \cdots \cap c_n$, where each $c_i$ is a disjunction, we want to find the ...
1
vote
0answers
20 views
Proof that MAX-2-SAT is NP-hard [duplicate]
According to Wikipedia, while the 2SAT problem is polynomial, its maximization variant MAX2SAT is NP-hard. But, they do not provide a reference for this claim. Is this obvious? If not, where can I ...
1
vote
1answer
43 views
NP-completeness and reduction of MAX-XOR-SAT and MAX-2-XOR-SAT
It is often stated that the MAX-XOR-SAT problem is NP-hard, and that likewise is the MAX-2-XOR-SAT problem. However, I cannot find a reduction from SAT to either of these problems, nor a proof of NP-...
3
votes
1answer
20 views
General structure of solutions to 3-SAT circuits
Certain special forms of the SAT problem have solution sets of a special form. For example, given any three solutions to a 2-SAT circuit, their bitwise median is also a solution. Likewise, given any ...
3
votes
1answer
15 views
Variance of MAXSAT clause satisfiability
For a given MAXSAT problem, it is trivially easy to compute the mean number of clauses satisfied for all assignments, or equivalently the expected number of clauses satisfied by a random assignment.
...
0
votes
1answer
153 views
2SAT Problem using Implication Graph
I was doing a practice question. As you can see below there is an Implication graph. To check whether the problem is satisfiable, I checked whether there were any 'bad loops'. To do so, for each ...
4
votes
2answers
135 views
Is there a way to convert a program into a Boolean formula?
Let's say I have a program P, in form of a binary code for x86 architecture.
I want to find a Boolean formula F (in form of CNF, or something like that), such ...
-1
votes
1answer
90 views
How many solutions are there for a XOR-SAT formula? [closed]
Does anyone know how many solutions there are for a XOR-SAT formula? And how do the variables in solutions distribute? For example, if (x0=1, x1=0, x2=1) is a solution for a XOR-SAT formula, how does ...
1
vote
1answer
17 views
what does it mean to extend an assignment?
For a constraint satisfaction problem, what does it mean for an assignment x to extend an assignment a?
Sorry if this is super trivial, I did not find an answer
e.g here: No Small Linear ...
0
votes
1answer
55 views
Given a NP Algorithm for SAT, do we expect to have Correct and Incorrect Solutions?
I am reading about Boolean Satisfiability Problem and Nondeterministic Algorithms, in the latter defination it says :
In computational complexity theory, nondeterministic algorithms are ones that, ...
