Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

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, ...