小编Axe*_*per的帖子

我最近下载GitHub并创建了一个存储库.我正在尝试上传一个Objective C项目.我该怎么做呢？

我试图使用Z3解决12000+布尔变量的SAT问题.我希望大多数变量在解决方案中评估为false.有没有办法引导或提示Z3作为SAT求解器首先尝试"极性假"？我已经尝试使用cryptominisat 2并取得了良好的效果.

我不明白为什么在邻接矩阵中插入一条边需要 O(1) 时间。例如，我们想从顶点 3 到 5 添加一条边，在定向图中我们需要将 graph[2][4] 更改为 1。在定向图中也可以反过来。怎么可能是 O(1)，如果我们至少有一次必须在数组中找到正确的行，那么它已经是 O(|V|)？

为了解决一组布尔方程,我正在使用以下输入试验Constraint-Programming Solver MiniZinc:

%  Solve system of Brent's equations modulo 2

%  Matrix dimensions
int: aRows = 3;
int: aCols = 3;
int: bCols = 3;
int: noOfProducts = 23;

%  Dependent parameters
int: bRows = aCols;
int: cRows = aRows;
int: cCols = bCols;
set of int: products = 1..noOfProducts;

%  Corefficients are stored in arrays
array[1..aRows, 1..aCols, products] of var bool: A;
array[1..bRows, 1..bCols, products] of var bool: B;
array[1..cRows, 1..cCols, products] of var …

该MiniZinc约束求解器允许表达基数约束很容易使用内置的sum()功能：

%  This predicate is true, iff 2 of the array
%  elements are true
predicate exactly_two_sum(array[int] of var bool: x) =
    (sum(x) == 2);

满足基数约束，当且仅当布尔变量数组中的真实元素的数量符合指定。布尔值自动映射到整数值0并1计算总和。

我将自己的基数约束谓词实现为一组计数器切片：

%  This predicate is true, iff 2 of the array
%  elements are true
predicate exactly_two_serial(array[int] of var bool: x) =
    let 
    {
      int: lb = min(index_set(x));
      int: ub = max(index_set(x));
      int: len = length(x);
    }
    in
    if len < 2 then
      false …

大多数消息来源说,在c#中重载++和 - 运算符导致一次性重载postfix和prefix.但看起来他们的行为仍然不同.

class Counter
{
    public Counter(int v = 0)
    {
        this.v = v;
    }
    public Counter(Counter c)
    {
        v = c.v;
    }
    public int GetValue() { return v; }
    public static Counter operator ++(Counter c)
    {
        c.v++;
        return new Counter(c);
    }
    private int v;
}


class Program
{
    public static void Main()
    {
        Counter c1 = new Counter(1);

        Counter c2 = c1++;

        Counter c3 = ++c1;

        c3++;

        System.Console.WriteLine("c1 = {0}", c1.GetValue());
        System.Console.WriteLine("c2 = {0}", c2.GetValue());
        System.Console.WriteLine("c3 = {0}", …

先前问题中指出的安装问题仍然存在.我曾尝试在Windows XP SP3 32位和Windows 7 64位下安装Z3 4.3.0和4.1.这些组合都不起作用!我能够做" from z3 import *",但是init()Z3 dll的失败.我的Python版本是2.7.3.Z3独立和Python独立工作,但没有很多抱怨它们不能一起工作.

这将有助于获得最新的安装配方,回答以下问题:

应该使用哪个Z3下载(源版本,预编译版本)？

应该使用哪个Python版本？

在init()调用中应该引用哪个或哪些Z3 DLL？一个例子会有所帮助(包括带空格的路径的原始字符串用法).

应该使用哪些Z3 Python源文件(Z3的某些下载有*.py文件,其他有*.pyc文件)？编译的Python文件是否与多个Python版本兼容？

如何设置PATH和PYTHONPATH？

如何以自动提供Z3初始化的方式调用Python的IDLE shell？

对不起,如果这听起来像是一个新手问题,但......