SAT Solver: SAT4J - оценка только подмножества предложений

Question

SAT Solver: SAT4J - оценка только подмножества предложений

У меня есть формула в файле.dimacs/.cnf, как показано ниже:

Можно ли извлечь из SAT4j только те предложения, которые содержат, например, переменные 2, 3 и 4? Затем мне нужно проверить согласованность только для этого нового набора предложений, т. Е. Для:

Я пытался использовать предположения, я пытался использовать ограничения, но я все еще не могу найти способ сделать это.

Спасибо за любое предложение.

редактировать

Я думал, что есть такой метод, как solver.addClause(clause), но наоборот solver.getClause(clause)... Хотя я кормлю решателя предложениями из файла.cnf.

Редактировать 2

Во-первых, предположения имеют одинаковый синтаксис с предложением,

val assumption: IVecInt = new VecInt(Array(1, 2))
val clause: IVecInt = new VecInt(Array(1, 2))

но переменные conjunctions в предположениях и disjunctions в пункте. Это разница. Правильно? Мои тестовые примеры говорят так. (Мне просто нужно было получить дополнительное одобрение на это).

Во-вторых, моя проблема с использованием переменных селектора:

Простая формула a V b имеет три модели:

(a, b), 
(a, -b), 
(-a, b)

Когда я добавляю переменную селектора, например, sи его предположение -sТогда у меня одинаковое количество моделей, т.е. 3 модели:

(a, b, -s),
(a, -b, -s),
(-a, b, -s)

Когда предположение trueт.е. sтогда у меня есть 4 модели вместо 0, которые я хочу:

(a, b, s), 
(a, -b, s), 
(-a, b, s), 
(-a, -b, s)

Конечно когда s = T, затем (s V a V b) = (T V a V b) = T, но это способ удаления для предложения (a V b)? Что мне нужно, так это количество моделей, реальных моделей! Есть ли способ найти точные модели при "удалении" как-то этих переменных (т.е. a а также b) что мы хотим исключить по предположению?

Для этого случая это мой текущий код в Scala:

object Example_01 {

  val solver: ISolver = new ModelIterator(SolverFactory.newDefault())
  val reader: DimacsReader = new DimacsReader(solver)
  val problem: IProblem = reader.parseInstance("example_01.cnf")    

  def main(args: Array[String]): Unit = {

    var nrModels: Int = 0
    val assumptions: IVecInt = new VecInt(Array(10))

    try {
      while(solver.isSatisfiable(assumptions)) {
        println(reader.decode(problem.model()))
        nrModels += 1
      }
    } catch {
      case e: ContradictionException => println("UnSAT: ", e)
    }

    println("The number of models is: " + nrModels)
}

Спасибо за любую помощь.

0

solver sat sat4j

Источник

user4712458 23 янв '17 в 13:49

2 ответа

Другие вопросы по тегам solver sat sat4j

user5769838 14 июн '17 в 04:23 2017-06-14 04:23 · Answer 1 · 2017-06-14 04:23

Я хотел бы добавить еще один способ. Использование блокирующего предложения.

Вы можете рассчитывать модели, перечисляя различные решения и получая точные модели. Затем вы отрицаете одно решение, соединяете его с остальной частью формулы и решаете снова. Это отрицательное предложение решения называется блокирующим предложением. Это не позволит решателю снова выбрать то же решение.

Теперь, в вашем случае, вы должны добавить предложение блокировки, которое относится только к тем переменным, которые вы хотите.

Предположим, у вас есть формула CNF

x and (y or z)

и вы получите решение x = 1, y = 1, z = 0.

Но, скажем, вы заинтересованы в x а также z только.

Из этого решения предложение о блокировке будет

!(x and !z)

Это запретит решение

x = 1, y = 1, z = 0, а такжеx = 1, y = 0, z = 0

Вы получите только одно решение

x = 1, z = 1 (y не имеет значения)

Надеюсь это поможет.

Если вы используете какой-то счетчик модели, найдите опцию добавления переменных проекции (иногда их также называют независимыми переменными). Вы в основном хотите проецировать все решения на подмножество переменных. Различные комбинации других переменных не должны влиять на количество моделей.

user3867609 25 янв '17 в 13:23 2017-01-25 13:23 · Answer 2 · 2017-01-25 13:23

Чтобы продолжить, нужно добавить в каждое предложение новую переменную селектора.

p cnf 15 9
7 1 0
8 -2 1 0
9 -1 2 0
10 -5 1 0
11 -6 1 0
12 -3 2 0
13 -4 2 0
14 -3 -4 0
15 3 4 -2 0

И тогда вам просто нужно присвоить дополнительную переменную true, чтобы отбросить предложение, и false, чтобы включить его, как допущения. В вашем случае предположение будет 7,-8,-9,10,11,-12,-13,14,-15.

Это не характерно для Sat4j, это способ продолжить, предложенный первоначально minisat, и который предоставляет большинство решателей SAT.

редактировать 2:

Вот способ использовать предположения и подсчет моделей

    ISolver solver = SolverFactory.newDefault();
    ModelIterator iterator = new ModelIterator(solver);
    iterator.newVar(2); // for a and b
    int selector = iterator.nextFreeVarId(true);
    assert selector == 3;
    IVecInt clause = new VecInt();
    // (a, b),
    clause.push(1).push(2);
    solver.addClause(clause);
    clause.clear();
    // (s, -a, -b)
    clause.push(-1).push(-2).push(3);
    solver.addClause(clause);
    clause.clear();
    IVecInt assumptions = new VecInt();
    // we activate the second clause in the solver
    assumptions.push(-3);
    while (iterator.isSatisfiable(assumptions)) {
        System.out.println("1:>" +new VecInt(iterator.model()));
    }
    assert iterator.numberOfModelsFoundSoFar() == 2;
    // need to reset the solver, since iterating over the model
    // adds new constraints in the solver
    iterator.reset();
    clause = new VecInt();
    // (a, b),
    clause.push(1).push(2);
    solver.addClause(clause);
    clause.clear();
    // (s, -a, -b)
    clause.push(-1).push(-2).push(3);
    solver.addClause(clause);
    clause.clear();
    // we disable the second clause in the solver
    assumptions.clear();
    assumptions.push(3);
    while (iterator.isSatisfiable(assumptions)) {
        System.out.println("2:>" + new VecInt(iterator.model()));
    }
    assert iterator.numberOfModelsFoundSoFar() == 3;
}