OKlibrary  0.2.1.6
UnitClausePropagation.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 23.12.2008 (Schwalbach) */
00002 /* Copyright 2008, 2009 Oliver Kullmann
00003 This file is part of the OKlibrary. OKlibrary is free software; you can redistribute
00004 it and/or modify it under the terms of the GNU General Public License as published by
00005 the Free Software Foundation and included in this library; either version 3 of the
00006 License, or any later version. */
00007 
00022 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/PartialAssignments.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/SetSystems.mac")$
00025 
00026 /* The most basic algorithm for unit-clause propagation, input a clause-set,
00027    output the reduced clause-set.
00028 */
00029 ucp_0_cs(F) := block([U],
00030   do (
00031     if empty_element_p(F) then return({{}}),
00032     if emptyp(U : lunion(scs_k(F,1))) then return(F),
00033     if clashp(U,U) then return({{}}),
00034     F : apply_pa_cs(U,F)
00035   ))$
00036 
00037 /* Now returning a pair [F,phi], where phi is a list of
00038    partial assignments, corresponding to the blocks of
00039    unit-clauses found (phi_1 comprises the unit-clauses
00040    in F, phi_2 those in pni_1 * F, etc.).
00041    Only forced assignments by unit-clauses are considered
00042    here, and so if {} in F, then the process stops, and the
00043    remaining clauses stay in F.
00044    If in some stage contradictory unit-clauses {x},{-x} are found,
00045    then the positive assignment is applied, while all other eliminations
00046    are ignored (if there are several such x, then that x with lexicographically
00047    first x or -x is chosen).
00048 */
00049 ucp_lpa_0_cs(F) := block([phi : [], U],
00050   do (
00051     if empty_element_p(F) then return(),
00052     if emptyp(U : lunion(scs_k(F,1))) then return(),
00053     if clashp(U,U) then (block(
00054      [x : var_l(first_element(intersection(U,comp_sl(U))))],
00055       F : apply_pa_cs({x},F),
00056       phi : cons({x},phi)),
00057      return()),
00058     F : apply_pa_cs(U,F),
00059     phi : cons(U,phi)
00060   ),
00061   return([F,reverse(phi)]))$
00062 
00063