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
109 views

How to choose between UC and PL when using the DPLL algorithm?

We know DPLL algorithm is backtracking + unit propagation + pure literal rule. I have an example. There is one example to solve following Satisfiability problem with DPLL. if assign of "0" to ...
1
vote
1answer
44 views

Small hard 3-SAT instances

I have read various references that for 3-SAT instances with large numbers of clauses, the optimal clause/variable ratio to generate 'difficult' instances is around 4. However, I would like to know ...
-4
votes
0answers
18 views

Reductions between CNF-SAT and DNF-SAT

Can someone help me to prove or disprove the following three claims about reductions between CNF-SAT And DNF-SAT? There is polynomial reduction from CNF-SAT to DNF-SAT. There is polynomial reduction ...
1
vote
0answers
38 views

prove that the satisfiability problem with each clause containing at most 3 literals, denoted by ≤3SAT, is NP-complete

I've tried to prove it for several days but I can't make sure if it is equivalent to max-3-SAT problem? This problem seems similar to the proof of SAT ∝ 3-SAT except the case where there are more than ...
1
vote
1answer
34 views

Can QBF encode #QBF?

In another question Initializing non-deterministic variables in QBF, I was interested about translating assertion-based pseudocode to QBF in order to have an exponentially more compact encoding ...
1
vote
1answer
60 views

Initializing non-deterministic variables in QBF

I'm trying to translate the following pseudocode to QBF. The integers are encoded as simple fixed-width bitvectors, and the entire procedure runs in polynomial space ensuring QBF has enough ...
1
vote
0answers
45 views

Reduction of 3-SAT to Vertex Cover?

Can someone explain to me in the most simplest possible way, how to reduce $3-SAT$ to $Vertex\:Cover$ ? I am following the explanation here(scroll to page 4 bottom). I understand the basic setup of ...
2
votes
1answer
68 views

Satisfiability 2 CNF-SAT to 3 CNF-SAT transformation/reduction

This Reduction is trying to prove that 2CNF-SAT is also NP-Complete, after proving 3CNF-SAT is NP-Complete. If we had a reduction that given an instance of 2CNF-SAT with k clauses over 'i' number of ...
1
vote
1answer
78 views

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

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
vote
1answer
52 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
44 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
51 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
51 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
88 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
45 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
100 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
79 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
38 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
43 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
163 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
69 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
65 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
66 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
27 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
163 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
37 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 non-...
1
vote
1answer
67 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
66 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
189 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
35 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
43 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
65 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
37 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
42 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
57 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
84 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
92 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
64 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
107 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
31 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
75 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
93 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
113 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 $$f(x_1,\...
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 ...