Satisfiability (SAT) is the problem of determining whether there is a variable assignment that fulfills a given Boolean formula.

learn more… | top users | synonyms (1)

1
vote
1answer
59 views

How to use an algorithm to find a satisfying assignment in polynomial time?

I am currently trying to solve the following problem but I am unsure how to go about it. The problem states: Suppose that someone gives you a polynomial-time algorithm to decide 3-SAT. Describe how ...
-1
votes
0answers
41 views

Reduction of SAT to Vertex Cover

I'm trying to understand how to reduce the below circuit-satisfiability problem into a vertex-cover problem. That is, show the resulting vertex cover graph and the number of vertices to select. Anyone ...
1
vote
1answer
47 views

Upper bound for #Monotone k-SAT

(I've recently started studying satisfiability problems. I've tried to be as clear as possible, but I'm not sure if all of the terminology used is correct.) Consider a collection of $n$ Boolean ...
1
vote
1answer
40 views

Does MiniSAT need exponential time?

I'm asking for a sequence of instances for SAT, one instance for each length, such that the sequence takes exponential time with MiniSAT.
1
vote
2answers
47 views

Variation of MAX 3-SAT

Suppose we are given a 3CNF, and we want to know whether k clauses from this 3CNF can be satisfied (k being any natural number)? I'm trying to think of an efficient algorithm to solve this problem. ...
1
vote
0answers
43 views

Modal logic axiom S4, transitive and reflexive frame, tableaux solver

I have a difficult problem to solve which as mentioned in the title is related to modal logic axiom S4. So, here is some background knowledge that can be useful: S4 axiom is a class of transitive ...
1
vote
1answer
73 views

Reducing co3SAT to UNIQUE-SAT

I am having trouble with this problem: Let N3SAT denote the non-satisfiability problem for 3CNF’s. Show that $N3SAT\leq_p UNQ$ where in UNQ, given a CNF φ we want to know whether there is a unique ...
-1
votes
1answer
40 views

Why does a satisfiable formula have a model?

I am studying Satisfiability of CNF formulas, and my lecture says that if for a certain formula there is a set of assignments such that formula is true then there is a model. My question is: Why does ...
1
vote
1answer
77 views

CNF-SAT reduction problem variant

I'm aware of the Cook-Levin theorem. I've also seen how to reduce SAT to 3-CNF SAT to show that the latter is also NP-Complete. The following problem is a variant, though, and I'm not sure how to ...
6
votes
2answers
71 views

Lower Bounds for Size of Independent Set in a Graph?

I recently learnt that for any instance of a k-SAT problem with $m$ clauses and $n$ literals , we have an assignment of literals such that at least $m(1 - 2^{-k})$ clauses are satisfied. I was ...
5
votes
1answer
167 views

Results on the difficulty of specific random 3-SAT problems?

This is a companion question to Results on number of solutions to random 3-SAT? Let $A$ and $B$ be two problems drawn from random 3-SAT, both with the same number of variables and clauses. If $A$ ...
2
votes
0answers
37 views

Results on number of solutions to random 3-SAT?

I'm looking for some published results, either empirical or theoretical, on the number of solutions to random 3-SAT problems. Given $N$ variables and a clause-to-variable ratio $\alpha$, how does the ...
2
votes
1answer
40 views

Conflict Driven Clause Learning combined with brute force

I am learning about the Conflict Driven Clause Learning method to solve SAT problems. In this method it is possible to learn clauses and add these in the set of the initial clauses. I understand a ...
6
votes
1answer
158 views

How to show ExactOneSAT is NP-Complete?

$\text{ExactOneSAT}= \{\phi\;|\;\phi\; \text{is a boolean formula}$ $\text{ such that it has a satisfying assignment with only one true literal per clause} \}$ I am trying to reduce 3SAT to this ...
1
vote
0answers
23 views

Heuristic Arguments against Existence of very inefficient alogirthm for SAT

I am reading the Handbook of Satisfiability and in the preface Martin Davis wrote Of course what is regarded as the most important problem in theoretical computer science, P = ? NP lives right ...
4
votes
2answers
64 views

Interesting small SAT problems?

I'm noodling around with making a hardware SAT solver on an FPGA, and I'm wondering if there are any interesting SAT problems smaller than, say, 50 variables both to stay within the limits of the FPGA ...
2
votes
1answer
55 views

How exactly does a Max 2 Sat reduce to a 3 Sat?

I've been reading this article which tries and explains how the max 2 sat problem is essentially a 3-sat problem and is NP-hard. However, if you see the article, I'm not able to understand why, after ...
4
votes
1answer
56 views

What happens to uninterpreted predicates in Ackermann's reduction?

I know the procedure to apply the Ackermann's reduction to a formula that doesn't involve uninterpreted predicates. But, how do we treat the uninterpreted boolean predicates? Nearly all the examples I ...
1
vote
0answers
26 views

Complexity Measure and Practical Hardness of SAT

I am study this paper "Relating Proof Complexity Measures and Practical Hardness of SAT". Here the authors propose to use pebble formulas to find a relation between these and practical SAT ...
1
vote
0answers
10 views

BDI logic or KARO framework solver - are there solvers for any new logic?

I am reading about agent logics and especially affective agents. There are BDI logics and combination of logics called KARO framework that considers those questions. All those logics seem to be ...
-1
votes
1answer
130 views

How can one reduce 3-CNF-SAT and k-CNF-SAT to each other?

I am studying for NP problems. To prove k-CNF-SAT is NP-hard, there must exists something that can be reduced to k-CNF-SAT. So what I thought is to reduce 3-CNF-SAT to k-CNF-SAT and reduce k-CNF-SAT ...
2
votes
1answer
36 views

What's non-algorithm-specific

I am reading the paper "Understanding Random SAT beyond the Clauses-to-Variables Ratio" and at beginning of the page 2 say the hardest region corresponds exactly to a phase transition in a ...
1
vote
1answer
65 views

NP to SAT. How does it works? [closed]

Let's start here: It is said that all NP problems can be reduced to SAT(boolean satisfiability problem). To be more accurate to Circuit SAT, because all decision problems like NP should end up with ...
0
votes
1answer
57 views

How can you check if a 2SAT problem has a bad loop

im trying to figure out why this is true The clauses {a,b}, {b,~c}, {c,~a} constitute a 2SAT problem with an implication graph without bad loops. Can someone show me how to illustrate this and ...
2
votes
2answers
119 views

Find hamilton cycle in a directed graph reduced to sat problem

I need to find a Hamiltonian cycle in a directed graph using propositional logic, and to solve it by sat solver. So after I couldn't find a working solution, I found a paper that describes how to ...
1
vote
0answers
32 views

Proving the following chain of implications

I'm struggling with a proof in the text for my logic course, and I'm wondering if someone could offer a hint or some help. The question is basically as follows. Show that if the decision problem for ...
2
votes
1answer
30 views

Schaefer's dichotomy theorem and reformulating 3-literal clauses

Does Schaefer's dichotomy theorem establish that a general 3-sat clause cannot be transformed into an equivalent set of 2-sat/Hornsat/affine clauses (using auxiliary variables) or just that this would ...
1
vote
1answer
42 views

Non-deterministic algorithms and Tautologies

I am studying the lecture The Complexity of Propositional Proofs. ​Here there is a definition together with a discussion (page 3). I don't understand that discussion. Let $F$ denote the set of ...
0
votes
0answers
64 views

Step by step of a modification of the Beame-Pitassi Algorithm

I am reading the paper Measuring the hardness of SAT instances by Ansótegui, Bonet, Levy and Manyà (Proc. 23rd AAAI Conf. on AI, pp. 222–228, 2008) (PDF). I am trying to ...
1
vote
1answer
22 views

Strahler of tree like refutations

I am reading the paper Measuring the hardness of SAT instances by Ansótegui, Bonet, Levy and Manyà (Proc. 23rd AAAI Conf. on AI, pp. 222–228, 2008) (PDF). I am trying to ...
2
votes
1answer
35 views

The Space of an Unsatisfiable Formula

I am reading the paper Measuring the hardness of SAT instances by Ansótegui, Bonet, Levy and Manyà (Proc. 23rd AAAI Conf. on AI, pp. 222–228, 2008) (PDF). I am trying to ...
1
vote
0answers
37 views

How to get all tree-like refutations of a formula

I need to extract all tree-like refutations of this formula $$(a+b)(a+ b')(a'+c)(a'+c')\,.$$ I get understand this one but how do I get the other ones?
2
votes
1answer
38 views

Measuring the hardness of SAT instances Lemma

I am reading the paper Measuring the hardness of SAT instances by Ansótegui, Bonet, Levy and Manyà (Proc. 23rd AAAI Conf. on AI, pp. 222–228, 2008) (PDF).I have two questions ...
3
votes
1answer
54 views

What does a square mean in a Boolean formula

I am reading the paper Measuring the hardness of SAT instances by Ansótegui, Bonet, Levy and Manyà (Proc. 23rd AAAI Conf. on AI, pp. 222–228, 2008) (PDF) and I would like to ...
5
votes
0answers
78 views

Any Natural Problems shown Easy by Reduction to Horn SAT?

To show that a problem is polynomial-time solvable, an often-successful technique is to reduce it to 2SAT (that is the problem of deciding satisfiability of CNF formulas with every clause containing ...
1
vote
1answer
84 views

Half-SAT intractability proof

I've been struggling lately with a problem that was in my last complex algorithms exam, and I can't find a solution. The problem is as follows: Half-SAT is a problem where C is a CNF boolean ...
5
votes
1answer
62 views

Complexity of black box satisfiablty

Say I have a black box $f : 2^n \to 2$ and I want to determine if it is satisfiable. That is, does there exist an input how which it returns true. I am for the purposes of this considering $n$ to be ...
1
vote
0answers
94 views

DPLL time complexity analysis

Consider the most naïve backtracking for CNF-SAT. It only checks if an assignment satisfies the input formula $\phi$ when all the $n$ variables have values assigned. Let $m$ be the size of $\phi$. ...
1
vote
1answer
30 views

Shaefer's Dichotomy Theorem [duplicate]

Could you please resolve a confusion with Schaefer's theorem for me? Namely, why does it not imply many problems in P are NP-complete? For example, primality testing surely cannot be reduced to one of ...
4
votes
0answers
73 views

“Balancing” positive and negative literals in 2-sat

I saw in an answer to this post that it is possible to construct 3-sat clauses with extra variables such that the number of positive and negative literals for each variable are equal. Does anyone ...
2
votes
1answer
92 views

Complexity of a SAT related problem

Given a set of (propositional) formulae $\Phi$, two formulae $\phi$ and $\xi$, determine whether there exists $\Psi\subseteq \Phi$ such that $\Psi\models \phi$ and $\Psi\not\models \xi$. Question: ...
6
votes
1answer
105 views

Is weighted XOR-SAT NP-hard?

Given $n$ boolean variables $x_1,\ldots,x_n$ each of which is assigned a positive cost $c_1,\ldots,c_n\in\mathbb{Z}_{>0}$ and a boolean function $f$ on these variables given in the form ...
11
votes
1answer
1k views

Why do Shaefer's and Mahaney's Theorems not imply P = NP?

I'm sure someone has thought about this before or immediately dismissed it, but why does Schaefer's dichotomy theory along with Mahaney's theorem on sparse sets not imply P = NP ? Here's my ...
0
votes
1answer
66 views

Can Tarjan's SCC algorithm find satisfying assignment to just 'any' digraph?

Is Tarjan's algorithm capable of finding satisfying assignment to any digraph consists of variables (vertices) and implications (edges)? I know that it solves implication graphs constructed by 2SAT ...
8
votes
2answers
98 views

Assignment to make formula unsatisfiable

Lets imagine we have a satisfiable formula $F(A_0, A_1,...A_k,S_0,...,S_n)$ The problem to solve is "Is there an assignment for variables $(S_0,...,S_n)$ which will make F unsatisfiable?". One way of ...
6
votes
1answer
126 views

Conflict Driven Clause Learning backtracking clarification

On the wikipedia page here it describes pretty well the CDCL algorithm (and it seems the pictures were taken from slides created by Sharad Malik at Princeton). However when describing how to backtrack ...
1
vote
1answer
131 views

Can Circuit Value Problem or HORN-SAT be reduced to PATH problem?

PATH = {(X,R,S,T) | exists an x in S that is admissible} Where R is a relation of X x X x X, S is a unary relation of X and T is a unary relation of X aswell. An x element of X is admissible if it is ...
0
votes
0answers
23 views

Arthur-Merlin protocol to decide a set size

Please look at the example here at the bottom of page 3, http://www.cs.nyu.edu/~khot/CSCI-GA.3350-001-2014/sol3.pdf Here it seems that the set whose size Arthur is trying to approximate is known in ...
2
votes
0answers
30 views

Parameterized complexity of Weighted Satisfiability with few variable occurrences

Given an integer $k$ and a Boolean CNF Formula $\phi$, Weighted Satisfiability asks whether $\phi$ is satisfiable by a model of weight $k$, i.e., a model that sets at most $k$ variables to true. This ...
2
votes
1answer
108 views

The initial NP-complete problem

It is always claimed that Cook and Levin gives the very first NP-complete problem and proof of it. But when I look at the actual proof I think what Cook and Levin did was reduced (or transformed) SAT ...