# Questions tagged [satisfiability]

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

447 questions
Filter by
Sorted by
Tagged with
124 views

### Passing arrays vs functions as arguments in SMT?

In SAT Modulo Theories (SMT), with the theory of uninterpreted functions, all functions are first order, that is, they don't take functions as arguments or return functions. In the theory of arrays, ...
123 views

### Complexity of 1-in-3 SAT variant with restrictions on “unique” variables per clause

I'm interested in the complexity of a particular variant of 1-in-3 SAT. Assume, as is usual, that clauses are allowed to be of length 1, 2, or 3. Then add the restriction that for any clause of length ...
50 views

### Maximize the number of satisfied disjunctions

I have ~4000 variables that are used in ~5000 logical formulas, where each formula consists only of conjunctions of the (non-negated) variables. I want to find the maximum number of satisfied formulas,...
144 views

### If a CNF contains only Horn and Xor clauses, then what is the complexity of determining Satisfiability?

If a CNF contains only Horn and Xor clauses, and does not contain clauses of other types, then can its Satisfiability be determined in polynomial time?
150 views

### What is the complexity of determining Satisfiability of a CNF containing both Horn and Dual Horn clauses?

If a CNF contains both horn and dual horn clauses and does not contain clauses of other types, then can its Satisfiability always be determined in polynomial time? If the answer to the above problem ...
643 views

### How does the number of clauses affect the difficulty of a 3-SAT problem? [closed]

What is the relationship between the number of clauses and the difficulty of a 3-SAT problem?
89 views

### How to adapt DPLL to solve HORNSAT?

This question wask asked in a homework of Computer Theory in Rome, Italy. How to simplify the DPLL algorithm in order to solve HORNSAT? My Approach: I know that an Horn clause is an OR of ...
132 views

### DPLL algorithm for 3SAT [closed]

This question is from my complexity theory course. How to change the standard DPLL algorithm for SAT in order to solve 3-SAT instances? The general DPLL algorithm for SAT is defined: ...
109 views

### Solving SAT correctly on all but $poly(m)$ formulas

The question is to show that there is no deterministic polynomial time algorithm that solves SAT correctly on all but $poly(m)$ formulas of size $m$, for every $m \geq 0$ unless $P \ne NP$. I know ...
150 views

### Proving SAT is in L

How to prove that SAT is in L if and only if NP=L? I know that reducing SAT in cook-levin theorem is computable in deterministic linear space . How to do it in log space? Any reference will also help.
105 views

### NP-hardness of an extention of 2 sat

a 2 sat instance which is unsatisfiable and an integer k are given, decision problem is that: is it possible to delete k variables, also remove clauses contain them, in order to satisfy the 2-sat ...
146 views

### Is it possible to reduce a SAT problem to it's simplest form with no assumed variables in P time? [closed]

So as you read in the title I want to know if it is possible in polynomial time to reduce a SAT problem to it's simplest version in CNF format with no assumed variables? The simplest form is with ...
40 views

521 views

### Is this possible to solve boolean satisfiablility by using karnaugh maps to simplify the whole given boolean formula by simplifying subformulas?

Building karnaugh map for the whole given boolean formula always costs Θ(2n) both time and space complexities, where $n$ is the number of boolean variables in the given boolean formula. It is ...
184 views

### monotone min 3-sat polynomial algorithm?

I know that 3SAT is npc but i wonder why my little algorithm won't solve this problem: given positive 3SAT - meaning: each of the m clauses is a disjunction of 3 literals over the variables x1,…,xnx1,...
464 views

### Is this possible to solve SAT in polynomial time by reducing it to the problem of solving system of nonlinear equations?

Every conjunctive normal form (CNF) formula can be converted to nonlinear system of equations, where each clause becomes an equation in the system and: If A and B are logical/boolean variables and ...
257 views

411 views

### Is this possible to solve 4SAT in polynomial time? [closed]

I know and admit that this is long, but please read it slow and understand everything. I think that this is one of the most interesting questions asked in computer science ever. I don't expect for ...
989 views

### Is this possible to solve 3SAT in O(n^24) time and O(1) space?

Assume that n is the number variables of the given 3CNF formula (n≥3) and all clauses in the given 3CNF formula are different. That means that for each clause, each literal can be either positive ...
417 views

### 3-SAT and Systems of Nonlinear Modular Equations

How is the 3-SAT problem reduced to solving for a system of nonlinear modular equations? I have read https://stackoverflow.com/questions/4294270/how-to-prove-that-a-problem-is-np-complete in how to ...
95 views

### These sample CNF formulas in DIMACS files are in P? (Schaefer's dichotomy theorem)

Here is my earlier question. But there was no full answer. I've decided to include specific DIMACS files: http://jarvis2.hmcloud.pl/sat/cnf.formula.10 (15.8MB) http://jarvis2.hmcloud.pl/sat/cnf....
287 views

### Satisfiabililty sufficient condition?

The conjecture itself: k-SAT formula is satisfiable if no pair of unit assignment $l$ and $\overline l$ imply the formula to contain unsatisfiable (k-1)-SAT. Example (XOR-SAT has no edges and cycles ...
57 views

### Small world theorem for set constraints

Let $S_1,\dots,S_n$ be variables representing unknown sets. A set expression has the form $S_i$, $\overline{E}$ (the complement of $E$), or $E \cap E'$, where $E,E'$ are set expressions. A ...
1k views

### Unique SAT complexity clarification

Unique SAT is defined as: Given any SAT problem, does the SAT problem have exactly 1 solution? As I understand it is co-NPHard. I am unclear how it is in co-NP Assuming the problem has more than 1 ...
62 views

### Correctness of following algorithm for 3-QCNF?

Let I have 3-QCNF formula. Classic recursive algorithm for TQBF takes exponential time. However, following divide & conquer modification allows to do it in quadratic time (not sure about ...
45 views

### “Insensitive” CNF/DNF SAT always satisfying same number of clauses

I came across this paper, which mentions an interesting variation on SAT: We call a CNF formula F insensitive if every total assignment α satisfies the same number of clauses of F. I hadn't come ...