Le problème général SAT (booléen satisfibility) est NP-complet. Mais 2-SAT , où chaque clause ne dispose que de deux variables est en P . Écrivez un solveur pour 2-SAT.

Contribution:

Une instance 2-SAT, codée en CNF comme suit. La première ligne contient V, le nombre de variables booléennes et N, le nombre de clauses. Ensuite, N lignes suivent, chacune avec 2 entiers non nuls représentant les littéraux d'une clause. Les entiers positifs représentent la variable booléenne donnée et les entiers négatifs représentent la négation de la variable.

Exemple 1

contribution

4 5
1 2
2 3
3 4
-1 -3
-2 -4

qui code la formule (x ₁ ou x ₂ ) et (x ₂ ou x ₃ ) et (x ₃ ou x ₄ ) et (pas x ₁ ou pas x ₃ ) et (pas x ₂ ou pas x ₄ ) .

Le seul paramètre des 4 variables qui rend la formule entière vraie est x ₁ = faux, x ₂ = vrai, x ₃ = vrai, x ₄ = faux , donc votre programme devrait sortir la seule ligne

production

0 1 1 0

représentant les valeurs de vérité des variables V (dans l'ordre de x ₁ à x _V ). S'il existe plusieurs solutions, vous pouvez générer n'importe quel sous-ensemble non vide, une par ligne. S'il n'y a pas de solution, vous devez sortir UNSOLVABLE.

Exemple 2

contribution

2 4
1 2
-1 2
-2 1
-1 -2

production

UNSOLVABLE

Exemple 3

contribution

2 4
1 2
-1 2
2 -1
-1 -2

production

0 1

Exemple 4

contribution

8 12
1 4
-2 5
3 7
2 -5
-8 -2
3 -1
4 -3
5 -4
-3 -7
6 7
1 7
-7 -1

production

1 1 1 1 1 1 0 0
0 1 0 1 1 0 1 0
0 1 0 1 1 1 1 0

(ou tout sous-ensemble non vide de ces 3 lignes)

Votre programme doit gérer tous les N, V ​​<100 dans un délai raisonnable. Essayez cet exemple pour vous assurer que votre programme peut gérer une grande instance. Le plus petit programme gagne.

Haskell, 278 caractères

(∈)=elem
r v[][]=[(>>=(++" ").show.fromEnum.(∈v))]
r v[]c@(a:b:_)=r(a:v)c[]++r(-a:v)c[]++[const"UNSOLVABLE"]
r v(a:b:c)d|a∈v||b∈v=r v c d|(-a)∈v=i b|(-b)∈v=i a|1<3=r v c(a:b:d)where i w|(-w)∈v=[]|1<3=r(w:v)(c++d)[]
t(n:_:c)=(r[][]c!!0)[1..n]++"\n"
main=interact$t.map read.words

Pas de force brute. Fonctionne en temps polynomial. Résout le problème difficile (60 variables, 99 clauses) rapidement:

> time (runhaskell 1933-2Sat.hs < 1933-hard2sat.txt)
1 1 1 0 0 0 0 0 0 1 1 0 0 1 0 1 1 1 0 1 1 0 0 1 0 0 1 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 1 0 0 1 0 1 0 0 0 0 1 0 1 1 1 1 0 

real 0m0.593s
user 0m0.502s
sys  0m0.074s

Et en fait, la plupart de ce temps est consacré à la compilation du code!

Fichier source complet, avec cas de test et tests de vérification rapide disponibles .

Non golfé:

-- | A variable or its negation
-- Note that applying unary negation (-) to a term inverts it.
type Term = Int

-- | A set of terms taken to be true.
-- Should only contain  a variable or its negation, never both.
type TruthAssignment = [Term]

-- | Special value indicating that no consistent truth assignment is possible.
unsolvable :: TruthAssignment
unsolvable = [0]

-- | Clauses are a list of terms, taken in pairs.
-- Each pair is a disjunction (or), the list as a whole the conjuction (and)
-- of the pairs.
type Clauses = [Term]

-- | Test to see if a term is in an assignment
(∈) :: Term -> TruthAssignment -> Bool
a∈v = a `elem` v;

-- | Satisfy a set of clauses, from a starting assignment.
-- Returns a non-exhaustive list of possible assignments, followed by
-- unsolvable. If unsolvable is first, there is no possible assignment.
satisfy :: TruthAssignment -> Clauses -> [TruthAssignment]
satisfy v c@(a:b:_) = reduce (a:v) c ++ reduce (-a:v) c ++ [unsolvable]
  -- pick a term from the first clause, either it or its negation must be true;
  -- if neither produces a viable result, then the clauses are unsolvable
satisfy v [] = [v]
  -- if there are no clauses, then the starting assignment is a solution!

-- | Reduce a set of clauses, given a starting assignment, then solve that
reduce :: TruthAssignment -> Clauses -> [TruthAssignment]
reduce v c = reduce' v c []
  where
    reduce' v (a:b:c) d
        | a∈v || b∈v = reduce' v c d
            -- if the clause is already satisfied, then just drop it
        | (-a)∈v = imply b
        | (-b)∈v = imply a
            -- if either term is not true, the other term must be true
        | otherwise = reduce' v c (a:b:d)
            -- this clause is still undetermined, save it for later
        where 
          imply w
            | (-w)∈v = []  -- if w is also false, there is no possible solution
            | otherwise = reduce (w:v) (c++d)
                -- otherwise, set w true, and reduce again
    reduce' v [] d = satisfy v d
        -- once all caluses have been reduced, satisfy the remaining

-- | Format a solution. Terms not assigned are choosen to be false
format :: Int -> TruthAssignment -> String
format n v
    | v == unsolvable = "UNSOLVABLE"
    | otherwise = unwords . map (bit.(∈v)) $ [1..n]
  where
    bit False = "0"
    bit True = "1"

main = interact $ run . map read . words 
  where
    run (n:_:c) = (format n $ head $ satisfy [] c) ++ "\n"
        -- first number of input is number of variables
        -- second number of input is number of claues, ignored
        -- remaining numbers are the clauses, taken two at a time

Dans la version golf, satisfyet formatont été intégrés reduce, bien que pour éviter de passer n, reducerenvoie une fonction d'une liste de variables ( [1..n]) au résultat de la chaîne.

• Edit: (330 -> 323) fait sun opérateur, une meilleure gestion de la nouvelle ligne
• Edit: (323 -> 313) le premier élément d'une liste de résultats paresseux est plus petit qu'un opérateur de court-circuit personnalisé; renommé fonction de solveur principal parce que j'aime utiliser ∮comme opérateur!
• Modifier: (313 -> 296) garder les clauses comme une seule liste, pas une liste de listes; traiter deux éléments à la fois
• Edit: (296 -> 291) a fusionné les deux fonctions mutuellement récursives; il était moins cher de s'aligner, ★donc le test est maintenant renommé∈
• Modifier: (291 -> 278) formatage de sortie intégré dans la génération des résultats

J, 119 103

echo'UNSOLVABLE'"_`(#&c)@.(*@+/)(3 :'*./+./"1(*>:*}.i)=y{~"1 0<:|}.i')"1 c=:#:i.2^{.,i=:0&".;._2(1!:1)3

• Réussit tous les cas de test. Aucun temps d'exécution notable.
• Force brute. Réussit les cas de test ci-dessous, oh, N = 20 ou 30. Pas sûr.
• Testé via un script de test complètement cérébral (par inspection visuelle)

Edit: Éliminé (n#2)et donc n=:, ainsi que l'élimination de certaines parens de rang (merci, isawdrones). Tacite-> explicite et dyadique-> monadique, éliminant chacun quelques caractères supplémentaires. }.}.à }.,.

Edit: Oups. Non seulement c'est une non-solution pour les grands N, mais i. 2^99x-> "erreur de domaine" pour ajouter l'insulte à la stupidité.

Voici la version originale non golfée et une brève explication.

input=:0&".;._2(1!:1)3
n =:{.{.input
clauses=:}.input
cases=:(n#2)#:i.2^n
results =: clauses ([:*./[:+./"1*@>:@*@[=<:@|@[{"(0,1)])"(_,1) cases
echo ('UNSOLVABLE'"_)`(#&cases) @.(*@+/) results

• input=:0&".;._2(1!:1)3 coupe les entrées sur les nouvelles lignes et analyse les nombres sur chaque ligne (en accumulant les résultats en entrée).
• n est affecté à n, matrice de clause affectée à clauses(n'a pas besoin du nombre de clauses)
• casesest 0..2 ⁿ -1 converti en chiffres binaires (tous les cas de test)
• (Long tacit function)"(_,1)est appliqué à chaque cas casesavec tous clauses.
• <:@|@[{"(0,1)] obtient une matrice des opérandes des clauses (en prenant abs (op number) - 1 et en déréférençant de case, qui est un tableau)
• *@>:@*@[ obtient un tableau en forme de clause de bits 'not not' (0 pour not) via un abus de signum.
• = applique les bits non aux opérandes.
• [:*./[:+./"1s'applique +.(et) à travers les lignes de la matrice résultante, et *.(ou) à travers le résultat de cela.
• Tous ces résultats se retrouvent sous la forme d'un tableau binaire de «réponses» pour chaque cas.
• *@+/ appliqué aux résultats donne un 0 s'il y a des résultats et 1 s'il n'y en a pas.
• ('UNSOLVABLE'"_) `(#&cases) @.(*@+/) results exécute une fonction constante donnant 'UNSOLVABLE' si 0, et une copie de chaque élément 'solution' des cas si 1.
• echo imprime le résultat par magie.

K - 89

La même méthode que la solution J.

n:**c:.:'0:`;`0::[#b:t@&&/+|/''(0<'c)=/:(t:+2_vs!_2^n)@\:-1+_abs c:1_ c;5:b;"UNSOLVABLE"]

Rubis, 253

n,v=gets.split;d=[];v.to_i.times{d<<(gets.split.map &:to_i)};n=n.to_i;r=[1,!1]*n;r.permutation(n){|x|y=x[0,n];x=[0]+y;puts y.map{|z|z||0}.join ' 'or exit if d.inject(1){|t,w|t and(w[0]<0?!x[-w[0]]:x[w[0]])||(w[1]<0?!x[-w[1]]:x[w[1]])}};puts 'UNSOLVABLE'

Mais c'est lent :(

Assez lisible une fois étendu:

n,v=gets.split
d=[]
v.to_i.times{d<<(gets.split.map &:to_i)} # read data
n=n.to_i
r=[1,!1]*n # create an array of n trues and n falses
r.permutation(n){|x| # for each permutation of length n
    y=x[0,n]
    x=[0]+y
    puts y.map{|z| z||0}.join ' ' or exit if d.inject(1){|t,w| # evaluate the data (magic!)
        t and (w[0]<0 ? !x[-w[0]] : x[w[0]]) || (w[1]<0 ? !x[-w[1]] : x[w[1]])
    }
}
puts 'UNSOLVABLE'

OCaml + Batteries, 438 436 caractères

Nécessite un OCaml Batteries inclus de niveau supérieur:

module L=List
let(%)=L.mem
let rec r v d c n=match d,c with[],[]->[String.join" "[?L:if x%v
then"1"else"0"|x<-1--n?]]|[],(x,_)::_->r(x::v)c[]n@r(-x::v)c[]n@["UNSOLVABLE"]|(x,y)::c,d->let(!)w=if-w%v
then[]else r(w::v)(c@d)[]n in if x%v||y%v then r v c d n else if-x%v then!y else if-y%v then!x else r v c((x,y)::d)n
let(v,_)::l=L.of_enum(IO.lines_of stdin|>map(fun s->Scanf.sscanf s"%d %d"(fun x y->x,y)))in print_endline(L.hd(r[][]l v))

Je dois avouer que c'est une traduction directe de la solution Haskell. Pour ma défense, qui à son tour est un codage directe de l'algorithme présenté ici [PDF], avec la mutuelle satisfy- eliminaterécursion roulé en une seule fonction. Une version non obscurcie du code, sans l'utilisation de piles, est:

let rec satisfy v c d = match c, d with
| (x, y) :: c, d ->
    let imply w = if List.mem (-w) v then raise Exit else satisfy (w :: v) (c @ d) [] in
    if List.mem x v || List.mem y v then satisfy v c d else
    if List.mem (-x) v then imply y else
    if List.mem (-y) v then imply x else
    satisfy v c ((x, y) :: d)
| [], [] -> v
| [], (x, _) :: _ -> try satisfy (x :: v) d [] with Exit -> satisfy (-x :: v) d []

let rec iota i =
    if i = 0 then [] else
    iota (i - 1) @ [i]

let () = Scanf.scanf "%d %d\n" (fun k n ->
    let l = ref [] in
    for i = 1 to n do
        Scanf.scanf "%d %d\n" (fun x y -> l := (x, y) :: !l)
    done;
    print_endline (try let v = satisfy [] [] !l in
    String.concat " " (List.map (fun x -> if List.mem x v then "1" else "0") (iota k))
    with Exit -> "UNSOLVABLE") )

(le iota kjeu de mots j'espère que vous pardonnerez).