SAT Solver

sugar - CSP を CNF にして、SAT ソルバに解かせてくれる

 glucose - 2016 SAT compeitition で Silver. Sugar で default.

minisat-inc - minisat の インクリメンタルバージョン. Sugar で default

 

Sugar でパズル解いてるやつ

http://bach.istc.kobe-u.ac.jp/sugar/puzzles/sugar-puzzles.pdf
ナンリンは15x15でダメ

 

 

ライブラリを追加したら ldconfig する

/etc/ld.so.conf で指定される共有ライブラリに、新しくファイルを加えた時は、ldconfig を実行して、/etc/ld.so.cache にキャッシュされているライブラリリストを更新する必要がある。

double, long double で切り下げた場合の結果が異なる

#include <stdio.h>

void show(long double x) {
  char result[10];
  __asm__("fldl %1\n\t"
          "fstpt %0\n\t"
          : "=m"(result)
          : "m"(x));
  int bits = 0;
  for (int i = 9; i >= 0; i--) {
    for (int j = 7; j >= 0; j--) {
      printf("%d", (result[i] >> j & 1) != 0);
      bits++;
      if (bits == 1 || bits == 16) {
        printf(" ");
      }
    }
  }
  printf("\n");
}

int main() {
  long double a = 0.53;
  long double b = 0.53L;
  show(a);
  show(b);

  long double c = a * 100.0;
  long double d = b * 100.0;
  show(c);
  show(d);

  // 52 53
  printf("%d %d\n", (int)(c), (int)(d));
}

上記のコードの出力は次のようになる。(x86_64 + gcc 5.4.0)

1 011110001111010 1111000010100011110101110000101000111101100000000000000000000000  # 真の値より大きい
1 011110001111010 1111000010100011110101110000101000111101011100001010000000000000  # 真の値より小さい
1 100000101000000 1000000000000000000000000000000000000000000110000000000000000000
1 100000100111111 1111111111111111111111111111111111111111111111111111100000000000
53 52

long double は、指数部 15 bit, 仮数部 63 bit の extended precision によって計算される。
double の仮数部は 52 bit なので、桁落ちする位置が異なり、偶数丸めによって、切り上げられたり切り下げられたりする。

参考:

Rust で Dijkstra

こんな感じかなあ。負にならない値はできるだけ usize を使うと、Vec へのアクセスでキャストせずに済んでよさそう? 動くコード:https://ideone.com/3yRoBI

use std::collections::BinaryHeap;

type Cell = (usize, usize);

#[inline]
fn neighbors((x,y): Cell, h: usize, w: usize) -> Vec<Cell> {
    let mut res = vec![];
    if x + 1 < h {
        res.push((x+1, y));
    }
    if y + 1 < w {
        res.push((x, y+1));
    }
    if x > 0 {
        res.push((x-1, y));
    }
    if y > 0 {
        res.push((x, y-1));
    }
    res
}

type State = (usize, Cell);

fn main() {
    let maze = vec![
        ".#....",
        "...##.",
        "#.#...",
        "..#.#.",
        ".#...#",
        "...#.."
    ];
    let start = (0,0);
    let h = maze.len();
    let w = maze[0].len();
    let goal = (h-1, w-1);
    
    let mut queue = BinaryHeap::<State>::new();
    queue.push((0, start));
    let inf = 100;
    let mut steps = vec![vec![inf; w]; h];
    loop {
        match queue.pop() {
            None => break,
            Some((step, c)) => {
                // これが気になる
                if maze[c.0].chars().nth(c.1) == Some('#') || steps[c.0][c.1] < inf {
                    continue;
                }
                steps[c.0][c.1] = step;
                for nc in neighbors(c, h, w) {
                    queue.push((step + 1, nc));
                }
            }
        }
    }
    println!("{}", steps[goal.0][goal.1]);
}